Prolog Extensions Based on Tableau Calculus

Abstract

The intention of this paper is to help bridging the gap between logic programming and theorem proving. It presents the design of a Gentzen type proof search procedure, based on classical tableau calculus, for knowledge bases consisting of arbitrary first order formulas. At each proof search step, when a new formula is to be chosen from the knowledge base, the procedure chooses in such a way that the search space is small. When applied to a Horn clause knowledge base and an atomic goal, it performs the same proof search steps as any PROLOG interpreter would do. Hence, PROLOG can be viewed as a special Gentzen type procedure just as it is a special (namely, linear input) resolution procedure.