**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.