Equational methods in first order predicate calculus (Q1065783)
From MaRDI portal
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Equational methods in first order predicate calculus |
scientific article |
Statements
Equational methods in first order predicate calculus (English)
0 references
1985
0 references
The author translates proof procedures (e.g. resolution and narrowing) in quantifier free first order logic (and not in full first order logic as announced in the title) into equational rewriting systems and investigates (partial) confluence and the appropriate modification of the Knuth-Bendix completion algorithm in this context.
0 references
proof procedures
0 references
resolution
0 references
narrowing
0 references
quantifier free first order logic
0 references
equational rewriting systems
0 references
confluence
0 references
Knuth-Bendix completion algorithm
0 references
0 references
