Linear depth deduction with subformula property for intuitionistic epistemic logic

DOI10.1007/s10817-022-09653-zarXiv2103.03377OpenAlexW3134776246MaRDI QIDQ6156631

Guido Fiorino

Publication date: 14 June 2023

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2103.03377

zbMATH Keywords

sequent calculisubformula propertyintuitionistic epistemic logiccounter-models generation

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Constructivism in mathematics. An introduction. Volume I
• Curry-Howard-Lambek correspondence for intuitionistic belief
• Modal type theory based on the intuitionistic modal logic \(\mathrm{IEL}^{-}\)
• First-order intuitionistic epistemic logic
• Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models
• Nested sequents for intuitionistic logics
• An Evaluation-Driven Decision Procedure for G3i
• An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic
• Sequent Calculus for Intuitionistic Epistemic Logic IEL
• A new algorithm for derivability in the constructive propositional calculus
• INTUITIONISTIC EPISTEMIC LOGIC

This page was built for publication: Linear depth deduction with subformula property for intuitionistic epistemic logic