g3ied and rg3ied¶

g3ied is a prover for intuitionistic propositional logic implementing the evaluation driven proof-search procedure for G3i presented in

M. Ferrari, C. Fiorentini, and G. Fiorino. An Evaluation-Driven Decision Procedure for G3i, submittet to ACM Transactions on Computational Logic (TOCL), July 2013.

rg3ied implements the calculus RG3i for Intuitionistic unprovability (which is dual to the direct calculus G3i).

g3ied and rg3ied are implemented upon the jtabwb framework.

Running the prover¶

Download g3ied-1.0.jar and rg3ied-1.0.jar.

Note

g3ied-1.0.jar and rg3ied-1.0.jar require Java 1.8 or later. The LaTeX files generated by the provers depend on the packages tikz, xifthen and proof available at CTAN.

Run the xxx.jar file using the following command:

$ java -jar xxx.jar [options] [problem file]

where [problem file] (optional) is the file containing the problem description and [options] is a list of options. The formula to prove can be specified at command line using the -i option.

Run:

$ java -jar xxx.jar -h

for a detailed description of available options.

Specifying input¶

Formulas must be specified using the following syntax:

Syntax of formulas
  atoms: Java identifiers
logical: false, & (and), | (or), ~ (not), -> (implies), <=> (iff)

notes: (~ A) is translated as (A -> false)
         (A <=> B) is translated as ((A -> B) & (B -> A))

Problem description¶

A problem description is a file describing an input problem. It contains the formulas describing the problem and, possibly, other informations as its name and its provability status.

The prover supports three problem descriptions.

Plain problem description¶

A plain problem description is a file consisting of only one line specifying the formula to prove. To provide such a file as input use the -r plain option. As an example, the following is a plain specification of the double negation of the tertium-non-datur principle.

~(~(p | ~p))

JTabWb problem description¶

A JTabWb problem description is a file having the following structure:

%------------------------
% Formula  : name
% Status   : provable|unprovable
%------------------------
formula
%------------------------

where:

name is the name of the formula;
status specifies if the formula is provable or unprovable;
formula is a formula.

To provide such a file as input use the -r jtw option.

As an example, the following is the specification of above problem in JTabWb-format:

%------------------------
% Formula  : double-negation-tertium-non-datur
% Status   : provable
%------------------------
~(~(p | ~p))
%------------------------

Some problems specified in the JTabWb format are available in ipl_examples_jtabwb.zip.

Output explanation¶

Running the prover you get a summary describing some details about the performed proof-search. For example, running g3ied on the Intuitionistically unprovable Scott principle, you get:

$ java -jar g3ied-1.0.jar ipl_examples_jtabwb/scott.jtabwb
Launcher for G3ied - Evaluation driven calculus for IPL
** Reader [jtawb_format]
> Parsing problem... time (ms) [1]
** Problem [Scott], status [UNPROVABLE]
> Building initial node set... time (ms) [117]
** Prover [g3ied 1.0 (seq=bsf, strategy=plain, evaluation=cover)]
> Proving...
****************************************************************
** Prover [g3ied 1.0 (seq=bsf, strategy=plain, evaluation=cover)]
** Problem [Scott], status [UNPROVABLE], proof-search [FAILURE], test [PASSED]
** Generated nodes [23], restored backtrack-points [2], restored branch-points [5]
** Timings (ms): PS (proof-search) [14], NSC (initial node set) [117], PP (problem parsing) [1]
** Proof time (PS + NSC + PP): (ms) [132]
****************************************************************

The first part of the report describes the actions performed the prover (input parsing, initial node set construction, proof-search). When the proof-search terminates the prover provides details about the performed proof search. In particular the second line describes the result of the proof-search on the given input problem:

status is the status of the input problelm (PROVABLE, UNPROVABLE or UNKNOWN).
proof-search is the status of the proof-search (SUCCESS or FAILURE).
test is PASSED if the status of the formula match the result of the proof-search and FAILED otherwise.

The following lines provide details on the prover execution (number of gnerated nodes, restored backtrack-points and restored branch-point) and execution times.

Running the rg3ied prover on the Scott principle specifying the -model option, the prover performs the proof-search using the RG3i calculus (the calculus for intuitionistic unprovability dual to G3i) and generates the LaTeX rendering of the counter-model for Scott principle.

$ java -jar rg3ied-1.0.jar -model wffs/ipl_examples_jtabwb/scott.jtabwb 
Launcher for RG3IED - evaluation driven unprovability calculus for IPL.
** Reader [jtawb_format]
> Parsing problem... time (ms) [1]
** Problem [Scott], status [UNPROVABLE]
> Building initial node set... time (ms) [116]
** Prover [rg3ied 1.0 (seq=array)]
> Proving...
****************************************************************
** Prover [rg3ied 1.0 (seq=array)]
** Problem [Scott], status [UNPROVABLE], proof-search [SUCCESS], test [PASSED]
** Generated nodes [45], restored backtrack-points [10], restored branch-points [2]
** Timings (ms): PS (proof-search) [20], NSC (initial node set) [116], PP (problem parsing) [1]
** Proof time (PS + NSC + PP): (ms) [137]
****************************************************************
> Generating model...done.
> Model LaTeX source saved in [model.tex]