A general refutational completeness result for an inference procedure based on associative-commutative unification

MaRDI QIDQ1209615zbMATHFDO

Authors Etienne Paul

Publication date 16 May 1993

Published in Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

completenessinference rules\(Q\)- semantic treeAC-paramodulationequality semantic treeextension clauses

Mathematics Subject Classification ID

Recommendations

• Automated deduction with associative-commutative operators
• Paramodulation with built-in AC-theories and symbolic constraints
• AC-complete unification and its application to theorem proving
• Proving refutational completeness of theorem-proving strategies
• Associative-commutative unification

Cited in

(9)

• Unnecessary inferences in associative-commutative completion procedures
• Associative-commutative deduction with constraints
• Cancellative Abelian monoids and related structures in refutational theorem proving. II
• Cancellative Abelian monoids and related structures in refutational theorem proving. I
• Proving refutational completeness of theorem-proving strategies
• AC-superposition with constraints: no AC-unifiers needed
• scientific article; zbMATH DE number 4049135 (Why is no real title available?)
• Theorem proving modulo associativity
• Automated deduction with associative-commutative operators

This page was built for publication: A general refutational completeness result for an inference procedure based on associative-commutative unification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1209615)