scientific article; zbMATH DE number 4043300

MaRDI QIDQ3780487zbMATH OpenFDO

Authors Guangkun Hou, Yang Xia

Publication date 1987

zbMATH Keywords

automatic theorem provingunificationassociative and commutative laws

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 4074540
• Extensions of unification modulo ACUI
• Unification in abelian semigroups
• Associative-commutative unification
• Complexity of unification problems with associative-commutative operators

Cited in

(4)

• AC-complete unification and its application to theorem proving
• scientific article; zbMATH DE number 845925 (Why is no real title available?)
• A technical note on AC-unification. The number of minimal unifiers of the equation \(\alpha x_ 1+ \cdots + \alpha x_ p \doteq _{AC} \beta y_ 1+ \cdots + \beta y_ q\)
• Competing for the \(AC\)-unification race

This page was built for publication:

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