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

zbMATH Open0778.68076MaRDI QIDQ1209615FDOQ1209615

Authors: Etienne Paul 

Publication date: 16 May 1993

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

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

zbMATH Keywords

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

Mathematics Subject Classification ID

Cited In (9)

• Theorem proving modulo associativity
• Cancellative Abelian monoids and related structures in refutational theorem proving. I
• Proving refutational completeness of theorem-proving strategies
• Unnecessary inferences in associative-commutative completion procedures
• Cancellative Abelian monoids and related structures in refutational theorem proving. II
• AC-superposition with constraints: no AC-unifiers needed
• Automated deduction with associative-commutative operators
• Title not available (Why is that?)
• Associative-commutative deduction with constraints

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)