scientific article
From MaRDI portal
Publication:2751362
zbMath1011.03004MaRDI QIDQ2751362
Anatoli Degtyarev, Andrei Voronkov
Publication date: 25 July 2002
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
surveytheorem provingautomated reasoningnonclassical logictableau calculiequality reasoningproof-searchequality eliminationsequent-based methodsimultaneous \(E\)-unificationtranslation of logic
Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Mechanization of proofs and logical operations (03B35) Research exposition (monographs, survey articles) pertaining to computer science (68-02)
Related Items (13)
Free-variable semantic tableaux for the logic of fuzzy inequalities ⋮ Progress in certifying hardware model checking results ⋮ Theorem Proving with Bounded Rigid E-Unification ⋮ Modal Tableau Systems with Blocking and Congruence Closure ⋮ Efficient Algorithms for Bounded Rigid E-unification ⋮ Superposition-based equality handling for analytic tableaux ⋮ Free Variables and Theories: Revisiting Rigid E-unification ⋮ Lean induction principles for tableaux ⋮ Theorem proving modulo ⋮ Congruence Closure with Free Variables ⋮ Fault-Tolerant Aggregate Signatures ⋮ Proof search algorithm in pure logical framework ⋮ THE ELIMINATION OF ATOMIC CUTS AND THE SEMISHORTENING PROPERTY FOR GENTZEN’S SEQUENT CALCULUS WITH EQUALITY
This page was built for publication:
