scientific article; zbMATH DE number 1303344

MaRDI QIDQ4249897zbMATH OpenFDO

Authors Leo Bachmair, Harald Ganzinger, Andrei Voronkov

Publication date 15 September 1999

zbMATH Keywords

experimental resultsautomated reasoningmodel eliminationequational theorem provingelimination of equalityparamodulation calculivariant of Brand's method

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 1552532
• scientific article; zbMATH DE number 1761416
• Theorem-proving with resolution and superposition
• scientific article; zbMATH DE number 1348470

Cited in

(8)

• SCL(EQ): SCL for first-order logic with equality
• SCL(EQ): SCL for first-order logic with equality
• Harald Ganzinger's legacy: contributions to logics and programming
• Computing finite models by reduction to function-free clause logic
• Computationally Equivalent Elimination of Conditions
• Craig interpolation with clausal first-order tableaux
• Superposition with Delayed Unification
• Connection tableaux with lazy paramodulation

Describes a project that uses

Uses Software

• SETHEO

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