×

Restricting backtracking in connection calculi. (English) Zbl 1205.68363

Summary: Connection calculi benefit from a goal-oriented proof search, but are in general not proof confluent. A substantial amount of backtracking is required, which significantly affects the time complexity of the proof search. This paper presents a simple strategy for effectively restricting backtracking in connection calculi. In combination with a few basic techniques it provides the basis for a refined connection calculus. The paper also describes how this calculus can be implemented directly by a few lines of Prolog code. This very compact program is the core of an enhanced version of the automated theorem prover leanCoP. The performance of leanCoP is compared with other lean theorem provers, connection provers, and state-of-the-art theorem provers. The results show that restricted backtracking is a successful technique when performing proof search in connection calculi.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

leanCoP; VAMPIRE; ILTP
PDFBibTeX XMLCite
Full Text: DOI