Input specification¶
The input of the prover consists of the formula to prove. Such a formula can be specified on the standard input or can be read from file. In the latter case two file formats are supported: plain and pitp. In all cases formulas must be specified using the PITP-syntax.
PITP-syntax
Propositional variables:
arbitrary sequences of letters, digits and '_' starting with a letter or '_'
Logical constants in order of precedence (from highest to lowest):
~ (not): prefix, unary
& (and): infix, binary
| (or): infix, binary
-> (implies): infix, binary
Separators: '(', ')'
Formula:: = propositional_variable
| ~ (Formula)
| Formula & Formula
| Formula | Formula
| Formula -> Formula
| (Formula)
true
and false
are treated as propositional variables, it depends on the
prover at hand if they have a special meaning or not (invoke the prover with the
-i
option to see the details on the syntax used by the prover).
Standard input¶
To specify the formula to prove invoke the prover with the -i
option and
specify a formula using the PITP-syntax on one line ended by return.
Plain problem description file¶
A plain problem description is a file consisting of only one line specifying a
formula using the PITP-syntax. 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))
PITP problem description file¶
A PITP 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 specified using the PITP-syntax
To provide such a file as input use the -r pitp
option.
As an example, the following is the specification of above problem in PITP-format:
%------------------------
% Formula : double-negation-tertium-non-datur
% Status : provable
%------------------------
~(~(p | ~p))
%------------------------
Examples¶
A collection of examples: examples.tgz
.