The paper "The Semantics of Predicate Logic as a Programming Language" by M. H. Van Emden and R. A. Kowalski explores the interpretation of first-order predicate logic as a programming language. The authors define both operational and fixpoint semantics for predicate logic programs and investigate their connections with proof theory and model theory. They conclude that operational semantics is a part of proof theory and that fixpoint semantics is a special case of model-theoretic semantics. The paper also discusses the procedural interpretation of Horn clauses, where programs are represented as sets of procedure declarations, and the use of resolution for computation. The authors provide detailed definitions and examples to illustrate these concepts, including the interpretation of well-formed formulas, the procedural interpretation, operational semantics, model-theoretic semantics, and fixpoint semantics. They demonstrate that the equivalence between operational and fixpoint semantics follows from the completeness theorem of first-order logic. The paper concludes by highlighting the broader implications of these findings for both theoretical and practical aspects of computing.The paper "The Semantics of Predicate Logic as a Programming Language" by M. H. Van Emden and R. A. Kowalski explores the interpretation of first-order predicate logic as a programming language. The authors define both operational and fixpoint semantics for predicate logic programs and investigate their connections with proof theory and model theory. They conclude that operational semantics is a part of proof theory and that fixpoint semantics is a special case of model-theoretic semantics. The paper also discusses the procedural interpretation of Horn clauses, where programs are represented as sets of procedure declarations, and the use of resolution for computation. The authors provide detailed definitions and examples to illustrate these concepts, including the interpretation of well-formed formulas, the procedural interpretation, operational semantics, model-theoretic semantics, and fixpoint semantics. They demonstrate that the equivalence between operational and fixpoint semantics follows from the completeness theorem of first-order logic. The paper concludes by highlighting the broader implications of these findings for both theoretical and practical aspects of computing.