The inverse method

MaRDI QIDQ2751355zbMATH OpenFDO

Authors Anatoli I. Degtyarev, Andrei Voronkov

Publication date 27 August 2002

zbMATH Keywords

intuitionistic logicmodal logicsredundancysequent calculidecision proceduremultisetsnamingsubstitutionsinverse methodconstruction of goals from previously proved subgoalshistory of the inverse methodlogics without the contraction rulepath calculipaths in formulassaturation algorithm

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Mechanization of proofs and logical operations (03B35)

Recommendations

• The inverse method application for non-classical logics
• What is the inverse method?
• scientific article; zbMATH DE number 1348471
• Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method
• scientific article; zbMATH DE number 4047178

Cited in

(19)

• Theorem proving based on the extension rule
• scientific article; zbMATH DE number 1765664 (Why is no real title available?)
• Resourceful program synthesis from graded linear types
• Socratic proofs
• A logical characterization of forward and backward chaining in the inverse method
• Gen2sat: an automated tool for deciding derivability in analytic pure sequent calculi
• Logic for Programming, Artificial Intelligence, and Reasoning
• What is the inverse method?
• scientific article; zbMATH DE number 4047178 (Why is no real title available?)
• Complexity of translations from resolution to sequent calculus
• Path calculus in the modal logic S4
• Resolution is cut-free
• Forward proof search for intuitionistic multimodal K logics
• A modal loosely guarded fragment of second-order propositional modal logic
• Disproving using the inverse method by iterative refinement of finite approximations
• Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method
• Unification and anti-unification in applicative matching logic
• A modal two-variable fragment of second-order propositional modal logic
• Decidability of the class E by Maslov's inverse method

This page was built for publication: The inverse method

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