Equational methods in first order predicate calculus (Q1065783)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: Equational methods in first order predicate calculus |
scientific article; zbMATH DE number 3922617
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Equational methods in first order predicate calculus |
scientific article; zbMATH DE number 3922617 |
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
0.9361286
0 references
0.89340556
0 references
0 references
0.8858531
0 references
0 references
