No description, website, or topics provided.
Switch branches/tags
Nothing to show
Clone or download
Pull request Compare This branch is 1 commit behind qkrgud5:master.
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
Makefile
README
TODO
def.ml
formula.ml
formula.mli
label.ml
label.mli
labellookup.ml
labellookup.mli
latex.ml
latex.mli
lexer.mll
parser.mly
prover.ml
rule.ml
rule.mli
sequent.ml
sequent.mli
test_provable
test_unprovable

README

A Theorem Prover for Intuitionistic Modal Logic IS5


Author : Hyungchul Park, Hyeonseung Im, Sungwoo Park


usage: ./prover [-i input_file] [-o output_tex] [-n] [-s shell_script]
  -i : set an input file path, the input file may contain one or more lines of formulas
  -o : set an output tex file path
  -n : this switch prevents proof search
  -s : shell script which runs after the output tex file is generated
  -help  Display this list of options
  --help  Display this list of options

Input Syntax

P := [a-Z] ([alphanum])*                  # atomic formulas 
A := P | true | false | ~ A | A & A | A v A | A -> A | box A | dia A | (A)                
     | A <-> A                            # syntactic sugar (A<->B means (A->B & B->A))


Sample Input

# provable formulas
box (a -> b) -> (box a -> box b)  # K axiom
box a -> a                        # T axiom
dia a -> box (dia a)              # 5 axiom
dia a -> ~ (box (~a))
a & b -> ~(~a v ~b)
p1 & dia p2 -> box (p2 -> p3) -> dia (p2 v p3)
(box((box((box p1) -> (box p1))) -> false)) -> false
dia p1 -> box (p1 -> p2) -> (dia p2 -> p3) -> box (p3 -> p4) -> (dia p4 -> p5) -> p5

# unprovable formulas
a <-> ~~a                         # double negation
a v ~a                            # law of excluded middle
dia a -> a
dia a -> box a
~ (box (~a)) -> dia a
(box(dia((box p12) v ((dia((p1 & (~p2)) v ((~p1) & p2))) v (box((dia((p2 & (~p3)) v ((~p2) & p3))) v (box((dia((p3 & (~p4)) v ((~p3) & p4))) v (box((dia((p4 & (~p5)) v ((~p4) & p5))) v (box((dia((p5 & (~p6)) v ((~p5) & p6))) v (box((dia((p6 & (~p7)) v ((~p6) & p7))) v (box false))))))))))))))) v (box((dia p1) -> (~p12)))


Output

Upon completing a proof search, the theorem prover generates a latex file result.tex which shows a proof tree for the given formula. (You can specify the name of the output file on the command line.)


Update history

- Dec 27, 2012 : initial release
- Jul 22, 2013 : bug fixed(formula signs), proof search optimization(avoid obvious redundancy in the proof search procedure)
- Apr  4, 2018 : updated latex code generation(the syntax is changed), fixed some minor bugs, added comments in the code, removed tabs