scientific article; zbMATH DE number 1303342

MaRDI QIDQ4249895zbMATH OpenFDO

Authors Uwe Waldmann

Publication date 17 June 1999

zbMATH Keywords

automated theorem provingcancellative superposition calculusdivisible torsion-free abelian groupsvariable elimination algorithmvariable overlaps

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Software, source code, etc. for problems pertaining to group theory (20-04)

Recommendations

• scientific article; zbMATH DE number 1405448
• Cancellative Abelian monoids and related structures in refutational theorem proving. II
• Superposition theorem proving for abelian groups represented as integer modules
• Superposition theorem proving for abelian groups represented as integer modules

Cited in

(14)

• Superposition theorem proving for abelian groups represented as integer modules
• Superposition with completely built-in abelian groups
• Cancellative Abelian monoids and related structures in refutational theorem proving. I
• Cancellative Abelian monoids and related structures in refutational theorem proving. II
• Set of support, demodulation, paramodulation: a historical perspective
• Extending reduction orderings to ACU-compatible reduction orderings
• On First-Order Model-Based Reasoning
• scientific article; zbMATH DE number 1765672 (Why is no real title available?)
• Theorem proving in cancellative abelian monoids (extended abstract)
• scientific article; zbMATH DE number 1405448 (Why is no real title available?)
• Superposition theorem proving for abelian groups represented as integer modules
• Automatic decidability and combinability
• ALASCA: reasoning in quantified linear arithmetic
• Refining unification with abstraction

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 Q4249895)