The Semantics of Predicate Logic as a Programming Language
- 1 October 1976
- journal article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 23 (4), 733-742
- https://doi.org/10.1145/321978.321991
Abstract
Sentences in first-order predicate logic can be usefully interpreted as programs. In this paper the operational and fixpoint semantics of predicate logic programs are defined, and the connections with the proof theory and model theory of logic are investigated. It is concluded that operational semantics is a part of proof theory and that fixpoint semantics is a special case of model-theoretic semantics.Keywords
This publication has 8 references indexed in Scilit:
- Linear resolution with selection functionArtificial Intelligence, 1972
- Finding resolution proofs and using duplicate goals in and/or treesInformation Sciences, 1971
- Two Results on Ordering for Resolution with Merging and Linear FormatJournal of the ACM, 1971
- Splitting and reduction heuristics in automatic theorem provingArtificial Intelligence, 1971
- The utility of independent subgoals in theorem provingInformation and Control, 1971
- A Simplified Format for the Model Elimination Theorem-Proving ProcedureJournal of the ACM, 1969
- Properties of Programs and the First-Order Predicate CalculusJournal of the ACM, 1969
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965