Abstract
We give declarative and operational semantics for logics that are expressible as finite sets of abstract clauses. The declarative semantics for these sets of generalized Horn clauses uses inductively defined sets and fixed points. It is shown to coincide with the operational semantics for successful and finitely failed derivations. The Abstract Clause Engine (ACE) implements proofs with abstract clauses. The semantics given here provide criteria for ACE's correctness and completeness.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
P. Aczel, An introduction to inductive definitions, in: Handbook of Mathematical Logic, (J. Barwise, Ed.), North-Holland, Amsterdam, 1977, 739–782.
P.B. Andrews, An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Academic, Orlando, 1986.
H.P. Barendregt, The Lambda-Calculus: Its Syntax and Semantics, Volume II, Second Edition, North-Holland, Amsterdam, 1984.
Th. Coquand and G. Huet, The Calculus of Constructions, Information and Computation 76, 2/3 (1988) 95–120.
M.H. van Emden and R.A. Kowalski, The semantics of predicate logic as a programming language, Journal of the Association for Computing Machinery 24 (1976) 733–742.
R. Harper, F. Honsell, and G. Plotkin, A framework for defining logics, Journal of the Association for Computing Machinery 40, 1 (1983) 143–184.
G.P. Huet, A unification algorithm for typed λ-calculus, Theoretical Computer Science 1 (1975) 27–57.
G.P. Huet, Résolution d'équations dans des Langages d'Ordre 1,2,...,ω, Thèse de Doctorat d'Etat, Université Paris VII, Paris, 1976.
J.M.E. Hyland and A.M. Pitts, The Theory of Constructions: categorical semantics and topos-theoretic models, Contemporary Mathematics 92 (1989) 137–199.
S.C. Kleene, Introduction to Metamathematics, Van Nostrand, Princeton, 1952.
L.C. Paulson, The foundation of a generic theorem prover, Journal of Automated Reasoning 5 (1989) 363–397.
L.C. Paulson, Isabelle: the next 700 theorem provers, In Logic and Computer Science, (P. Oddifreddi, Ed.), Academic, Orlando, 1990, 361–386.
F. Pfenning, Logic programming in the LF logical framework, in: Logical Frame-works, (G. Huet and G. Plotkin, Eds.), Cambridge, 1991, 149–181.
A. Tarski, A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics 5 (1955) 285–309.
D.A. Wolfram, M.J. Maher, and J-L. Lassez, A unified treatment of resolution strategies for logic programs, Proceedings of the Second International Logic Programming Conference, Uppsala, 1984, 263–276.
D.A. Wolfram, ACE: the abstract clause engine, System Summary, Proceedings of the Tenth International Conference on Automated Deduction, Kaiserslautern, Federal Republic of Germany, 23–27 July 1990, Lecture Notes in Artificial Intelligence 449, Springer, Berlin, 1990, 679–680.
D.A. Wolfram, The Clausal Theory of Types, Cambridge Tracts in Theoretical Computer Science 21, Cambridge, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wolfram, D.A. (1994). Semantics for abstract clauses. In: Barendregt, H., Nipkow, T. (eds) Types for Proofs and Programs. TYPES 1993. Lecture Notes in Computer Science, vol 806. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58085-9_85
Download citation
DOI: https://doi.org/10.1007/3-540-58085-9_85
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58085-0
Online ISBN: 978-3-540-48440-0
eBook Packages: Springer Book Archive