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
orUNKNOWN
). - proof-search is the status of the proof-search (
SUCCESS
orFAILURE
). - test is
PASSED
if the status of the formula match the result of the proof-search andFAILED
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.