scientific article
From MaRDI portal
Publication:2751355
zbMath0992.03016MaRDI QIDQ2751355
Andrei Voronkov, Anatoli Degtyarev
Publication date: 27 August 2002
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
inverse methodredundancyintuitionistic logicsubstitutionsmodal logicssequent calculidecision proceduremultisetsnamingconstruction of goals from previously proved subgoalshistory of the inverse methodlogics without the contraction rulepath calculipaths in formulassaturation algorithm
Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05)
Related Items
Socratic proofs ⋮ Disproving Using the Inverse Method by Iterative Refinement of Finite Approximations ⋮ A modal loosely guarded fragment of second-order propositional modal logic ⋮ A logical characterization of forward and backward chaining in the inverse method ⋮ Resolution is cut-free ⋮ Decidability of the Class E by Maslov’s Inverse Method ⋮ Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method ⋮ Gen2sat: An Automated Tool for Deciding Derivability in Analytic Pure Sequent Calculi ⋮ Complexity of translations from resolution to sequent calculus ⋮ Path calculus in the modal logic S4 ⋮ Resourceful program synthesis from graded linear types
