g3ibu

g3ibu is a prover for intuitionistic propositional logic based on the sequent calculi Gbu and Rbu presented in

M. Ferrari, C. Fiorentini, and G. Fiorino. A terminating evaluation-driven variant of G3i. In D. Galmiche and D. Larchey-Wendling, editors, TABLEAUX 2013, LNCS, volume 8123, pages 104-118. Springer-Verlag, 2013.

g3ibu is implemented upon the jtabwb framework.

Running the prover

Download the g3ibu-1.0.jar file.

Note

g3ibu-1.0.jar requires Java 1.8 or later. The LaTeX files generated by the application depend on the packages tikz, xifthen and proof available at CTAN.

Run the g3ibu-1.0.jar file using the following command:

$ java -jar g3ibu-1.0.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 -input option.

By default the proof-search is performed using the calculus Gbu, to use the calculus Rbu you must specify the -ref option.

Run:

$ java -jar g3ibu-1.0.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)

  formula:: = atom 
            | ~ formula
            | formula & formula
            | formula | formula
            | formula -> formula
            | formula <=> formula
            | (formula)

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 in non-verbose mode, we get a summary describing the essential facts about the performed proof-search. For example, running g3ibu on the Intuitionistically unprovable Scott principle, we get:

$ java -jar g3ibu-1.0.jar wffs/ipl_examples_jtabwb/scott.jtabwb 
** Reader [jtawb_format]
> Parsing problem... time (ms) [1]
** Problem [Scott], status [UNPROVABLE]
> Building initial node set... time (ms) [114]
** Prover [g3ibu 1.0 (seq=bsf, eval=min)]
> Proving...
****************************************************************
** Prover [g3ibu 1.0 (seq=bsf, eval=min)]
** Problem [Scott], status [UNPROVABLE], proof-search [FAILURE], test [PASSED]
** Generated nodes [66], restored backtrack-points [8], restored branch-points [19]
** Timings (ms): PS (proof-search) [16], NSC (initial node set) [114], PP (problem parsing) [1]
** Proof time (PS + NSC + PP): (ms) [131]
****************************************************************

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 g3ibu prover on the Scott principle specifying the -p rg3ibu and -proof options, the prover performs the proof-search using the Rbu calculus and generates the LaTeX rendering of the counter-model.

$ java -jar g3ibu-1.0.jar -p rg3ibu -model wffs/ipl_examples_jtabwb/scott.jtabwb 
** Reader [jtawb_format]
> Parsing problem... time (ms) [1]
** Problem [Scott], status [UNPROVABLE]
> Building initial node set... time (ms) [109]
** Prover [rg3ibu 1.0 (seq=bsf)]
> Proving...
****************************************************************
** Prover [rg3ibu 1.0 (seq=bsf)]
** Problem [Scott], status [UNPROVABLE], proof-search [SUCCESS], test [PASSED]
** Generated nodes [95], restored backtrack-points [24], restored branch-points [6]
** Timings (ms): PS (proof-search) [20], NSC (initial node set) [109], PP (problem parsing) [1]
** Proof time (PS + NSC + PP): (ms) [130]
****************************************************************
> Generating model...done.
> Model LaTeX source saved in [model.tex].

Read more: Verbose mode.