scientific article; zbMATH DE number 1303344

zbMATH Open0926.03006MaRDI QIDQ4249897FDOQ4249897

Authors: Leo Bachmair, Harald Ganzinger, Andrei Voronkov 

Publication date: 15 September 1999

Title of this publication is not available (Why is that?)

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

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)

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
• Computationally Equivalent Elimination of Conditions
• Computing finite models by reduction to function-free clause logic
• Craig interpolation with clausal first-order tableaux
• Superposition with Delayed Unification
• Connection tableaux with lazy paramodulation

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)