Proof-search in intuitionistic logic based on constraint satisfaction
From MaRDI portal
Publication:4645245
DOI10.1007/3-540-61208-4_20zbMath1415.03010OpenAlexW1608421539MaRDI QIDQ4645245
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
Analysis of algorithms and problem complexity (68Q25) Complexity of computation (including implicit computational complexity) (03D15) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Subsystems of classical logic (including intuitionistic logic) (03B20)
Related Items (6)
Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem ⋮ Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification ⋮ 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-search in type-theoretic languages: An introduction
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Linearizing intuitionistic implication
- Intuitionistic propositional logic is polynomial-space complete
- Proof search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification
- An improved refutation system for intuitionistic predicate logic
- An Efficient Unification Algorithm
- Contraction-free sequent calculi for intuitionistic logic
- An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic
- Observable Semantics for Constraint Logic Programs
- AC-superposition with constraints: No AC-unifiers needed
- Automated Reasoning
This page was built for publication: Proof-search in intuitionistic logic based on constraint satisfaction
