Devising powerful heuristics or shifting the control to humans have probably been the two most common solutions to keep the search space in theorem proving manageable. In this paper we take advantage of both, by using abstraction as a tool to plan proofs by induction and by proving its effectiveness in ABSFOL (an interactive theorem prover built on top of GETFOL).
Proof planning by abstraction
Villafiorita Monteleone, Adolfo;Sebastiani, Roberto
1994-01-01
Abstract
Devising powerful heuristics or shifting the control to humans have probably been the two most common solutions to keep the search space in theorem proving manageable. In this paper we take advantage of both, by using abstraction as a tool to plan proofs by induction and by proving its effectiveness in ABSFOL (an interactive theorem prover built on top of GETFOL).File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
