IntuitRIL

An extension of the prover intuitR to Intermediate Propositional Logics. See [1] for a presentation; it is implemented in Haskell.

The directory documents contains

• a full version of the paper, with the omitted proofs (pdf)
• the slides presented at IJCAR 2022 (pdf).

The directory examples contains the files obtained by running intuitRIL with the following input formulas in the Gödel-Dummett Logic GL:

• ¬a ∨ ¬¬a     (directory examples/out-jankovAxiom-GL, see Example 3 in the paper)
• (¬a → b ∨ c ) → (¬a → b) ∨ (¬a → c )     (directory examples/out-kpAxiom-GL).

References

[1] Fiorentini Camillo and Mauro Ferrari. SAT-Based Proof Search in Intermediate Propositional Logics.

In: Blanchette et al. (Eds.): IJCAR 2022, LNAI 13385, pp. 57–74, 2022.

https://doi.org/10.1007/978-3-031-10769-6_5 (Open Access)

Haskell installation

You have to install the Haskell toolchain (see the section Installation instructions), in particular:

• GHC: the Glasgow Haskell Compiler
• cabal-install: the Cabal installation tool for managing Haskell software.

IntuitRIL compilation

From the root directory (i.e., the directory containing the file intuitRIL.cabal) run the command:

 cabal install

It should be printed a message like this:

 ....
 Symlinking 'intuitRIL' to '/myHome/.cabal/bin/intuitRIL'

This means that intuitRIL is the command to launch the prover. Actually, intuitRIL is a symbolic link to /myHome/.cabal/bin/intuitRIL; if the command intuitRIL is not found you have to add the directory /myHome/.cabal/bin/ to your PATH variable (or write the complete path of the command).

To print the usage help:

intuitRIL -h

Running

The input formula must be written in a text file. A formula F is specified by the following syntax:

  F :=     atom          // prop. variable
        |  $false        // false
        |   ~F           // not 
        |  F & F         // and
        |  F | F         // or
        |  F => F        // implication 
        |  F <=> F       // bi-implication

Examples of formulas:

(a => b) | ( b => a )
a | (a => b | ~b)
~ a | ~~a
( ((a1 <=> a2) =>  a1 & a2 & a3) & ((a2 <=> a3)  =>  a1 & a2 & a3)  & (( a3 <=> a1)  => a1 & a2 & a3 ) )  =>  a1 & a2 & a3  

You can also use the TPTP syntax. Examples of formulas are available in the directory test (files with suffix .p).

To decide the validity of the formula written in the file form.p in the logic with name LogName, run the command:

 intuitRIL -lLogName form.p

If the option -lLogName is omitted, the default logic is Intuitionistic Propositional Logic; see below the list of the implemented logics.

To generate the output files (trace, models), use the option -t:

 intuitRIL -lLogName  -t form.p

A directory out-... will be created containing the source files (.tex and .gv). To compile them, move into such a directory and enter the command make.

Note that:

• files .tex are compiled using pdflatex.

• files .gv are compiled using the command dot of Graphviz - Graph Visualization Software.

Both the commands pdflatex and dot must be in your PATH variable. If something goes wrong, try to execute the commands:

pdflatex your_file.tex
dot your_file.gv -Tpng -o out.png

Note If the text in the pdf file exceeds the page width, open the tex file and uncomment one of the following lines:

%%\pdfpagewidth 80in  
%%\pdfpagewidth 200in %% MAX WIDTH

Now the text in the pdf is very tiny and must be magnified.

We have implemented other different trace levels (options -tk, with k=0,1,2):

 intuitRIL -l LogName -t0 form.p     // minimum trace level, no output files [DEFAULT]
 intuitRIL -l LogName -t1 form.p     // medium  trace level, no output files 
 intuitRIL -l LogName -t2 form.p     // maximum trace level, no output files 

If you only want to clausify the input formula, use option -c:

 intuitRIL -c form.p

The examples in the directory examples have be obtained by running the following command lines (you have to run the prover from your local directory test or specify the full path of the input files .p):

intuitRIL -lgl -t jankovAxiom.p 
intuitRIL -lgl -t kpAxiom.p

Implemented logics

Logic name	Description
gl	Gödel-Dummett Logic (linear models)
glk	Gödel-Dummett Logic of depth k (linear models with depth at most k, where k≥ 1)
jn	Jankov Logic (one maximal word)
kp	Kreisel and Putnam Logic (*)

(*) Semantic condition:

(w0 < w1) ∧ (w0 < w2) ⇒ ∃ w s.t. (w0 ≤ w) ∧ (w ≤ w1) ∧ (w ≤ w2) ∧ (maxW(w) ⊆ maxW(w1) ∪ maxW(w2))

where maxW(w') is the set of maximal worlds w'' such that w' ≤ w''. Termination is not guaranteed.

Examples:

 intuitRIL -lgl  form.p
 intuitRIL -lgl2 -t0 form.p
 intuitRIL -ljn -t2  form.p
 intuitRIL -lkp -t  form.p