TPTP Problems
- Introduction
- TPTP problems use the
TPTP Format for Problems
- Standard format header provides documentation
- include directives import axiom files
- Comments starting with % or within /* ... */
bracketing
- Example:
SET817+4
- Header fields
- Not for use by ATP
- Problem identification and description
- File - problem name, current TPTP release, and
problem's TPTP release
- Domain - domain, and possibly a subdomain
- Problem - one-line abstract problem description
- Version - problem version differentiation
- English - full description of the problem
- Other occurences
- Refs - relevant references
- Source - where the problem came from
- Names - names by which this problem is known
- Status and syntax
- Status - SZS status of the problem
- Rating -
difficulty ratings over releases
- Syntax - syntactic measures
- General information
- Comments - free format comments
- Bugfixes - describes any bugfixes that have been done
- include directives
- In the TPTP, used to include whole axiom files, unnested
- More selective inclusion, and nested inclusion, is legal
- Formulae
- Of the form language(name,role,formula,source,useful info).
- language - fof and cnf
- name - (hopefully unique) name in problem
- role - gives the user semantics, e.g., axiom,
lemma, conjecture, and hence defines use
in an ATP system.
See
the BNF for the recognized roles.
- formula - logical formula in a human and machine readable
format, based on Prolog syntax.
- Terms and atoms written in prefix notation
- Variables start with Uppercase
- Uninterpreted function and predicate symbols either start with
lower_case and contain alphanumerics and underscore,
or are in 'single quotes'
- Unary connective is ~
- Binary connectives are &, |, =>,
<=, <=>, ~&, and ~|
- Quantifiers are ! (universal) and ?
(existential), with the quantified variables in []s
- Interpreted function and predicate symbols that are
syntactically distinct from uninterpreted ones.
- Defined function and predicate symbols
- $true, $false
- =, !=
- "double quoted distinct objects"
- System function and predicate symbols start with
$$
- source - record where the formula came from
- file records - file name and formula name within
that file
- inference records - for inferred formulae
- ATP system's inference rule name (non-standardized)
- Inference information, e.g., SZS status, assumptions
- Parent formulae names and nested inference records
- useful info - aribtray useful information as required by
user applications