Proof-search in intuitionistic logic based on constraint satisfaction

DOI10.1007/3-540-61208-4_20MaRDI QIDQ4645245zbMATH OpenOpenAlexFDO

Authors Andrei Voronkov

Publication date 10 January 2019

Published in Theorem Proving with Analytic Tableaux and Related Methods (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-61208-4_20

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Complexity of computation (including implicit computational complexity) (03D15) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Analysis of algorithms and problem complexity (68Q25)

Recommendations

• Proof-search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification
• Proof-search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification
• A proof-search procedure for intuitionistic propositional logic
• Labelled proof systems for intuitionistic provability
• Proof search in intuitionistic logic with equality, or back to simultaneous rigid E-unification

Cites work

• AC-superposition with constraints: no AC-unifiers needed
• An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic
• An Efficient Unification Algorithm
• An improved refutation system for intuitionistic predicate logic
• Automated Reasoning
• Contraction-free sequent calculi for intuitionistic logic
• scientific article; zbMATH DE number 3125693 (Why is no real title available?)
• scientific article; zbMATH DE number 4045220 (Why is no real title available?)
• scientific article; zbMATH DE number 49746 (Why is no real title available?)
• scientific article; zbMATH DE number 3639144 (Why is no real title available?)
• scientific article; zbMATH DE number 1348467 (Why is no real title available?)
• scientific article; zbMATH DE number 1348471 (Why is no real title available?)
• scientific article; zbMATH DE number 3299689 (Why is no real title available?)
• scientific article; zbMATH DE number 3335934 (Why is no real title available?)
• Intuitionistic propositional logic is polynomial-space complete
• Linearizing intuitionistic implication
• Observable Semantics for Constraint Logic Programs
• Proof search in intuitionistic logic with equality, or back to simultaneous rigid E-unification

Cited in

(12)

• Representing scope in intuitionistic deductions
• Decidability and complexity of simultaneous rigid E-unification with one variable and related results
• Connection methods in linear logic and proof nets construction
• Proof finding algorithms for implicational logics
• Proof-search in type-theoretic languages: An introduction
• Proof-search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification
• Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem
• Efficient SAT-based proof search in intuitionistic propositional logic
• SAT-based proof search in intermediate propositional logics
• Reasoning about set constraints applied to tractable inference in intuitionistic logic
• scientific article; zbMATH DE number 1354098 (Why is no real title available?)
• Proof-search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification

This page was built for publication: Proof-search in intuitionistic logic based on constraint satisfaction

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