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

MaRDI QIDQ1209615zbMATH OpenFDO

Authors Etienne Paul

Publication date 16 May 1993

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

zbMATH Keywords

\(Q\)- semantic treeAC-paramodulationcompletenessequality semantic treeextension clausesinference rules

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)

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

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)