Abstract
We specify a certain proof search strategy TC based on classical tableau calculus which extends PROLOG to full first order predicate logic. This is meant in the strong algorithmic sense: For the special case of a definite Horn clause knowledge base Σ and an atomic goal α, TC finds a proof for α from Σ if and only if (standard) PROLOG finds that proof. We motivate TC, describe its theoretical background and design, and indicate some principal ways how to interface TC with the outside system.
EARN: SCHFELD at DHDIBMI
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
W. Bibel, Matings in Matrices, Communications of the ACM 26(1983), 844–852
A. Blaser, B. Alschwee, He. Lehmann, Hu. Lehmann, W. Schönfeld, Ein Expertensystem mit natürlichsprachlichem Dialog — Ein Projektbericht, in: W. Brauer, R. Radig (Hrsg.), Wissensbasierte System, GI-Kongrex 1985, Informatik-Fachberichte 112, Springer-Verlag, Berlin 1985, 42–57
W.W. Bledsoe, Non-resolution theorem proving, Artificial Intelligence 9(1977), 1–35
W.A. Carnielli, Systematization of finite many-valued logics through the method of tableaux, J. Symbolic Logic 52.2 (1987), 473–493
A.K. Chandra, D.C. Kozen, L.J. Stockmeyer, Alternation, J. ACM 28(1981), 114–133
K. Clark, Negation as failure, in: H. Gallaire e.a. (eds.), Logic and data bases, Plenum Press, New York 1978
A. Colmerauer, H. Kanoui, R. Pasero, P. Roussel, Un système de communication homme-machine en français, Rapport Groupe Intelligence Artificielle, Marseille 1973.
G. Gentzen, Untersuchungen über das logische Schliessen, Math. Zeitschr. 39 (1934), 167–210, 405–431.
A. Horn, On sentences which are true of direct unions of algebras, J. Symbolic Logic 16(1951), 14–21.
F. Oppacher, E. Suen, Controlling deduction with proof condensation and heuristics, Proc. 8th Conf. Automated Deduction, 384–393
J.A. Robinson, A machine-oriented logic based on the resolution principle, J. ACM 12(1965), 23–41
W. Schönfeld, PROLOG extensions based on tableau calculus, Proc. 9th Int. Conf. Artificial Intelligence, Aug. 1985, Los Angeles, Ca., Vol. 2, 730–732
P.H. Schmitt, The THOT Theorem Prover, TR 87.09.007, IBM Wissenschaftliches Zentrum Heidelberg (1987)
Ehud H. Shapiro, Alternation and the Computational Complexity of Logic Programs, J. Logic Programming 1(1984), 19–33
R.M. Smullyan, First-order logic, Springer-Verlag, Berlin-Heidelberg-New York 1968
G. Wrightson, Semantic tableaux, unification, and links, Technical Report CSD-ANZARP-84-001, University of Wellington, 1984
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1988 Springer-Verlag
About this paper
Cite this paper
Schönfeld, W. (1988). Interfacing a logic machine. In: Börger, E., Büning, H.K., Richter, M.M. (eds) CSL '87. CSL 1987. Lecture Notes in Computer Science, vol 329. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-50241-6_42
Download citation
DOI: https://doi.org/10.1007/3-540-50241-6_42
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-50241-8
Online ISBN: 978-3-540-45960-6
eBook Packages: Springer Book Archive