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

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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11582/4794
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact