Instantiation Theory: On the Foundations of Automated Deduction

Front Cover
Springer Science & Business Media, Aug 7, 1991 - Computers - 133 pages
0 Reviews
Instantiation Theory presents a new, general unification algorithm that is of immediate use in building theorem provers and logic programming systems. Instantiation theory is the study of instantiation in an abstract context that is applicable to most commonly studied logical formalisms. The volume begins with a survey of general approaches to the study of instantiation, as found in tree systems, order-sorted algebras, algebraic theories, composita, and instantiation systems. A classification of instantiation systems is given, based on properties of substitutions, degree of type strictness, and well-foundedness of terms. Equational theories and the use of typed variables are studied in terms of quotient homomorphisms and embeddings, respectively. Every instantiation system is a quotient system of a subsystem of first-order term instantiation. The general unification algorithm is developed as an application of the basic theory. Its soundness is rigorously proved, and its completeness and efficiency are verfied for certain classes of instantiation systems. Appropriate applications of the algorithm include unification of first-order terms, order-sorted terms, and first-order formulas modulo alpha-conversion, as well as equational unification using simple congruences.
 

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

I
1
IV
2
V
4
VII
7
VIII
9
IX
11
XI
17
XII
18
XXX
61
XXXII
64
XXXIII
65
XXXIV
68
XXXV
70
XXXVI
75
XXXVII
81
XXXIX
83

XIII
19
XIV
23
XVI
25
XVII
26
XVIII
28
XIX
33
XX
37
XXII
40
XXIII
45
XXIV
47
XXV
49
XXVI
51
XXVII
52
XXVIII
55
XXIX
56
XL
89
XLI
92
XLII
94
XLIII
97
XLIV
98
XLV
100
XLVI
103
XLVII
108
XLVIII
112
XLIX
116
L
117
LI
121
LII
122
LIII
128
Copyright

Other editions - View all

Common terms and phrases