scientific article

zbMath0739.03011MaRDI QIDQ3972527

Grigori Mints

Publication date: 25 June 1992

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

zbMATH Keywords

modal logiccompletenessintuitionistic logicpropositional logicsresolution ruleclause normal formextension of Maslov's methodresolution-type calculus

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Classical propositional logic (03B05) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items (26)

Proof strategies in linear logic ⋮ Tableau reductions: towards an optimal decision procedure for the modal necessity ⋮ Completeness of a first-order temporal logic with time-gaps ⋮ Cut elimination in coalgebraic logics ⋮ A polynomial space construction of tree-like models for logics with local chains of modal connectives ⋮ Finite tree-countermodels via refutation systems in extensions of positive logic with strong negation ⋮ Resolution with order and selection for hybrid logics ⋮ Three faces of natural deduction ⋮ Intuitionistic Decision Procedures Since Gentzen ⋮ 3-SAT = SAT for a class of normal modal logics ⋮ Proof-terms for classical and intuitionistic resolution ⋮ A resolution theorem prover for intuitionistic logic ⋮ Optimized encodings of fragments of type theory in first order logic ⋮ On temporal logic S4Dbr ⋮ Complexity of subclasses of the intuitionistic propositional calculus ⋮ Linearizing intuitionistic implication ⋮ Resolution is cut-free ⋮ Decidability of the Class E by Maslov’s Inverse Method ⋮ Proof theory of Nelson's paraconsistent logic: a uniform perspective ⋮ What you always wanted to know about rigid E-unification ⋮ Complexity of translations from resolution to sequent calculus ⋮ Proof-search in type-theoretic languages: An introduction ⋮ Path calculus in the modal logic S4 ⋮ Resolution calculus for the first order linear logic ⋮ Admissibility of Cut in Coalgebraic Logics ⋮ Clausal resolution in a logic of rational agency

This page was built for publication: