Interpretations

Specifying a TPTP Format Interpretation

The top level building blocks of TPTP interpretation files are annotated formulae and comments. An annotated formula has the form:

    language(name,role,formula,source,useful info). 

The useful information is optional. The languages currently supported are thf - typed higher-order form, tff - typed first-order form, fof - (full) first-order form, and cnf - clause normal form.

An interpretation is a list of annotated formulae, typically without the source or useful information. (This is a description of an ordinary interpretation - the TPTP language can do a lot more than this.)

• Name: The name is a word starting lower case, e.g., original_f1, or a single quoted word, e.g., 'A crazy $ name'.

• Role: The role for interpretations is interpretation, optionally with a subrole, e.g., interpretation-domains.

• Logical formula: The logical formula uses the TPTP syntax for formulae.

The annotated formulae define the domain and symbol mappings of the interpretation. All the details are in the documentation for the TPTP language.

Example Problem

Here is a FOF countermodel for the toy problem in the Problems page, but with the conjecture changed to:

fof(equality_lost,conjecture,

    ! [H1,H2] :

      ( ( human(H1)

        & human(H2)

        & created_equal(H1,H2) )

    <=> H1 = H2 ) ).

%------------------------------------------------------------------------ 

fof(equality_lost_domain,interpretation-domains,

    ! [X] :

      ( X = "a"

      | X = "f"

      | X = "john"

      | X = "gotA" ) ).

fof(equality_lost_term_mappings,interpretation-mappings,

    ( a = "a"

    & f = "f"

    & john = "john"

    & grade_of("a") = "a"

    & grade_of("f") = "a"

    & grade_of("john") = "f"

    & grade_of("gotA") = "a" ) ).

fof(equality_lost_predicate_mappings,interpretation-mappings,

    ( ~ human("a")

    & ~ human("f")

    & human("john")

    & human("gotA")

    & ~ created_equal("a","john")

    & ~ created_equal("a","gotA")

    & ~ created_equal("f","john")

    & ~ created_equal("f","gotA")

    & ~ created_equal("john","a")

    & ~ created_equal("john","f")

    & ~ created_equal("gotA","a")

    & ~ created_equal("gotA","f")

    & ~ created_equal("a","a")

    & ~ created_equal("a","f")

    & ~ created_equal("f","a")

    & ~ created_equal("f","f")

    & created_equal("john","john")

    & created_equal("john","gotA")

    & created_equal("gotA","john")

    & created_equal("gotA","gotA") ) ).

%------------------------------------------------------------------------ 

Checking an Interpretation

A quick way to check the syntax of an interpretation is to run it through tptp4X, available online in SystemOnTSTP. Select the "Input formulae" option and paste the formulae into the text box. Select tptp4X as the system (or select no System - TPTP4X is the default). ProcessProblem, and if the syntax is faulty an error massage will be returned.

Once the syntax is OK, choose the AGMV model verifier system. RunSelectedSystems and see if it verifies the interpretation.