CINECA IRIS Institutional Research Information System
IRIS è la piattaforma adottata dall’Università degli Studi di Udine per gestire l’archivio aperto dei prodotti della ricerca. L’archivio contiene articoli, contributi in volume, monografie, interventi pubblicati in atti di convegno, Tesi di dottorato e altri materiali.
EnglishIn 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 | Post-print | Non pubblico | Open Access Visualizza/Apri |
http://hdl.handle.net/11390/672425
Copyright © 2018