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: CUP
Year: 1993
Language: English
Pages: 133
Title ......Page 3
Copyright ......Page 4
Contents ......Page 5
Preface ......Page 7
1.1.1 The Skolem-Herbrand-Godel Theorem ......Page 9
1.1.3 Compound Instances ......Page 11
1.1.4 Testing Validity ......Page 12
1.1.5 Unsatisfiability Procedures ......Page 13
1.2 Logic Programming ......Page 15
1.2.2 Refutations and Answers ......Page 17
1.2.4 Negation ......Page 18
1.3 Discussion ......Page 21
1.4 Overview of the Book ......Page 22
2.1 Type Symbols ......Page 25
2.2 Terms ......Page 26
2.3.1 a-Conversion ......Page 28
2.3.2 b-Reduction ......Page 29
2.4 Normal Forms ......Page 30
2.5 Substitutions ......Page 32
3.1 Automating Higher-Order Logic ......Page 35
3.2.1 Syntax ......Page 37
3.3 General Models ......Page 38
3.4 The Clausal Theory of Types ......Page 40
3.4.2 Normal Form CTT Terms ......Page 41
3.5 Term Structures ......Page 44
3.5.1 Lambda-Models ......Page 46
3.5.2 Properties of Lambda-Models ......Page 48
3.6 The Higher-Order Theorem ......Page 49
4.1 Higher-Order Equational Unification ......Page 53
4.1.1 Higher-Order Term Rewriting Systems ......Page 55
4.1.2 Soundness and Completeness ......Page 59
4.1.3 Third-Order Equational Matching ......Page 62
4.2 Higher-Order Unification ......Page 63
4.2.1 Higher-Order Unifiers ......Page 64
4.2.2 Higher-Order Pre-Unification Procedure ......Page 65
4.2.3 Heuristics and Implementations ......Page 67
4.2.4 Undecidability Results ......Page 69
4.3.1 Freezing Lemma ......Page 72
4.4.1 Examples of Nontermination ......Page 73
4.4.2 Removing Constant Symbols ......Page 74
4.4.3 An Algorithm for Higher-Order Matching ......Page 76
4.4.4 Plotkin-Statman Conjecture ......Page 81
4.4.5 Decidable Matching Problems ......Page 84
4.4.6 Regular Unification Problems ......Page 88
4.5 Second-Order Monadic Unification ......Page 92
4.5.1 Decidability and the Monoid Problem ......Page 94
4.6 First-Order Equational Unification ......Page 95
5.1 Higher-Order Equational Resolution ......Page 97
5.1.1 ~-Lambda-Models and Closed Resolution ......Page 99
5.1.2 The General Level ......Page 100
5.2 CTT and Logic Programming ......Page 102
5.2.1 Least CTT Models ......Page 104
5.2.2 Least Fixed Points ......Page 106
5.2.3 BF- and SLD-resolution ......Page 108
5.2.4 Soundness and Completeness ......Page 110
5.2.5 Declarative and Operational Semantics ......Page 112
5.3 Discussion ......Page 113
Bibliography ......Page 115
Index ......Page 129