Restricting backtracking in connection calculi

Issue title: Practical Aspects of Automated Reasoning

Article type: Research Article

Authors: Otten, Jens

Affiliations: Institut für Informatik, University of Potsdam, August-Bebel-Str. 89, 14482 Potsdam-Babelsberg, Germany. E-mail: jeotten@cs.uni-potsdam.de

Abstract: 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.

Keywords: Automated theorem proving, connection calculus, restricted backtracking, leanCoP

DOI: 10.3233/AIC-2010-0464

Journal: AI Communications, vol. 23, no. 2-3, pp. 159-182, 2010