In this paper we present a theoretical basis justifying the incorporation of decidability results for a first-order theory T into an automated theorem prover for T. We state rules which extend resolution using decidability results relative to T in both the ground and the non-ground case, and prove the correctness and completeness of these rules. This is done by considering the ground case of such theories first, and then by applying a straightforward lifting argument. Examples are given illustrating the inference speed-ups which can be obtained by considering decision procedures with resolution-based inference.
Titolo: | T-theorem proving. I |
Autori: | |
Data di pubblicazione: | 1995 |
Rivista: | |
Abstract: | In this paper we present a theoretical basis justifying the incorporation of decidability results for a first-order theory T into an automated theorem prover for T. We state rules which extend resolution using decidability results relative to T in both the ground and the non-ground case, and prove the correctness and completeness of these rules. This is done by considering the ground case of such theories first, and then by applying a straightforward lifting argument. Examples are given illustrating the inference speed-ups which can be obtained by considering decision procedures with resolution-based inference. |
Handle: | http://hdl.handle.net/11390/672425 |
Appare nelle tipologie: | 1.1 Articolo in rivista |
File in questo prodotto:
File | Descrizione | Tipologia | Licenza | |
---|---|---|---|---|
ttp1.pdf | Versione Editoriale (PDF) | Non pubblico | Accesso ristretto Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.