A Theorem Prover for Intuitionistic Modal Logic IS5

Hyungchul Park, Hyeonseung Im, and Sungwoo Park

Introduction

We present an automated theorem prover which implements a bidirectional decision procedure for intuitionistic modal logic IS5. Given a formula in IS5, it first simulates proof search in the forward direction in order to generate a set of inference rules specialized for the goal formula. Then it attempts to build a proof tree composed of these inference rules by performing proof search in the backward direction. Thus, although it internally performs only backward proof search, the decision procedure is effectively bidirectional, thereby taking advantage of both forward and backward proof searches.

Mechanized proof of the cut elimination property in Coq

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]

How to install

Our theorem prover is written in OCaml. To install the prover, you need OCaml v4.00.0 or higher. The prover is freely available under the terms of the GNU Lesser General Public License Version 2.1. It can be downloaded as a gzip'd tarball [prover.tar.gz] or you can access the git repository [github]. 
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

Input and Output

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.) Here is an example of a proof tree for input formula (box((box((box p1) -> (box p1))) -> false)) -> false:
  1. Labeling of the input formula

  2. The set of derived rules

  3. 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".)

Email us at .

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