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.