Equational methods in first order predicate calculus
type: Item
instance of: scholarly article
title: Equational methods in first order predicate calculus
zbMATH Open document ID: 0577.03003
DOI: 10.1016/S0747-7171(85)80026-2
author: Etienne Paul
published in: Journal of Symbolic Computation
publication date: 1985-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03C05
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B20
zbMATH DE Number: 3922617
zbMATH Keywords: proof procedures
zbMATH Keywords: resolution
zbMATH Keywords: narrowing
zbMATH Keywords: quantifier free first order logic
zbMATH Keywords: equational rewriting systems
zbMATH Keywords: confluence
zbMATH Keywords: Knuth-Bendix completion algorithm
MaRDI profile type: Publication
cites work: Q5762080
cites work: Q5679729
cites work: Q3674088
cites work: A complete proof of correctness of the Knuth-Bendix completion algorithm
cites work: Q3883561
cites work: Q5581665
cites work: Q3347863
cites work: Complete Sets of Reductions for Some Equational Theories
cites work: Q5678447
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
cites work: A remark on functionally free algebras
Recommended article: Equational treatment of first-order logic
Recommended article: Q3320371
Recommended article: Complete problems in the first-order predicate calculus
Recommended article: Equational logic as a tool
Recommended article: Q4702593
Recommended article: Q3784072
Recommended article: Equational Reasoning in Non-Classical Logics
Recommended article: Q4345010
Recommended article: Equational reasoning in Isabelle
Recommended article: Equational inference, canonical proofs, and proof orderings
description: scientific article; zbMATH DE number 3922617