---
title: "Prolog Extensions Based on Tableau Calculus"
authors:
  - "Wolfgang Schönfeld"
doi: ""
url: "https://ijcai.org/proceedings/1985/144"
pdf: "https://ijcai.org/proceedings/1985/0144.pdf"
venue: "Proceedings of the Ninth International Joint Conference on Artificial Intelligence"
year: 1985
pages: "730-731"
track: "Logic Programming"
keywords:
---

# Prolog Extensions Based on Tableau Calculus

Wolfgang Schönfeld

*Proceedings of the Ninth International Joint Conference on Artificial Intelligence*, pages 730-731.

## Abstract

The intention of this paper is to help bridging the gap between logic programming and theorem proving. lt presents the design of a Gentzen type proof search procedure, based on classical tableau calculus, for knowledge bases consisting of arbitrary frrst 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 PROLOGinterpreter would do. Hence, PROLOG can be viewed as a special Gentzen type procedure just as it is a special (namely, linear input) resolution procedure.