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

zbMath0778.68076MaRDI QIDQ1209615

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

Related Items (4)

Automated deduction with associative-commutative operators ⋮ Associative-commutative deduction with constraints ⋮ Cancellative Abelian monoids and related structures in refutational theorem proving. I ⋮ Cancellative Abelian monoids and related structures in refutational theorem proving. II

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