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
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 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]
Read more: Verbose mode.