Elimination of equality via transformation with ordering constraints

DOI10.1007/BFB0054259MaRDI QIDQ4249897zbMATH OpenFDO

Authors Leo Bachmair, Harald Ganzinger, Andrei Voronkov

Publication date 15 September 1999

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/11858/00-001M-0000-0014-9A16-2

zbMATH Keywords

automated reasoningelimination of equalityequational theorem provingexperimental resultsmodel eliminationparamodulation calculivariant of Brand's method

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 1552532
• Equality and constrained resolution
• Theorem-proving with resolution and superposition
• Basic paramodulation and superposition

Cited in

(8)

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

Describes a project that uses

Uses Software

• SETHEO

This page was built for publication: Elimination of equality via transformation with ordering constraints

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