cabal install
super LOGIC FILE
# LOGIC:
# -cl Classical Logic
# -il Intuitionistic Logic
# -jn Jankov Logic
# -lc Gödel-Dummett Logic
# "FORMULA" Axiomatisation over IL
# FORMULA:
# p | ~A | A&B | A|B | A=>B
# FILE:
# https://tptp.org/TPTP/SyntaxBNF.html
# Jankov
super -jn test/problems/LCL/LCL181+1.p
# Jankov as extension over IPL
super "~p | ~~p" test/problems/LCL/LCL181+1.p
# Gödel-Dummett
super -lc test/problems/LCL/LCL230+1.p
- Based on a the rules of sequent calculi LJT* and intuitionistic tableau calculus.
- Once a variable
$p$ or$\neg p$ is added to the antecedent, the sequent is substituted with$[\top/p]$ or$[\bot/p]$ respectively. - Formulas are reduced with boolean simplification rules before proof attempt and during substitutions.
- Formulas of the sequent are analyzed through naive focussing, some may be temporarily locked to restrict backtracking.
- Dyckhoff (1992). Contraction-free sequent calculi for intuitionistic logic. doi:10.2307/2275431
- Ferrari (2012). Simplification Rules for Intuitionistic Propositional Tableaux. doi:10.1145/2159531.2159536
- Dyckhoff (2016). Intuitionistic Decision Procedures Since Gentzen. doi:10.1007/978-3-319-29198-7_6