scientific article
From MaRDI portal
Publication:3997615
zbMath0749.03006MaRDI QIDQ3997615
Publication date: 17 September 1992
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
sequent calculusresolution calculusautomated theorem provingtableau calculusconnection methodunifier setcalculus of extended definitional resolutioncomplexities of resolution refutationscomplexity of calculiconnection structure calculus
Analysis of algorithms and problem complexity (68Q25) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Mechanization of proofs and logical operations (03B35)
Related Items (27)
On the relative merits of path dissolution and the method of analytic tableaux ⋮ Accelerating tableaux proofs using compact representations ⋮ A new methodology for query answering in default logics via structure-oriented theorem proving ⋮ Generalizing theorems in real closed fields ⋮ Andrews Skolemization may shorten resolution proofs non-elementarily ⋮ KoMeT ⋮ lean\(T^ AP\): Lean tableau-based deduction ⋮ Invariant-free clausal temporal resolution ⋮ On resolution with short clauses ⋮ An answer to an open problem of Urquhart ⋮ Analytic tableaux for default logics ⋮ Lean induction principles for tableaux ⋮ Non-elementary speed-ups in proof length by different variants of classical analytic calculi ⋮ Towards a unified model of search in theorem-proving: subgoal-reduction strategies ⋮ CERES: An analysis of Fürstenberg's proof of the infinity of primes ⋮ On the practical value of different definitional translations to normal form ⋮ The search efficiency of theorem proving strategies ⋮ Model elimination without contrapositives ⋮ LeanT A P: Lean tableau-based theorem proving ⋮ On Stronger Calculi for QBFs ⋮ Learning from Łukasiewicz and Meredith: investigations into proof structures ⋮ A solver for QBFs in negation normal form ⋮ Prolog technology for default reasoning: proof theory and compilation techniques ⋮ On the modelling of search in theorem proving -- towards a theory of strategy analysis ⋮ Some pitfalls of LK-to-LJ translations and how to avoid them ⋮ A new methodology for developing deduction methods ⋮ Practically useful variants of definitional translations to normal form
This page was built for publication:
