Completeness plays a extremely crucial role in automated theorem proving and it represents an essential desiderata for any calculus one could introduce. As far as a particular calculus is concerned, its Completeness Theorem connects the syntactic aspect of the reasoning activity to its semantic counterpart. This work emphasizes two, somehow orthogonal, aspects of completeness for first-order calculi. From the syntactic point of view, we single out minimal, albeit sufficient, requirements on the underlying language to ensure general completeness results. On the other side, concerning the semantic aspects of automated reasoning, we generalize standard completeness arguments to the case of theory-reasoning (i.e., inference in the context of an underlying and implicit first-order theory), and in particular to the T-resolution approach.

Proving the completeness of theory-based variants of resolution

FORMISANO, Andrea
1999

Abstract

Completeness plays a extremely crucial role in automated theorem proving and it represents an essential desiderata for any calculus one could introduce. As far as a particular calculus is concerned, its Completeness Theorem connects the syntactic aspect of the reasoning activity to its semantic counterpart. This work emphasizes two, somehow orthogonal, aspects of completeness for first-order calculi. From the syntactic point of view, we single out minimal, albeit sufficient, requirements on the underlying language to ensure general completeness results. On the other side, concerning the semantic aspects of automated reasoning, we generalize standard completeness arguments to the case of theory-reasoning (i.e., inference in the context of an underlying and implicit first-order theory), and in particular to the T-resolution approach.
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/11391/918986
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact