Prolog Extensions Based on Tableau Calculus
Proceedings of the Ninth International Joint Conference on Artificial Intelligence. Logic Programming. 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.
@inproceedings{ijcai1985p144,
title = {Prolog Extensions Based on Tableau Calculus},
author = {Schönfeld, Wolfgang},
booktitle = {Proceedings of the Ninth International Joint Conference on
Artificial Intelligence, {IJCAI-85}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Aravind Joshi},
pages = {730--731},
year = {1985},
note = {Logic Programming},
url = {https://ijcai.org/proceedings/1985/144},
}
TY - CPAPER TI - Prolog Extensions Based on Tableau Calculus AU - Schönfeld, Wolfgang T2 - Proceedings of the Ninth International Joint Conference on Artificial Intelligence, IJCAI-85 PB - International Joint Conferences on Artificial Intelligence PY - 1985 SP - 730 EP - 731 UR - https://ijcai.org/proceedings/1985/144 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
