Hyungchul Park, Hyeonseung Im, and Sungwoo Park

- A Bidirectional Proof Search Procedure for Intuitionistic Modal Logic IS5. Hyungchul Park. Master thesis, December 2013. [PDF]
- A Bidirectional Decision Procedure for Intuitionistic Modal Logic IS5. Hyungchul Park, Hyeonseung Im, Sungwoo Park. Submitted for publication, April 2018. [PDF]

We have designed a new sequent calculus for intuitionistic modal logic IS5 and formally proven its cut elimination property using the Coq proof assistant. The sequent calculus uses a new form of label-free sequent which has three different contexts --- local context for describing the current world, global context containing universally valid formulas, and frame for describing accessible worlds. The Coq proof scripts formalize the sequent calculus, prove such structural properties as exchange, weakening, and contraction, and prove the cut elimination property.

The proof scripts along with required libraries can be downloaded as a gzip'd tarball [coq.tar.gz].
Extracting the file creates a subdirectory `coq`,
and you can compile the proof scripts by typing `make`.
You can generate all the documents using coqdoc by typing `make doc`.
We have tested all the proof scripts on Coq 8.3pl4 (April 2012).

Click on the dependency graph to see each proof script:
[dependency graph and coq scripts]

tar xvzf prover.tar.gz cd is5 make ./prover # command line interactive prover ./prover -i test # proof search for the formula in input file 'test' ./prover -help # to display switch options

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))

# 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)))

- Labeling of the input formula

- The set of derived rules

- The proof tree for the input formula
(both superscripts 'a' and 'b' in rule names denote "global"
if the principal formula resides in the global context;
otherwise, 'a' denotes "local" and 'b' denotes "frame".)

Programming Language Laboratory Department of Computer Science and Engineering Pohang University of Science and Technology (POSTECH) Republic of Korea