5 Input Language

5.1 LOP

E natively uses E-LOP, a dialect of the LOP language designed for SETHEO.At the moment, your best bet is to retrieve the LOP description from the E web site [Sch99] and/or check out the examples available from it. LOP is very close to Prolog, and E can usually read many fully declarative Prolog files if they do not use arithmetic or rely on predefined symbols. Plain SETHEO files usually also work very well. There are a couple of minor differences, however:

5.2 TPTP Format

The TPTP [Sut05] is a library of problems for automated theorem prover. Problems in the TPTP are written in TPTP syntax. There are two major versions of the TPTP syntax, both of which are supported by E.

Version 212 of the TPTP syntax was used up for TPTP releases previous to TPTP 3.0.0.

The current version 3 of the TPTP syntax, described in [SSCG06], covers both input problems and both proof and model output using one consistent formalism. It has been used as the native format for TPTP releases since TPTP 3.0.0.

Parsing in TPTP format version 2 is enabled by the options --tptp-in, tptp2-in, --tptp-format and --tptp2-format. The last two options also select TPTP 2 format for the output of normal clauses during and after saturation. Proof output will be in PCL2 format, however.

As an alternative, E also supports TPTP-3 syntax with the options --tstp-in , tptp3-in, --tstp-format and --tptp3-format. The last two options will also enable TPTP-3 format for proof output. Note that many of E’s support tools still require PCL2 format. Various tools for processing TPTP-3 proof format are available via the TPTP web-site, http://www.tptp.org.

In either TPTP format, clauses and formulas with TPTP type conjecture or negated-conjecture (TPTP-3 only) are considered goal clauses for the --sos-uses-input-types option.

12Version 1 allowed the specification of problems in clause normal form only. Version 2 is a conservative extension of version 1 and adds support for full first order formulas.