TPTP Format for Finite Interpretations

Introduction

A finite interpretation (or "finite model" of some identified formulae) consists of a finite domain, an interpretation of functors - a functor applied to domain elements is interpreted as a domain element, and an interpretation of predicates - a predicate applied to domain elements is interpreted as either true or false. The elements of the domain are known to be distinct. The interpretation of functors and predicates is total, i.e., there is an interpretation for every functor and predicate for every pattern of domain element arguments.

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

Specifying the Domain

The domain of a finite interpretation is written in the form:

    fof(fi_name,fi_domain,
        ! [X] : ( X = e₁ | X = e₂ | ... | X = e_n )  ).

where the e_i are all "distinct object"s, or all distinct integers, or all distinct constant terms. If "distinct object"s or integer terms appear in the interpreted signature, then all those terms must appear in the domain. If constant terms are used they are freely chosen constants that do not appear in the signature being interpreted. The e_i values provide an exhaustive list of terms whose interpretation form the domain (there is a bijection from the terms to the domain, so one may think of the terms directly as the domain elements). The use of "distinct object"s or integer terms for a domain is preferred over constant terms, because it takes advantage of the predefined interpretation of such terms - all such terms and corresponding domain elements are known to be distinct. If the domain elements are constant terms then their inequality must be explicitly stated in annotated formulae of the form:

    fof(e_i_not_e_j,fi_domain,
        e_i != e_j ).

Specifying the Functor and Predicate Interpretations

The interpretation of functors is written in the form:

    fof(fi_name ,fi_functors,
        ( f(e₁,...,e_m) = e_r
        & f(e₁,...,e_p) = e_s
        ...  )   ).

specifying that, e.g., f(e₁,...,e_m) is interpreted as the domain element e_r. If "distinct object"s or integer terms appear in the interpreted signature, then those terms are necessarily interpreted as themselves and must not be interpreted in the fi_functors.

The interpretation of predicates is written in the form:

    fof(fi_name ,fi_predicates,
        ( p(e₁,...,e_m)
        & ~ p(e₁,...,e_p)
        ...  )   ).

specifying that, e.g., p(e₁,...,e_m) is interpreted as true and p(e₁,...,e_p) is interpreted as false. Equality is naturally interpreted by the domain, with the understanding that identical elements are equal.

Example

Consider the following FOF problem that is CounterSatisfiable, i.e., there is a model for the axioms and negated conjecture.

%----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) )  ).
%------------------------------------------------------------------------------

Layout and Variations

Normally every functor and predicate is interpreted once for every pattern of domain element arguments. No functor or predicate may be interpreted more than once for an argument pattern. If a functor or predicate is not interpreted for a given argument pattern then multiple interpretations are being represented, in which that functor or predicate applied to the argument pattern is interpreted as each of the possible values (each domain element for a functor, both true and false for a predicate).

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") )  ).

Verifying Models

An interpretation can be verified as a model of a set of formulae by directly evaluating each formula in the model. The TPTP format also provides an alternative approach - the interpretation is adjoined to the formulae, and a trusted model finder is then used to find a model of the combined formula set.

Infinite Interpretations

Although there is no firm proposal for the representation of infinite interpretations, the following ideas have arisen:

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.

This format was developed by Koen Claessen and Geoff Sutcliffe, and has benefited from input at the 2005 TPTP Tea Party.