scientific article; zbMATH DE number 1303344

zbMath0926.03006MaRDI QIDQ4249897

Andrei Voronkov, Leo Bachmair, Harald Ganzinger

Publication date: 15 September 1999

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

automated reasoningexperimental resultsmodel eliminationequational theorem provingelimination of equalityparamodulation calculivariant of Brand's method

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (7)

Craig interpolation with clausal first-order tableaux ⋮ Connection tableaux with lazy paramodulation ⋮ Harald Ganzinger’s Legacy: Contributions to Logics and Programming ⋮ SCL(EQ): SCL for first-order logic with equality ⋮ Superposition with Delayed Unification ⋮ Computing finite models by reduction to function-free clause logic ⋮ SCL(EQ): SCL for first-order logic with equality

Uses Software

• Unnamed Item

This page was built for publication: