The TPTP language is sufficient for recording a finite interpretation. The domain, interpretation of functors, and interpretation of predicates, are written as FOF annotated formulae. A recorded interpretation provides the information required for various forms of processing, such as model verification, interpretation of formulae, and identification of isomorphic interpretations. The goals of the representation format are:

- Use the TPTP syntax with as little modification as possible
- Use FOF formulae to represent all aspects
- A representation that is amenable to checking and use
- A representation that is compact
- A representation that allows multiple interpretations to be easily represented

fof(where thefi_name,fi_domain, ! [X] : ( X =e| X =_{1}e| ... | X =_{2}e) )._{n}

fof(e_not__{i}e,fi_domain,_{j}e!=_{i}e)._{j}

fof(specifying that, e.g.,fi_name,fi_functors, ( f(e,...,_{1}e) =_{m}e& f(_{r}e,...,_{1}e) =_{p}e... ) )._{s}

The interpretation of predicates is written in the form:

fof(specifying that, e.g.,fi_name,fi_predicates, ( p(e,...,_{1}e) & ~ p(_{m}e,...,_{1}e) ... ) )._{p}

%----All (hu)men are created equal. John is a human. John got an F grade. %----There is someone (a human) who got an A grade. An A grade is not %----equal to an F grade. Grades are not human. Therefore, it is not the %----case being created equal is the same as really being equal. fof(all_created_equal,axiom, ! [H1,H2] : ( ( human(H1) & human(H2) ) => created_equal(H1,H2) ) ). fof(john,axiom, human(john) ). fof(john_failed,axiom, grade(john) = f ). fof(someone_got_an_a,axiom, ? [H] : ( human(H) & grade(H) = a ) ). fof(distinct_grades,axiom, a != f ). fof(grades_not_human,axiom, ! [G] : ~ human(grade(G)) ). fof(equality_lost,conjecture, ! [H1,H2] : ( created_equal(H1,H2) <=> H1 = H2 ) ). %------------------------------------------------------------------------------Here is a model for the axioms and negated conjecture (adapted from the one found by Paradox 1.3):

%------------------------------------------------------------------------------ fof(equality_lost,interpretation_domain, ! [X] : ( X = "a" | X = "f" | X = "john" | X = "got_A") ). fof(equality_lost,interpretation_terms, ( a = "a" & f = "f" & john = "john" & grade("a") = "f" & grade("f") = "a" & grade("john") = "f" & grade("got_A") = "a" ) ). fof(equality_lost,interpretation_atoms, ( ~ human("a") & ~ human("f") & human("john") & human("got_A") & ~ created_equal("a","a") & ~ created_equal("a","f") & ~ created_equal("a","john") & ~ created_equal("a","got_A") & ~ created_equal("f","a") & ~ created_equal("f","f") & ~ created_equal("f","john") & ~ created_equal("f","got_A") & ~ created_equal("john","a") & ~ created_equal("john","f") & created_equal("john","john") & created_equal("john","got_A") & ~ created_equal("got_A","a") & ~ created_equal("got_A","f") & created_equal("got_A","john") & created_equal("got_A","got_A") ) ). %------------------------------------------------------------------------------Here's the same example using constant terms for domain elements:

%------------------------------------------------------------------------------ fof(equality_lost,interpretation_domain, ! [X] : ( X = e_a | X = e_f | X = e_john | X = e_got_A) ). fof(equality_lost,interpretation_domain, ( e_a != e_f & e_a != e_john & e_a != e_got_A & e_f != e_john & e_f != e_got_A & e_john != e_got_A ) ). fof(equality_lost,interpretation_terms, ( a = e_a & f = e_f & john = e_john & grade(e_a) = e_f & grade(e_f) = e_a & grade(e_john) = e_f & grade(e_got_A) = e_a ) ). fof(equality_lost,interpretation_atoms, ( ~ human(e_a) & ~ human(e_f) & human(e_john) & human(e_got_A) & ~ created_equal(e_a,e_a) & ~ created_equal(e_a,e_f) & ~ created_equal(e_a,e_john) & ~ created_equal(e_a,e_got_A) & ~ created_equal(e_f,e_a) & ~ created_equal(e_f,e_f) & ~ created_equal(e_f,e_john) & ~ created_equal(e_f,e_got_A) & ~ created_equal(e_john,e_a) & ~ created_equal(e_john,e_f) & created_equal(e_john,e_john) & created_equal(e_john,e_got_A) & ~ created_equal(e_got_A,e_a) & ~ created_equal(e_got_A,e_f) & created_equal(e_got_A,e_john) & created_equal(e_got_A,e_got_A) ) ). %------------------------------------------------------------------------------

It is recommended that interpretations follow a standard layout, as illustrated by the examples above. However, the conjuncts of function and predicate interpretations can also be separated into individual annotated formulae, and compact forms are possible using more complex formulae, e.g.,

fof(equality_lost,interpretation_atoms, ( ~ human("a") & ~ human("f") & human("john") & human("got_A") & ! [X] : ~ created_equal("a",X) & ! [X] : ~ created_equal("f",X) & ! [X] : ~ created_equal(X,"a") & ! [X] : ~ created_equal(X,"f") & created_equal("john","john") & created_equal("john","got_A") & created_equal("got_A","john") & created_equal("got_A","got_A") ) ).

- Herbrand interpretations can be represented by term grammars, e.g.,
formulae of the form:
! [X,Y] : ( p(X,Y) <=> ( ( X != a & Y != a ) | ( X = a & Y = a ) ) )

There are decision procedures for the validity of ground atoms in the context of such formulae. - Saturations can represent infinite models. These would contain the saturated set of clauses and %$$ comments to specify the ordering, etc.
- The forthcoming higher order format
`thof`may be used to capture fixed points.