next up previous
Next: The Logical Parts Up: Common Syntax of the Previous: Notation

Problems

The unit of information we can describe are problems. A problem may not only contain formulae or clauses but also information on parameter settings for various provers or some specific proofs.

problem ::= begin_problem(identifier).
    description
    logical_part
    {settings}$^\ast$
    end_problem.

Note that the description part as well as the logical part are mandatory.



Uwe Brahm
1999-09-15