scientific article; zbMATH DE number 15881

MaRDI QIDQ3972527zbMATH OpenFDO

Authors G. E. Mints

Publication date 25 June 1992

zbMATH Keywords

clause normal formcompletenessextension of Maslov's methodintuitionistic logicmodal logicpropositional logicsresolution ruleresolution-type calculus

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 510785
• scientific article; zbMATH DE number 4055570
• Gentzen-type systems, resolution and tableaux
• scientific article; zbMATH DE number 683345
• scientific article; zbMATH DE number 4027425

Cited in

(44)

• Gentzen systems, resolution, and literal trees
• Linearizing intuitionistic implication
• Gentzen-type systems, resolution and tableaux
• Resolution calculus for the first order linear logic
• A Gentzen system for conditional logic
• Proof strategies in linear logic
• Completeness of a first-order temporal logic with time-gaps
• A polynomial space construction of tree-like models for logics with local chains of modal connectives
• Proof-search in type-theoretic languages: An introduction
• Clausal resolution in a logic of rational agency
• Resolution with order and selection for hybrid logics
• On temporal logic S4Dbr
• Gentzen-like systems for partial propositional calculi. I. II
• Path calculus in the modal logic S4
• Admissibility of cut in coalgebraic logics
• Tableau reductions: towards an optimal decision procedure for the modal necessity
• Intuitionistic Decision Procedures Since Gentzen
• Decidability of the class E by Maslov's inverse method
• scientific article; zbMATH DE number 4027425 (Why is no real title available?)
• scientific article; zbMATH DE number 510785 (Why is no real title available?)
• scientific article; zbMATH DE number 517002 (Why is no real title available?)
• scientific article; zbMATH DE number 2042613 (Why is no real title available?)
• Three faces of natural deduction
• A resolution theorem prover for intuitionistic logic
• Proof-terms for classical and intuitionistic resolution
• Optimized encodings of fragments of type theory in first order logic
• What you always wanted to know about rigid \(E\)-unification
• Complexity of translations from resolution to sequent calculus
• Finite tree-countermodels via refutation systems in extensions of positive logic with strong negation
• Cut elimination in coalgebraic logics
• Resolution calculi for non-normal modal logics
• Improved decision procedures for the modal logics K, T and S4
• Dual tableau-based decision procedures for fragments of the logic of binary relations
• Proof-theoretic results of common sense modal predicate calculi
• 3-SAT = SAT for a class of normal modal logics
• Forward proof search for intuitionistic multimodal K logics
• Improved decision procedures for multi-modal tense logic using CEGAR-tableaux
• From modal sequent calculi to modal resolution
• Complexity of subclasses of the intuitionistic propositional calculus
• On an inferential semantics for intuitionistic sentential logic
• Refutations and proofs in the paraconsistent modal logics: \textbf{KN4} and \textbf{KN4.D}
• Non-iterative modal resolution calculi
• Proof theory of Nelson's paraconsistent logic: a uniform perspective
• Resolution is cut-free

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3972527)