This book presents the theoretical foundation of a higher-order logic programming language with equality, based on the clausal theory of types. A long-sought goal of logic programming, the clausal theory of types is a logic programming language that allows functional computation as a primitive operation while having rigorous, sound, and complete declarative and operational semantics. The language is very powerful, supporting higher-order equational deduction and functional computation. Its higher order syntax makes it concise and expressive, abstract data types can be expressed in it, and searching for multiple solutions is a basic operation. The author proves a number of important and surprising results: a Skolem-Herbrand-Gödel theorem for higher-order logic; a Higher-Order Resolution Theorem, which includes as special cases some previously unproven conjectures about equational matching and higher-order matching.
Author(s): D. A. Wolfram
Series: Cambridge Tracts in Theoretical Computer Science 21
Publisher: Cambridge University Press
Year: 1993
Language: English
Pages: 133
Cover......Page 1
Cambridge Tracts in Theoretical Computer Science......Page 3
The Clausal Theory of Types......Page 4
9780521117906......Page 5
Contents......Page 6
Preface......Page 8
1.1.1 The Skolem-Herbrand-Godel Theorem......Page 10
1.1.3 Compound Instances......Page 12
1.1.4 Testing Validity......Page 13
1.1.5 Unsatisfiability Procedures......Page 14
1.2 Logic Programming......Page 16
1.2.2 Refutations and Answers......Page 18
1.2.4 Negation......Page 19
1.3 Discussion......Page 22
1.4 Overview of the Book......Page 23
2.1 Type Symbols......Page 26
2.2 Terms......Page 27
2.3.1 α-Conversion......Page 29
2.3.2 β-Reduction......Page 30
2.4 Normal Forms......Page 31
2.5 Substitutions......Page 33
3.1 Automating Higher-Order Logic......Page 36
3.2.1 Syntax......Page 38
3.3 General Models......Page 39
3.4 The Clausal Theory of Types......Page 41
3.4.2 Normal Form CTT Terms......Page 42
3.5 Term Structures......Page 45
3.5.1 λ-Models......Page 47
3.5.2 Properties of λ-Models......Page 49
3.6 The Higher-Order Theorem......Page 50
4.1 Higher-Order Equational Unification......Page 54
4.1.1 Higher-Order Term Rewriting Systems......Page 56
4.1.2 Soundness and Completeness......Page 60
4.1.3 Third-Order Equational Matching......Page 63
4.2 Higher-Order Unification......Page 64
4.2.1 Higher-Order Unifiers......Page 65
4.2.2 Higher-Order Pre-Unification Procedure......Page 66
4.2.3 Heuristics and Implementations......Page 68
4.2.4 Undecidability Results......Page 70
4.3.1 Freezing Lemma......Page 73
4.4.1 Examples of Nontermination......Page 74
4.4.2 Removing Constant Symbols......Page 75
4.4.3 An Algorithm for Higher-Order Matching......Page 77
4.4.4 Plotkin-Statman Conjecture......Page 82
4.4.5 Decidable Matching Problems......Page 85
4.4.6 Regular Unification Problems......Page 89
4.5 Second-Order Monadic Unification......Page 93
4.5.1 Decidability and the Monoid Problem......Page 95
4.6 First-Order Equational Unification......Page 96
5.1 Higher-Order Equational Resolution......Page 98
5.1.1 ~-λ-Models and Closed Resolution......Page 100
5.1.2 The General Level......Page 101
5.2 CTT and Logic Programming......Page 103
5.2.1 Least CTT Models......Page 105
5.2.2 Least Fixed Points......Page 107
5.2.3 BF- and SLD-resolution......Page 109
5.2.4 Soundness and Completeness......Page 111
5.2.5 Declarative and Operational Semantics......Page 113
5.3 Discussion......Page 114
Bibliography......Page 116
Index......Page 130
