Instantiation theory. On the foundations of automated deduction (Q1202066)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Instantiation theory. On the foundations of automated deduction |
scientific article |
Statements
Instantiation theory. On the foundations of automated deduction (English)
0 references
23 January 1993
0 references
Instantiation, or the theory of variable substitution in terms, is studied here in an abstract setting. In order to make the theory as general and clean as possible, the basic concepts are introduced axiomatically, so that, rather than working upon any particular formalism, such as the terms of first-order predicate logic or lambda- calculus, all such term systems are examples. The climax of the text is a unification algorithm which is proven to be sound and, under appropriate conditions, complete; the complexity of the algorithm is also discussed. Other topics along the way include further properties that an instantiation system might enjoy, such as various degrees of type strictness and well-foundedness of terms, and quotient system, subsystems, and homomorphisms.
0 references
instantiation
0 references
variable substitution
0 references
term systems
0 references
unification
0 references
complexity
0 references
well-foundedness
0 references