Interpretation Representation and Model Verification

by Geoff Sutcliffe, Alex Steen, Pascal Fontaine, Jack McKeown

Representation of Interpretations in the TPTP World

Background
Representation of FOF Finite interpretations
Representation of FOF Saturation interpretations
Representation of FOF Formulae interpretations
Representation of TFF Finite interpretations
Representation of TXF Finite interpretations
Representation of THF Finite interpretations
Representation of TFF Infinite interpretations
- Representation of TFF Infinite interpretations using uninterpreted terms
- Representation of TFF Infinite interpretations using defined terms
- Representation of TFF Mixed interpretations
Representation of Kripke interpretations
Representation of Finite-Finite Kripke interpretations
- Representation of Finite-Finite Kripke interpretations with only global axioms
- Representation of Finite-Finite Kripke interpretations with global and local axioms
Representation of Finite-Infinite Kripke interpretations
Representation of Infinite-Finite Kripke interpretations
Representation of Infinite-Infinite Kripke interpretations

Background

Why is Model Finding Useful?

Checking the consistency of an axiomatization. [Sutcliffe]
Finding the countermodel for a conjecture [Claessen], in particular ...
In fault finding applications, e.g., in software verification, a countermodel for a proof obligation points to the location of the fault. [Sutcliffe]
Finding a solution to a problem that is coded as a model finding problem. [Claessen]
In teaching it is really useful to inspecting outcomes of student's experiments. [Steen]

Is there a need for model finding systems that:

Give only a "yes", indicating that there is a model.
- In an (industrial) application where models indicate bugs, users would probably get very frustrated. [McCune]
- Acceptable, but a model is preferred. [Claessen]
- As part of a decision procedure, sat/unsat could be used as a yes/no subroutine. I do use this for my I/O logic reasoner. [Steen]
Give only a "yes, finite", indicating that there is a finite model.
Output a model in some form
- In the case of a countermodel for a conjecture, one would like to have some concrete representation of it to see why the theorem cannot be proved. [Claessen]
- Sometimes it is very easy to find satisfiability (a saturation) with ordered resolution even if there is a finite model. [Tammet]
- Regardless of the cardinalities, applications that use ATP systems to find models typically need an explicit model with a domain and symbol mapping. [Sutcliffe]
Output a finite model in some form
- Finite models are used to evaluate other clauses. [McCune]
- It's better to require the output of a finite model as this can be easily checked by other systems. [Zhang]
- It is not enough to know that there is a solution; one would like to know what the solution is. [Claessen]

Representation of Interpretations

Infinite domains are necessary as soon as the formula language contains any numbers on an infinite domain (not arithemetic modulo). Infinite domains are also necessary for other (non-numeric) applications, e.g., those that involve modeling time. Types of interpretations include:

Classical interpretations
- Interpretations with a finite domain, and the symbol interpretations. These are called finite interpretations. The finite domain can be:
  - Explicitly enumerated.
  - The finite Herbrand Universe of a Herbrand interpretation.
- Interpretations with an infinite domain, and the symbol interpretations. These are called infinite interpretations. The infinite domain can be:
  - Explicitly generated, e.g., Peano arithmetic terms.
  - Explicitly specified, e.g., the integers.
  - Algebraic numbers (real closed fields)
  - The infinite Herbrand Universe of a Herbrand interpretation.
  - One can explicitly state that it's infinite while leaving open how this is realized, e.g., "in all infinite domains, it holds that ..."
  - Any others?
- Saturations. Saturations embody a Herbrand interpretation.
- Models that are nearly constant everywhere, as used in the SMT world for model-based quantifier instantiation.
- Consistent sets of formulae represent families of interpretations. [Steen]
- +You can read off a satisfying assignment from a non-closable tableau, right? [Steen]
- Any others?
Non-classical Kripke interpretations
- Kripke interpretations with a finite number of worlds.
- Kripke interpretations with an infinite number of worlds. Infinite worlds are necessary when there are, e.g., in alethic modal logic, an infinite number of possibilities; in temporal logics, R is serial (always has a successor) and non-circular etc., so there have to be infinitely many worlds (points in time). [Steen]
- Within each world of a Kripke interpretation there is a classical interpretation, with the options as above.

Properties of Different Representations

A finite model with an enumerated domain, and the symbol interpretations.
- My experience suggests that one would prefer a finite model over a saturation. [Claessen]
- A finite model can be abbreviated in some way, e.g., if a 30-ary predicate is true for all but three cases, it is enough to mention those 3 cases and a default case. A large predicate table can be expressed in terms of a few smaller ones, e.g., p(X,Y) := q(X) & r(Y). [Claessen]
A definition of an infinite domain, and the symbol interpretations.
- The domain must be adequate for interpreting all formulae. [Sutcliffe]
- I hope it will be OK to specify the interpretation for that subset of an infinite domain that is used, for which the range coincides with the domain. The subset is induced by interpretation of terms, first constants, then inductively by functions. But what if no constants ... add a new constant as done for the Herbrand Universe in a Herbrand interpretation? [Sutcliffe]
- There are uncountably many interpretations: whatever the language, it will be possible to represent only a small (negligible) subset of all models.
- The only ATP systems I know of that can produce an explicit infinite domain model are Z3 (Pascal says) and cvc5 (I think!). [Sutcliffe]
A saturation.
- Hardly a useful artifact. [Sutcliffe]
- Saturations are pretty much impossible to interpret explicitly in a way that can be used constructively by users. [Sutcliffe]
- A saturation is not a direct representation of a finite model. [Tammet]
- A saturation tells you only that models exist, but very little about what they might look like. Take some equational axioms for a group plus a denial of commutativity; the typical saturation gives the complete set of reductions for free groups plus the denial of commutativity, which does help finding an example of a non-commutative group. [McCune]
- There are classes of problem (including problems where all models are infinite) in which saturation can tell you everything about the models. [McCune]
- A saturated set of clauses at the end doesn't mean much for other systems. [Zhang]
- I have never been able to make use of a saturated clause set. [Claessen]
- The clauses of a saturation could in principle be used for checking whether some later presented finite part of an infinite model is OK. [Tammet]
- In some sense the saturation does not differ very much from the original clause set: the saturation is also just a clause set, and is typically not a fixpoint for other search strategies. [Tammet]
- Given a saturation and the system search control, it's sometimes possible to decide if a ground atom is TRUE or FALSE. [Schulz] In the general case you cannot even decide ground atoms. [Tammet]
- There have been several attempts to improve the representation (Viennese ATP researchers (Leitsch, Baaz, Fermüller etc.), but the improvements are basically still the fixpoint set of clauses. [Tammet]
- I have never read the proof of completeness of superposition but isn't it the case that a saturation allows to build a model? [Fontaine]
- An email exchange with Joe Schoisswohl and Cezary Kaliszyk
```
A Saturation (S) is a way of writing a Herbrand interpretation
(HI) of input formulae (I). I learned that a HI consists of:

Domain (D) = The Herbrand Universe (HU), and if the HU is empty add a new
           constant.
Function map (F) = Identity
Predicate map (P) = Some way of saying which elements of the Herbrand
           Base (HB) are true/false.

So, simplistically, S can be represented in the TPTP format by providing
the conjunction of the universally quantified formulae of S. Yeah, I know
a saturation is modulo the ATP system's ordering, so it might not be
possible to prove S |= I, but let's gloss over that for now. There might
be a deeper issue: In the CNF context, S can contain symbols not in I
(e.g., Skolems), and hence not part of the HU. So formally, S might not
be an interpretation of I. What problems might arise? I'm thinking of an
example like ...

Axioms
    ? [X] : p(X)
HI
    D = {a}
    F = id
    P = p(a) == true
But ...
    S = {p(sk)}

Here p(sk) |= ? [X] : p(X). Are there any weird cases where things break?
Can we say that an S that contains symbols not from the I really represents
a HI of I? Or only a HI of CNF(I), then lean on equisatisfiability to prove
that "if S |= I then HI |- I" where HI is somehow constructed from S?
```

Representation of FOF Finite Interpretations

Consider the following FOF problem from the TPTP Format for Finite Interpretations in the TPTP Quick Guide. It 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_of(john) = f ).

fof(someone_got_an_a,axiom,
    ? [H] :
      ( human(H)
      & grade_of(H) = a ) ).

fof(distinct_grades,axiom,
    a != f ).

fof(grades_not_human,axiom,
    ! [G] : ~ human(grade_of(G)) ).

fof(equality_lost,conjecture,
    ! [H1,H2] :
      ( ( human(H1)
        & human(H2)
        & created_equal(H1,H2) )
    <=> H1 = H2 ) ).
%------------------------------------------------------------------------------

A weakness of the format for the finite interpretation presented in the TPTP Format for Finite Interpretations in the TPTP Quick Guide is that the format relies on the formulae names (all the same) to link the three components of the interpretation, which is not allowed in the TPTP world. In the new format these are merged into a single annotated formula with the role interpretation:

%------------------------------------------------------------------------------
fof(equality_lost,interpretation,
    ( ! [X] : ( X = "a" | X = "f" | X = "john" | X = "gotA") 
    & ( a = "a"
      & f = "f"
      & john = "john"
      & grade_of("a") = "a"
      & grade_of("f") = "a"
      & grade_of("john") = "f"
      & grade_of("gotA") = "a" ) 
    & ( ~ human("a")
      & ~ human("f")
      & human("john")
      & human("gotA")
      & ~ created_equal("a","a")
      & ~ created_equal("a","f")
      & ~ created_equal("a","john")
      & ~ created_equal("a","gotA")
      & ~ created_equal("f","a")
      & ~ created_equal("f","f")
      & ~ created_equal("f","john")
      & ~ created_equal("f","gotA")
      & ~ created_equal("john","a")
      & ~ created_equal("john","f")
      & created_equal("john","john")
      & created_equal("john","gotA")
      & ~ created_equal("gotA","a")
      & ~ created_equal("gotA","f")
      & created_equal("gotA","john")
      & created_equal("gotA","gotA") ) ) ).
%------------------------------------------------------------------------------

Note how the use of "distinct object"s makes the domain elements distinct.

The consistency of the interpretation formula can be confirmed by Vampire.
The verification proof problem FOF_Finite.s.p can be proved by Vampire.

The parts of a single interpretation formula can be separated out at varying levels of granularity, using subroles. At a medium grained level the domain and mappings can be separated:

%------------------------------------------------------------------------------
fof(equality_lost_domain,interpretation-domain,
    ! [X] : ( X = "a" | X = "f" | X = "john" | X = "gotA") ).

fof(equality_lost_term_mappings,interpretation-mapping,
    ( 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-mapping,
    ( ~ 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") ).
%------------------------------------------------------------------------------

At a fine grained level the domain and mappings can be separated by symbol:

%------------------------------------------------------------------------------
fof(equality_lost_domain,interpretation-domain($i,$i),
    ! [X] : ( X = "a" | X = "f" | X = "john" | X = "gotA") ).

fof(equality_lost_a,interpretation-mapping(a,$i),
    a = "a" ).

fof(equality_lost_f,interpretation-mapping(f,$i),
    f = "f" ).

fof(equality_lost_john,interpretation-mapping(john,$i),
    john = "john" ).

fof(equality_lost_grade_of,interpretation-mapping(grade_of,$i),
    ( grade_of("a") = "a"
    & grade_of("f") = "a"
    & grade_of("john") = "f"
    & grade_of("gotA") = "a" ) ).

fof(equality_lost_human,interpretation-mapping(human,$o),
    ( ~ human("a")
    & ~ human("f")
    & human("john")
    & human("gotA") ).

fof(equality_lost_created_equal,interpretation-mapping(created_equal,$o),
    ( ~ 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") ).
%------------------------------------------------------------------------------

Representation of FOF Saturation Interpretations

The new format for interpretations can also be used for saturations that induce a set of Herbrand interpretations, by giving the saturation formulae the role interpretation-herbrand: (the -herbrand is optional but useful):

%------------------------------------------------------------------------------
cnf(c_0_15,interpretation-herbrand,
    ( created_equal(X1,X2) | ~ human(X1) | ~ human(X2) ) ).

cnf(c_0_16,interpretation-herbrand, ~ human(grade_of(X1)) ).

cnf(c_0_17,interpretation-herbrand, grade_of(esk3_0) = a ).

cnf(c_0_18,interpretation-herbrand, grade_of(john) = f ).

cnf(c_0_20,interpretation-herbrand,
    ( esk1_0 != esk2_0 | ~ human(esk1_0) | ~ human(esk2_0) ) ).

cnf(c_0_21,interpretation-herbrand,
    ( created_equal(esk1_0,esk2_0) | esk1_0 = esk2_0 ) ).

cnf(c_0_22,interpretation-herbrand, ( human(esk2_0) | esk1_0 = esk2_0 ) ).

cnf(c_0_23,interpretation-herbrand, ( human(esk1_0) | esk1_0 = esk2_0 ) ).

cnf(c_0_24,interpretation-herbrand, ~ human(a) ).

cnf(c_0_25,interpretation-herbrand, ~ human(f) ).

cnf(c_0_26,interpretation-herbrand, a != f ).

cnf(c_0_27,interpretation-herbrand, human(esk3_0) ).

cnf(c_0_28,interpretation-herbrand, human(john) ).
%------------------------------------------------------------------------------

(This saturation was created by E.)

The consistency of the interpretation formulae can be confirmed by Vampire.
The verification proof problem FOF_Saturation.s.p can be proved by E.

Representation of FOF Formulae Interpretations

The new format for interpretations can also be used for formulae that induce a set of Herbrand interpretations, by giving the formulae the role interpretation-herbrand (the -herbrand is optional but useful):

%------------------------------------------------------------------------------
fof(created_equal,interpretation-herbrand,
    ! [X0,X1] : ( created_equal(X0,X1) <=> $true ) ).

fof(human,interpretation-herbrand,
    ! [X0] : ( human(X0) <=> ( X0 != "f" & X0 != "a" ) ) ).

fof(john,interpretation-herbrand,
    ! [X0] : ( X0 = john <=> X0 = "john" ) ).

fof(grade_of,interpretation-herbrand,
    ! [X0,X1] :
      ( X0 = grade_of(X1)
    <=> ( ( X0 = "f" & X1 != "gotA" )
        | ( X0 = "a" & X1 = "gotA" ) ) ) ).

fof(f,interpretation-herbrand,
    ! [X0] : ( X0 = f <=> X0 = "f" ) ).

fof(a,interpretation-herbrand,
    ! [X0] : ( X0 = a <=> X0 = "a" ) ).
%------------------------------------------------------------------------------

(This set of formulae is a modified version of the Herbrand-formulae created by iProver.)

The consistency of the interpretation formulae can be confirmed by Vampire.
The verification proof problem FOF_Formulae.s.p can be proved by Vampire.

Representation of TFF/TXF Interpretations

The example of a finite FOF interpretation clearly points to the need for types. The problem would be better written as ...

%------------------------------------------------------------------------------
tff(human_type,type,      human: $tType ).
tff(cat_type,type,        cat: $tType ).
tff(jon_decl,type,        jon: human ).
tff(garfield_decl,type,   garfield: cat ).
tff(arlene_decl,type,     arlene: cat ).
tff(nermal_decl,type,     nermal: cat ).
tff(loves_decl,type,      loves: cat > cat ).
tff(owns_decl,type,       owns: ( human * cat ) > $o ).

tff(only_jon,axiom, ! [H: human] : H = jon ).

tff(only_garfield_and_arlene_and_nermal,axiom,
    ! [C: cat] : 
      ( C = garfield | C = arlene | C = nermal ) ).

tff(distinct_cats,axiom,
    ( garfield != arlene & arlene != nermal 
    & nermal != garfield ) ).

tff(jon_owns_garfield_not_arlene,axiom,
    ( owns(jon,garfield) & ~ owns(jon,arlene) ) ).

tff(all_cats_love_garfield,axiom,
    ! [C: cat] : ( loves(C) = garfield ) ).

tff(jon_owns_garfields_lovers,conjecture,
    ! [C: cat] :
      ( ( loves(C) = garfield & C != arlene ) 
       => owns(jon,C) ) ).
%------------------------------------------------------------------------------

... and a finite interpretation (a countermodel for the conjecture) is ...

%------------------------------------------------------------------------------
tff(human_type,type,      human: $tType ).
tff(cat_type,type,        cat: $tType ).
tff(jon_decl,type,        jon: human ).
tff(garfield_decl,type,   garfield: cat ).
tff(arlene_decl,type,     arlene: cat ).
tff(nermal_decl,type,     nermal: cat ).
tff(loves_decl,type,      loves: cat > cat ).
tff(owns_decl,type,       owns: ( human * cat ) > $o ).

%----Types of the domains
tff(d_human_type,type,    d_human: $tType ).
tff(d_cat_type,type,      d_cat: $tType ).
%----Types of the promotion functions
tff(d2human_decl,type,    d2human: d_human > human ).
tff(d2cat_decl,type,      d2cat: d_cat > cat ).
%----Types of the domain elements
tff(d_jon_decl,type,      d_jon: d_human ).
tff(d_garfield_decl,type, d_garfield: d_cat ).
tff(d_arlene_decl,type,   d_arlene: d_cat ).
tff(d_nermal_decl,type,   d_nermal: d_cat ).

tff(garfield,interpretation,
%----The domain for human is d_human
    ( ( ! [H: human] : ? [DH: d_human] : H = d2human(DH)
%----The d_human elements are {d_jon}
      & ! [DH: d_human] : ( DH = d_jon )
%----The type-promoter is a bijection
      & ! [DH1: d_human,DH2: d_human] :
          ( d2human(DH1) = d2human(DH2) => DH1 = DH2 )
%----The domain for cat is d_cat
      & ! [C: cat] : ? [DC: d_cat] : C = d2cat(DC)
%----The d_cat elements are {d_garfield,d_arlene,d_nermal}
      & ! [DC: d_cat]: 
          ( DC = d_garfield | DC = d_arlene | DC = d_nermal )
      & $distinct(d_garfield,d_arlene,d_nermal)
%----The type-promoter is a bijection
      & ! [DC1: d_cat,DC2: d_cat] : 
          ( d2cat(DC1) = d2cat(DC2) => DC1 = DC2 ) )
%----Interpret terms via the type-promoted domain
    & ( jon = d2human(d_jon)
      & garfield = d2cat(d_garfield)
      & arlene = d2cat(d_arlene)
      & nermal = d2cat(d_nermal)
      & loves(d2cat(d_garfield)) = d2cat(d_garfield)
      & loves(d2cat(d_arlene)) = d2cat(d_garfield)
      & loves(d2cat(d_nermal)) = d2cat(d_garfield) )
%----Interpret atoms as true or false
    & ( owns(d2human(d_jon),d2cat(d_garfield))
      & ~ owns(d2human(d_jon),d2cat(d_arlene))
      & ~ owns(d2human(d_jon),d2cat(d_nermal)) ) ) ).
%------------------------------------------------------------------------------

The consistency of the interpretation formula can be confirmed by Vampire.
The verification proof problem TFF_Finite.s.p can be proved by Vampire.

The parts of a single interpretation formula can be separated out at varying levels of granularity, using subroles. At a medium grained level the domain and mappings can be separated:

%------------------------------------------------------------------------------
tff(human_type,type,      human: $tType ).
tff(cat_type,type,        cat: $tType ).
tff(jon_decl,type,        jon: human ).
tff(garfield_decl,type,   garfield: cat ).
tff(arlene_decl,type,     arlene: cat ).
tff(nermal_decl,type,     nermal: cat ).
tff(loves_decl,type,      loves: cat > cat ).
tff(owns_decl,type,       owns: ( human * cat ) > $o ).

tff(d_human_type,type,    d_human: $tType ).
tff(d_cat_type,type,      d_cat: $tType ).
tff(d2human_decl,type,    d2human: d_human > human ).
tff(d2cat_decl,type,      d2cat: d_cat > cat ).
tff(d_jon_decl,type,      d_jon: d_human ).
tff(d_garfield_decl,type, d_garfield: d_cat ).
tff(d_arlene_decl,type,   d_arlene: d_cat ).
tff(d_nermal_decl,type,   d_nermal: d_cat ).

tff(garfield_domains,interpretation-domain,
    ( ! [H: human] : ? [DH: d_human] : H = d2human(DH)
    & ! [DH: d_human] : ( DH = d_jon )
    & ! [DH1: d_human,DH2: d_human] :
        ( d2human(DH1) = d2human(DH2) => DH1 = DH2 )
    & ! [C: cat] : ? [DC: d_cat] : C = d2cat(DC)
    & ! [DC: d_cat]: 
        ( DC = d_garfield | DC = d_arlene | DC = d_nermal )
    & $distinct(d_garfield,d_arlene,d_nermal)
    & ! [DC1: d_cat,DC2: d_cat] : 
        ( d2cat(DC1) = d2cat(DC2) => DC1 = DC2 ) ) ).

tff(garfield_mappings,interpretation-mapping,
    ( ( jon = d2human(d_jon)
      & garfield = d2cat(d_garfield)
      & arlene = d2cat(d_arlene)
      & nermal = d2cat(d_nermal)
      & loves(d2cat(d_garfield)) = d2cat(d_garfield)
      & loves(d2cat(d_arlene)) = d2cat(d_garfield)
      & loves(d2cat(d_nermal)) = d2cat(d_garfield) )
    & ( owns(d2human(d_jon),d2cat(d_garfield))
      & ~ owns(d2human(d_jon),d2cat(d_arlene))
      & ~ owns(d2human(d_jon),d2cat(d_nermal)) ) ) ).
%------------------------------------------------------------------------------

At a fine grained level the individual symbol mappings can be separated. The types of the symbols and the types of the domain must be given.

%------------------------------------------------------------------------------
tff(human_type,type,      human: $tType ).
tff(cat_type,type,        cat: $tType ).
tff(jon_decl,type,        jon: human ).
tff(garfield_decl,type,   garfield: cat ).
tff(arlene_decl,type,     arlene: cat ).
tff(nermal_decl,type,     nermal: cat ).
tff(loves_decl,type,      loves: cat > cat ).
tff(owns_decl,type,       owns: ( human * cat ) > $o ).

tff(d_human_type,type,    d_human: $tType ).
tff(d_cat_type,type,      d_cat: $tType ).
tff(d2human_decl,type,    d2human: d_human > human ).
tff(d2cat_decl,type,      d2cat: d_cat > cat ).
tff(d_jon_decl,type,      d_jon: d_human ).
tff(d_garfield_decl,type, d_garfield: d_cat ).
tff(d_arlene_decl,type,   d_arlene: d_cat ).
tff(d_nermal_decl,type,   d_nermal: d_cat ).

tff(garfield_domain_human,interpretation-domain(human,d_human),
    ( ! [H: human] : ? [DH: d_human] : H = d2human(DH)
    & ! [DH: d_human] : ( DH = d_jon )
    & ! [DH1: d_human,DH2: d_human] :
        ( d2human(DH1) = d2human(DH2) => DH1 = DH2 ) ) ).

tff(garfield_domain_cat,interpretation-domain(cat,d_cat),
    ( ! [C: cat] : ? [DC: d_cat] : C = d2cat(DC)
    & ! [DC: d_cat]: 
        ( DC = d_garfield | DC = d_arlene | DC = d_nermal )
    & $distinct(d_garfield,d_arlene,d_nermal)
    & ! [DC1: d_cat,DC2: d_cat] : 
        ( d2cat(DC1) = d2cat(DC2) => DC1 = DC2 ) ) ).

tff(garfield_mapping_jon,interpretation-mapping(jon,d_human),
    jon = d2human(d_jon) ).

tff(garfield_mapping_garfield,interpretation-mapping(garfied,d_cat),
    garfield = d2cat(d_garfield) ).

tff(garfield_mapping_arlene,interpretation-mapping(arlene,d_cat),
    arlene = d2cat(d_arlene) ).

tff(garfield_mapping_nermal,interpretation-mapping(nermal,d_cat),
    nermal = d2cat(d_nermal) ).

tff(garfield_mapping_loves,interpretation-mapping(loves,d_cat),
    ( loves(d2cat(d_garfield)) = d2cat(d_garfield)
    & loves(d2cat(d_arlene)) = d2cat(d_garfield)
    & loves(d2cat(d_nermal)) = d2cat(d_garfield) ) ).

tff(garfield_mapping_owns,interpretation-mapping(owns,$o),
    ( owns(d2human(d_jon),d2cat(d_garfield))
    & ~ owns(d2human(d_jon),d2cat(d_arlene))
    & ~ owns(d2human(d_jon),d2cat(d_nermal)) ) ).
%------------------------------------------------------------------------------

Representation of TXF Interpretations

Representation of THF Interpretations

The following TH0 problem is CounterSatisfiable, i.e., there is a model for the axioms and negated conjecture.

%------------------------------------------------------------------------------
thf(beverage_decl,type,   beverage: $tType ).
thf(syrup_decl,type,      syrup: $tType ).
thf(coffee_type,type,     coffee: beverage ).
thf(mix_type,type,        mix: beverage > syrup > beverage ).
thf(heat_type,type,       heat: beverage > beverage ).
thf(heated_mix_type,type, heated_mix: beverage > syrup > beverage ).
thf(hot_type,type,        hot: beverage > $o ).

thf(heated_mix,axiom,
    ( heated_mix
    = ( ^ [B: beverage,S: syrup] : ( heat @ ( mix @ B @ S ) ) ) ) ).

thf(hot_mixture,axiom,
    ! [B: beverage,S: syrup] : ( hot @ ( heated_mix @ B @ S ) ) ).

thf(heated_coffee_mix,axiom,
    ! [S: syrup] : ( ( heated_mix @ coffee @ S ) = coffee ) ).

thf(hot_coffee,conjecture,
    ? [Mixture: syrup > beverage] :
      ~ ? [S: syrup] :
          ( ( ( Mixture @ S ) = coffee )
          & ( hot @ ( Mixture @ S ) ) ) ).
%------------------------------------------------------------------------------

Here's a finite model (that I found using Nitpick) ...

%------------------------------------------------------------------------------
thf(beverage_decl,type,   beverage: $tType ).
thf(syrup_decl,type,      syrup: $tType ).
thf(coffee_type,type,     coffee: beverage ).
thf(mix_type,type,        mix: beverage > syrup > beverage ).
thf(heat_type,type,       heat: beverage > beverage ).
thf(heated_mix_type,type, heated_mix: beverage > syrup > beverage ).
thf(hot_type,type,        hot: beverage > $o ).

thf(d_beverage_decl,type, d_beverage: $tType ).
thf(d_syrup_decl,type,    d_syrup: $tType ).
thf(d2beverage_type,type, d2beverage: d_beverage > beverage ).
thf(d2syrup_type,type,    d2syrup: d_syrup > syrup ).
thf(d_coffee_type,type,   d_coffee: d_beverage ).
thf(d_date_type,type,     d_date: d_syrup ).

thf(hot_coffee,interpretation,
    ( ( ! [B: beverage] : ? [DB: d_beverage] : ( B = ( d2beverage @ DB ) )
      & ! [DB: d_beverage] : ( DB = d_coffee )
      & ! [DB1: d_beverage,DB2: d_beverage] :
          ( ( ( d2beverage @ DB1 ) = ( d2beverage @ DB2 ) ) => ( DB1 = DB2 ) )
      & ! [S: syrup] : ? [DS: d_syrup] : ( S = ( d2syrup @ DS ) )
      & ! [DS: d_syrup] : ( DS = d_date )
      & ! [DS1: d_syrup,DS2: d_syrup] :
          ( ( ( d2syrup @ DS1 ) = ( d2syrup @ DS2 ) ) => ( DS1 = DS2 ) ) )
    & ( ( ( mix @ ( d2beverage @ d_coffee ) @ ( d2syrup @ d_date ) ) 
        = ( d2beverage @ d_coffee ) )
      & ( ( heat @ ( d2beverage @ d_coffee ) ) 
        = ( d2beverage @ d_coffee ) )
      & ( ( heated_mix @ ( d2beverage @ d_coffee ) @ ( d2syrup @ d_date ) ) 
        = ( d2beverage @ d_coffee ) )
      & ( hot @ ( d2beverage @ d_coffee ) ) ) ) ).
%------------------------------------------------------------------------------

The verification proof problem THF_Finite.s.p can be proved by Vampire.

Representation of Infinite Interpretations

Consider the following TFF example that requires an integer size domain ...

%------------------------------------------------------------------------------
tff(person_type,type,        person: $tType ).
tff(bob_decl,type,           bob: person ).
tff(child_of_decl,type,      child_of: person > person ).
tff(is_descendant_decl,type, is_descendant: (person * person) > $o ).

tff(descendents_different,axiom,
    ! [A: person,D: person] : 
      ( is_descendant(A,D) => ( A != D ) ) ).

tff(descendent_transitive,axiom,
    ! [A: person,C: person,G: person] :
      ( ( is_descendant(A,C) & is_descendant(C,G) ) 
     => is_descendant(A,G) ) ).

tff(child_is_descendant,axiom,
    ! [P: person] : is_descendant(P,child_of(P)) ).

tff(all_have_child,axiom,
    ! [P: person] : ? [C: person] : C = child_of(P) ).
%------------------------------------------------------------------------------

Here's a model using closed terms representing Peano numbers as the domain elements ...

%------------------------------------------------------------------------------
tff(person_type,type,         person: $tType ).
tff(bob_decl,type,            bob: person ).
tff(child_of_decl,type,       child_of: person > person ).
tff(is_descendant_decl,type,  is_descendant: ( person * person ) > $o ).

tff(peano_type,type,          peano: $tType).
tff(zero_decl,type,           zero: peano ).
tff(s_decl,type,              s: peano > peano ).
tff(peano2person_decl,type,   peano2person: peano > person ).
tff(peano_less_decl,type,     peano_less: ( peano * peano ) > $o ).

tff(people,interpretation,
%----Domain for type person is the Peano numbers
    ( ( ! [P: person] : ? [I: peano] : ( P = peano2person(I) )
      & ! [I: peano] : ( I = zero | ? [P: peano] : I = s(P) )
%----The type promoter is a bijection (injective and surjective)
      & ! [I1: peano,I2: peano] :
          ( peano2person(I1) = peano2person(I2) => I1 = I2 )
%----Relationships between Peano numbers
      & ! [I1: peano,I2: peano,I3: peano] :
          ( peano_less(I1,s(I1))
          & ( ( peano_less(I1,I2) & peano_less(I2,I3) )
           => peano_less(I1,I3) )
          & ( peano_less(I1,I2)
           => I1 != I2 ) ) )
%----Mapping people to Peano numbers
    & ( bob = peano2person(zero)
      & ! [I: peano] :
          child_of(peano2person(I)) = peano2person(s(I)) )
%----Interpretation of descendancy
    & ( ! [A: peano,D: peano] :
          ( is_descendant(peano2person(A),peano2person(D))
        <=> peano_less(A,D) ) ) ) ).
%------------------------------------------------------------------------------

The consistency of the interpretation formula cannot be confirmed by any ATP system I have.

The verification proof problem TFF_Peano.s.p can be proved by Vampire.

Here's a model using the integers for the domain elements ...

%------------------------------------------------------------------------------
tff(person_type,type,        person: $tType ).
tff(bob_decl,type,           bob: person ).
tff(child_of_decl,type,      child_of: person > person ).
tff(is_descendant_decl,type, is_descendant: ( person * person ) > $o ).

tff(int2person_decl,type,    int2person: $int > person ).

tff(people,interpretation,
%----Domain for type person is the integers
    ( ( ! [P: person] : ? [I: $int] : int2person(I) = P
%----The type promoter is a bijection (injective and surjective)
      & ! [I1: $int,I2: $int] : 
          ( int2person(I1) = int2person(I2) => I1 = I2 ) )
%----Mapping people to integers. Note that Bob's ancestors will be interpreted 
%----as negative integers.
    & ( bob = int2person(0)
      & ! [I: $int] : child_of(int2person(I)) = int2person($sum(I,1)) )
%----Interpretation of descendancy
    & ! [A: $int,D: $int] : 
        ( is_descendant(int2person(A),int2person(D)) <=> $less(A,D) ) ) ).
%------------------------------------------------------------------------------

The consistency of the interpretation formula cannot be confirmed by any ATP system I have.

TFF_Integer.s.p is the proof problem to verify the countermodel.
The consistency of the proof problem's axioms cannot be confirmed by any ATP system I have.
The verification proof problem can be proved by Vampire.

Finite and infinite domains can be mixed. Here's a problem that can be proven by Vampire. With the conjecture modified as below, it has a countermodel with integer domains for the X and Y positions (mimicing the logic), and a finite domain for the Z level.

%------------------------------------------------------------------------------
tff(level_type,type,  level: $tType).
tff(ground_decl,type, ground: level).
tff(middle_decl,type, middle: level).
tff(top_decl,type,    top: level).
tff(space_decl,type,  space: level).

tff(possible_position_decl,type,
    possible_position: ( $int * $int * level ) > $o ).

tff(only_four_distinct_levels,axiom,
    ( ! [Z: level] :
        ( ( Z = ground )
        | ( Z = middle )
        | ( Z = top )
        | ( Z = space ) )
    & ( ground != middle )
    & ( ground != top )
    & ( ground != space )
    & ( middle != top )
    & ( middle != space )
    & ( top != space ) ) ).
%    & $distinct(ground,middle,top,space) ) ).

tff(start_at_origin,axiom,
    possible_position(0,0,ground) ).

tff(move_X,axiom,
    ! [X: $int,Y: $int,Z: level] :
      ( possible_position(X,Y,Z)
     => ( possible_position($difference(X,1),Y,Z)
        & possible_position($sum(X,1),Y,Z) ) ) ).

tff(move_Y,axiom,
    ! [X: $int,Y: $int,Z: level] :
      ( possible_position(X,Y,Z)
     => ( possible_position(X,$difference(Y,1),Z)
        & possible_position(X,$sum(Y,1),Z) ) ) ).

tff(move_Z,axiom,
    ! [X: $int,Y: $int] :
      ( ( possible_position(X,Y,ground)
       => possible_position(X,Y,middle) )
      & ( possible_position(X,Y,middle)
       => ( possible_position(X,Y,ground)
          & possible_position(X,Y,top) ) )
      & ( possible_position(X,Y,top)
       => possible_position(X,Y,middle) ) ) ).

tff(can_fly,conjecture,
    possible_position(3,-5,space) ).
%------------------------------------------------------------------------------

Here's the countermodel ...

%------------------------------------------------------------------------------
tff(level_type,type,level: $tType).
tff(ground_decl,type,ground: level).
tff(middle_decl,type,middle: level).
tff(top_decl,type,top: level).
tff(space_decl,type,space: level).
tff(possible_position_decl,type,
    possible_position: ($int * $int * level) > $o ).

tff(d_level_type,type,d_level: $tType).
tff(d_ground_decl,type,d_ground: d_level).
tff(d_middle_decl,type,d_middle: d_level).
tff(d_top_decl,type,d_top: d_level).
tff(d_space_decl,type,d_space: d_level).
tff(d2level_decl,type,d2level: d_level > level).

tff(drone,interpretation,
    ( ( ! [L: level] : ? [DL: d_level] : L = d2level(DL)
      & ! [Z: d_level] : ( Z = d_ground | Z = d_middle | Z = d_top | Z = d_space )
      & ( d_ground != d_middle
        & d_ground != d_top
        & d_ground != d_space
        & d_middle != d_top
        & d_middle != d_space
        & d_top != d_space )
%     & $distinct(ground,middle,top,space)
      & ! [DL1: d_level,DL2: d_level] : ( d2level(DL1) = d2level(DL2) => DL1 = DL2 ) )
    & ( ground = d2level(d_ground)
      & middle = d2level(d_middle)
      & top = d2level(d_top)
      & space = d2level(d_space) )
    & ! [X: $int,Y: $int] :
        ( possible_position(X,Y,d2level(d_ground))
        & possible_position(X,Y,d2level(d_middle))
        & possible_position(X,Y,d2level(d_top))
        & ~ possible_position(X,Y,d2level(d_space)) ) ) ).
%------------------------------------------------------------------------------

The consistency of the interpretation formula can be confirmed by Z3 (and not by Vampire).
The verification proof problem TFF_Mixed.s.p can be proved by Vampire.

Representation of Kripke Interpretations

This can be done in only a typed logic.

Record world information in interpretation-formulas, using a new defined type $world, a new defined predicate $in_world with type ($world * $o) > $o, a new defined predicate $accessible_world with type ($world * $world) > $o, and a new defined constant $local_world with type $world. Syntactically distinct constants of type $world are known to be unequal. The interpretation in a world is represented as above, with guards used to specify the worlds in which the interpretation is used.

The logic specification of the problem is included as a comment, because the interpretation-formulae under-specify the logic, e.g., it's usually not possible to see whether an interpretation was meant to exemplify a S5 logic specification or a K logic specification - in both cases the concrete model could interpret the accessibility relation as equivalence relation (this is required for S5 but it is also OK for K).

Representation of Finite-Finite Kripke Interpretations - Global Axioms

Here's a non-theorem. Note that there are only global axioms and a local conjecture, which is the standard for satisfiability checking with Kripke semantics.

%------------------------------------------------------------------------------
tff(semantics,logic,
    $alethic_modal ==
      [ $domains == $constant,
        $designation == $rigid,
        $terms == $local,
        $modalities == $modal_system_M ] ).

tff(person_decl,type,person: $tType).
tff(product_decl,type,product: $tType).
tff(alex_decl,type,alex: person).
tff(chris_decl,type,chris: person).
tff(leo_decl,type,leo: product).
tff(work_hard_decl,type,work_hard: (person * product) > $o).
tff(gets_rich_decl,type,gets_rich: person > $o).

%----If there is a product that a person works hard on, then 
%----it's possible that the person will get rich.
tff(work_hard_to_get_rich,axiom,
    ! [P: person] :
      ( ? [R: product] : work_hard(P,R)
     => ( {$possible} @ (gets_rich(P)) ) ) ).

%----Nobody necessarily gets rich.
tff(not_all_get_rich,axiom,
    ~ ? [P: person] : ({$necessary} @ (gets_rich(P)) ) ).

%----Alex and Chris work hard on Leo-III.
tff(alex_works_on_leo,axiom,
    work_hard(alex,leo) ).

tff(chris_works_on_leo,axiom,
    work_hard(chris,leo) ).

%----Chris is not Alex
tff(chris_not_alex,axiom,
    chris != alex ).

%----It's possible that Alex gets rich but Chris does not.
tff(only_alex_gets_rich,conjecture,
    ( {$possible} @ (gets_rich(alex) & ~ gets_rich(chris)) ) ).
%------------------------------------------------------------------------------

After using NTF2THF to embed the problem into TH0, Nitpick finds a model with a finite number of worlds each of which has a finite domain (hence a "Finite-Finite Kripke Interpretation") that I converted by hand into TPTP format ...

%------------------------------------------------------------------------------
tff(semantics,logic,
    $alethic_modal ==
      [ $domains == $constant,
        $designation == $rigid,
        $terms == $local,
        $modalities == $modal_system_M ] ).

%----Declarations to fool Vampire when processing this file directly
% tff('$world_type',type,$world: $tType).
% tff('$local_world_decl',type,$local_world: $world).
% tff('$accessible_world_decl',type,$accessible_world: ($world * $world) > $o).
% tff('$in_world_decl',type,$in_world: ($world * $o) > $o).

tff(person_decl,type,    person: $tType).
tff(product_decl,type,   product: $tType).
tff(alex_decl,type,      alex: person).
tff(chris_decl,type,     chris: person).
tff(leo_decl,type,       leo: product).
tff(work_hard_decl,type, work_hard: (person * product) > $o).
tff(gets_rich_decl,type, gets_rich: person > $o).

tff(d_person_type,type,  d_person: $tType).
tff(d2person_decl,type,  d2person: d_person > person ).
tff(d_alex_decl,type,    d_alex: d_person).
tff(d_chris_decl,type,   d_chris: d_person).
tff(d_product_type,type, d_product: $tType).
tff(d2product_decl,type, d2product: d_product > product ).
tff(d_leo_decl,type,     d_leo: d_product).

tff(w1_decl,type,w1:     $world).
tff(w2_decl,type,w2:     $world).

tff(leo_workers,interpretation,
    ( ( ! [W: $world] : ( W = w1 | W = w2 )
      & $distinct(w1,w2)
      & $local_world = w2
      & $accessible_world(w1,w1)     %----Logic is M
      & $accessible_world(w2,w2)
      & $accessible_world(w1,w2) 
      & $accessible_world(w2,w1) )
    & $in_world(w1,
        ( ! [P: person] : ? [DP: d_person] : P = d2person(DP)
        & ! [DP: d_person] : ( DP = d_alex | DP = d_chris )
        & $distinct(d_alex,d_chris)
        & ? [DP: d_person] : ( DP = d_alex )
        & ? [DP: d_person] : ( DP = d_chris )
        & ! [DP1: d_person,DP2: d_person] : 
            ( d2person(DP1) = d2person(DP2) => DP1 = DP2 )
        & ! [P: product] : ? [DP: d_product] : P = d2product(DP)
        & ! [DP: d_product] : DP = d_leo
        & ? [DP: d_product] : DP = d_leo
        & ! [DP1: d_product,DP2: d_product] :
            ( d2product(DP1) = d2product(DP2) => DP1 = DP2 ) )
      & ( alex = d2person(d_alex)
        & chris = d2person(d_chris)
        & leo = d2product(d_leo) )
      & ( work_hard(d2person(d_alex),d2product(d_leo))
        & work_hard(d2person(d_chris),d2product(d_leo))
        & gets_rich(d2person(d_alex))
        & gets_rich(d2person(d_chris)) ) )
    & $in_world(w2,
        ( ! [P: person] : ? [DP: d_person] : P = d2person(DP)
        & ! [DP: d_person] : ( DP = d_alex | DP = d_chris )
        & $distinct(d_alex,d_chris)
        & ? [DP: d_person] : ( DP = d_alex )
        & ? [DP: d_person] : ( DP = d_chris )
        & ! [DP1: d_person,DP2: d_person] : 
            ( d2person(DP1) = d2person(DP2) => DP1 = DP2 )
        & ! [P: product] : ? [DP: d_product] : P = d2product(DP)
        & ! [DP: d_product] : DP = d_leo
        & ? [DP: d_product] : DP = d_leo
        & ! [DP1: d_product,DP2: d_product] :
            ( d2product(DP1) = d2product(DP2) => DP1 = DP2 )
        & ( alex = d2person(d_alex)
          & chris = d2person(d_chris)
          & leo = d2product(d_leo) )
        & ( work_hard(d2person(d_alex),d2product(d_leo))
          & work_hard(d2person(d_chris),d2product(d_leo))
          & ~ gets_rich(d2person(d_alex))
          & ~ gets_rich(d2person(d_chris)) ) ) ) ) ).
%------------------------------------------------------------------------------

The consistency of the interpretation formula can be confirmed by Vampire.
The NXF verification proof problem NXF_Finite-Finite-Global.s.p can be proved by Leo-III.

Representation of Finite-Finite Kripke Interpretations - Global and Local Axioms

Here's a problem that can be proven by Leo-III. Note that it has both global and local axioms (contrary to the standard case for proving, where all the axioms are global). With the conjecture modified as below, it has a countermodel with a finite number of worlds each of which has a finite domain ...

%------------------------------------------------------------------------------
tff(semantics,logic,
    $alethic_modal == 
      [ $domains == $constant,
        $designation == $rigid,
        $terms == $local,
        $modalities == $modal_system_M ] ).

tff(fruit_type,type,   fruit: $tType).
tff(apple_decl,type,   apple: fruit).
tff(banana_decl,type,  banana: fruit).
tff(healthy_decl,type, healthy: fruit > $o).
tff(rotten_decl,type,  rotten: fruit > $o).

tff(apple_not_banana,axiom,
    apple != banana ).

tff(necessary_healthy_fruit_everywhere,axiom,
    ! [F: fruit] : ( {$necessary} @ (healthy(F)) ) ).

tff(fruit_possibly_not_rotten,axiom,
    ! [F: fruit] : ( {$possible} @ (~ rotten(F)) ) ).

tff(rotten_banana_here,axiom-local,
    rotten(banana) ).

tff(not_true,conjecture,
    ( {$necessary} @ 
      (( healthy(apple)
       & ~ rotten(banana) )) ) ).
%------------------------------------------------------------------------------

After using NTF2THF to embed the problem into TH0, Nitpick finds a countermodel that I converted by hand into TPTP format ...

%------------------------------------------------------------------------------
tff(semantics,logic,
    $alethic_modal ==
      [ $domains == $constant,
        $designation == $rigid,
        $terms == $local,
        $modalities == $modal_system_M ] ).

%----Declarations to fool Vampire when processing this file directly
% tff('$world_type',type,$world: $tType).
% tff('$local_world_decl',type,$local_world: $world).
% tff('$accessible_world_decl',type,$accessible_world: ($world * $world) > $o).
% tff('$in_world_decl',type,$in_world: ($world * $o) > $o).

tff(fruit_type,type,fruit: $tType).
tff(apple_decl,type,apple: fruit).
tff(banana_decl,type,banana: fruit).
tff(healthy_decl,type,healthy: fruit > $o).
tff(rotten_decl,type,rotten: fruit > $o).

tff(d_fruit_type,type,d_fruit: $tType).
tff(d2fruit_decl,type, d2fruit: d_fruit > fruit ).
tff(d_apple_decl,type,d_apple: d_fruit).
tff(d_banana_decl,type,d_banana: d_fruit).

tff(w1_decl,type,w1: $world).
tff(w2_decl,type,w2: $world).

tff(fruity_worlds,interpretation,
    ( ( ! [W: $world] : ( W = w1 | W = w2 )
      & $local_world = w1
      & $accessible_world(w1,w1)     %----Logic is M
      & $accessible_world(w2,w2)
      & $accessible_world(w1,w2) )
    & $in_world(w1,
        ( ( ! [F: fruit] : ? [DF: d_fruit] : F = d2fruit(DF)
          & ! [DF: d_fruit] : ( DF = d_apple | DF = d_banana )
          & $distinct(d_apple,d_banana)
          & ? [DP: d_fruit] : ( DP = d_apple )
          & ? [DP: d_fruit] : ( DP = d_banana )
          & ! [DF1: d_fruit,DF2: d_fruit] : 
              ( d2fruit(DF1) = d2fruit(DF2) => DF1 = DF2 ) )
        & ( apple = d2fruit(d_apple)
          & banana = d2fruit(d_banana) )
        & ( healthy(d2fruit(d_apple))
          & healthy(d2fruit(d_banana))
          & ~ rotten(d2fruit(d_apple))
          & rotten(d2fruit(d_banana)) ) ) )
    & $in_world(w2,
        ( ( ! [F: fruit] : ? [DF: d_fruit] : F = d2fruit(DF)
          & ! [DF: d_fruit] : ( DF = d_apple | DF = d_banana )
          & $distinct(d_apple,d_banana)
          & ? [DP: d_fruit] : ( DP = d_apple )
          & ? [DP: d_fruit] : ( DP = d_banana )
          & ! [DF1: d_fruit,DF2: d_fruit] : 
              ( d2fruit(DF1) = d2fruit(DF2) => DF1 = DF2 ) )
        & ( apple = d2fruit(d_apple)
          & banana = d2fruit(d_banana) )
        & ( healthy(d2fruit(d_apple))
          & healthy(d2fruit(d_banana))
          & ~ rotten(d2fruit(d_apple))
          & ~ rotten(d2fruit(d_banana)) ) ) ) ) ).
%------------------------------------------------------------------------------

The consistency of the interpretation formula can be confirmed by Vampire.

Representation of Finite-Infinite Kripke Interpretations

Here's a problem that can be proven by Leo-III. With the conjecture modified as below, it has a countermodel that requires (I think, at least it uses) only two worlds, and they have infinite domains because sequences of tosses are infinite and different sequences are unequal.

%------------------------------------------------------------------------------
tff(simple_spec,logic,
    $alethic_modal == [
      $constants == $rigid,
      $quantification == $constant,
      $modalities == $modal_system_S4 ] ).

tff(sequence_type,type,  sequence: $tType ).
tff(null_decl,type,      null: sequence ).
tff(toss_decl,type,      toss: sequence > sequence ).
tff(all_heads_decl,type, all_heads: sequence > $o ).

tff(different_sequences,axiom,
    ! [S: sequence] : 
      ( ( toss(S) != null )
      & ( toss(S) != S ) ) ).

tff(injection,axiom,
    ! [S1: sequence,S2: sequence] :
      ( ( toss(S1) = toss(S2) )
     => ( S1 = S2 ) ) ).

tff(all_heads_possible,axiom,
    ! [S: sequence] :
      ( all_heads(S)
     => ( {$possible} @ (all_heads(toss(S)) ) ) ) ).

tff(no_heads,axiom,
    all_heads(null) ).
          
tff(two_heads_necessary,conjecture,
    ( {$necessary} 
    @ (? [S: sequence] : 
         ( all_heads(S) 
         & all_heads(toss(S)) ) ) ).
%------------------------------------------------------------------------------

After using NTF2THF to embed the problem into TH0, Nitpick cannot find a countermodel ... as expected ... Nitpick can find only finite models. So I hand-rolled a countermodel. In the countermodel sequences of tosses are represented by integers, with the null sequence represented by 1. The encoding is easy to see in binary, reading the tosses left-to-right and the bits right-to-left. If the last bit is 0 a head was tossed, if 1 a tail was tossed: null = 1 = 0001, head = 2 = 0010, tail = 3 = 0011, head-head = 4 = 0100, head-tail = 5 = 0101, tail-head = 6 = 0110, tail-tail = 7 = 0111, head-head-head = 8 = 1000, head-head-tail = 9 = 1001, head-tail-head = 10 = 1010, head-tail-tail = 11 = 1011, tail-head-head = 12 = 1100, etc, etc. The local world tosses a sequence of heads, interpreted as integer domain elements that are powers of 2. The other world first tosses a tail, represented by 3, and then tosses all heads, interpreted as integer domain elements that are powers of 2 multiplied by 3. There is no definition of sequences interpreted as integer domain elements less or equal to 0, but they are not "all_heads".

%------------------------------------------------------------------------------
tff(simple_spec,logic,
    $alethic_modal == [
      $constants == $rigid,
      $quantification == $constant,
      $modalities == $modal_system_S4 ] ).

%----Declarations to fool Vampire when processing this file directly
% tff('$world_type',type,$world: $tType).
% tff('$local_world_decl',type,$local_world: $world).
% tff('$accessible_world_decl',type,$accessible_world: ($world * $world) > $o).
% tff('$in_world_decl',type,$in_world: ($world * $o) > $o).

tff(sequence_type,type, sequence: $tType ).
tff(null_decl,type, null: sequence ).
tff(toss_decl,type, toss: sequence > sequence ).
tff(all_heads_decl,type, all_heads: sequence > $o ).

tff(int2sequence_decl,type,int2sequence: $int > sequence).

tff(w1_decl,type,w1: $world).
tff(w2_decl,type,w2: $world).

tff(tossed_worlds,interpretation,
    ( ( ! [W: $world] : ( ( W = w1 ) | ( W = w2 ) )
      & $local_world = w1
      & $accessible_world(w1,w1)
      & $accessible_world(w2,w2)
      & $accessible_world(w1,w2) )
    & $in_world(w1,
%----The domain for type sequence is the integers
        ( ( ! [S: sequence] : ? [I: $int] : S = int2sequence(I)
%----The type promoter is a bijection
          & ! [X: $int,Y: $int] : 
              ( int2sequence(X) = int2sequence(Y) => X = Y ) )
        & ( null = int2sequence(1)
%----In world w1 the first toss is a head. This is redundant.
          & toss(int2sequence(1)) = int2sequence(2)
          & ! [I: $int] : 
              toss(int2sequence(I)) = int2sequence($product(I,2)) )
        & ( all_heads(int2sequence(1))
          & ! [I: $int] :
              ( all_heads(int2sequence(I))
            <=> ( $greatereq(I,2)
                & ( $remainder_e(I,2) = 0 )
                & all_heads(int2sequence($quotient_e(I,2))) ) ) ) ) )
    & $in_world(w2,
        ( ( ! [S: sequence] : ? [I: $int] : S = int2sequence(I)
          & ! [X: $int,Y: $int] : 
              ( int2sequence(X) = int2sequence(Y) => X = Y ) )
        & ( null = int2sequence(1)
%----In world w2 the first toss is a tail
          & toss(int2sequence(1)) = int2sequence(3)
          & ! [I: $int] : 
              ( I != 1
             => toss(int2sequence(I)) = int2sequence($product(I,2)) ) )
        & ( all_heads(int2sequence(1))
          & ! [I: $int] :
              ( all_heads(int2sequence(I))
            <=> ( $greatereq(I,2)
                & ( $remainder_e(I,2) = 0 )
                & all_heads(int2sequence($quotient_e(I,2))) ) ) ) ) ) ) ).

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

The consistency of the interpretation formula cannot be confirmed by any ATP system I have.

Representation of Infinite-Finite Kripke Interpretations

This example requires (I think) an infinite number of worlds. The interpretation in the local world will have an infinite domain, but all the other worlds' domains need only a single element (one of the domain elements from the local world). All the domain elements of the local world need to have a corresponding world with that domain element.

%------------------------------------------------------------------------------
tff(simple_spec,logic,
    $alethic_modal == [
      $constants == $rigid,
      $quantification == $constant,
      $modalities == $modal_system_M ] ).

tff(person_type,type, person: $tType).
tff(geoff_decl,type,  geoff: person).
tff(alive_decl,type,  alive: (person * $int) > $o).
tff(age_decl,type,    age: (person * $int) > $int).

tff(born_by_1961,axiom,
    ? [BirthYear: $int] :
      ( $lesseq(BirthYear,1961)
      & ! [PreBirthYear: $int] :
          ( $less(PreBirthYear,BirthYear)
         => ( ~ alive(geoff,PreBirthYear)
            & ( age(geoff,PreBirthYear) = -1 ) ) )
      & ! [FromBirthYear: $int] :
          ( $greatereq(FromBirthYear,BirthYear)
         => ( alive(geoff,FromBirthYear)
            & ( age(geoff,FromBirthYear) = $difference(FromBirthYear,BirthYear)) ) ) ) ).

tff(necessarily_alive_between,axiom,
    ! [StartYear: $int,EndYear: $int] :
      ( ( $less(StartYear,EndYear)
        & alive(geoff,StartYear)
        & alive(geoff,EndYear) )
     => ( {$necessary} 
        @ (! [BetweenYear: $int] :
             ( ( $greatereq(BetweenYear,StartYear)
               & $lesseq(BetweenYear,EndYear) )
            => alive(geoff,BetweenYear) )) ) ) ).

tff(necessarily_dead_after,axiom,
    ! [DeathYear: $int] :
      ( ( alive(geoff,DeathYear)
        & ~ alive(geoff,$sum(DeathYear,1)) )
     => ( {$necessary}
        @ (! [Year: $int] :
             ( $greater(Year,DeathYear)
            => ~ alive(geoff,Year) ) ) ) ) ).

tff(might_live_another_year,axiom,
    ! [Year: $int] :
      ( alive(geoff,Year)
     => ( {$possible} @ (alive(geoff,$sum(Year,1))) ) ) ).

%----Adding this should make the axioms contradictory
% tff(must_die,axiom,
%     {$necessary} @
%       ( ? [Year: $int] :
%           ( $greater(Year,1961)
%           & ~ alive(geoff,Year ) ) ).

%----This should be provable
% tff(might_live_long,conjecture,
%     {$possible} @
%       ( ? [Year: $int] :
%           ( age(geoff,Year) = 120
%           & alive(geoff,Year) ) ) ).
%------------------------------------------------------------------------------

Here's a model with an integer number of worlds.

%------------------------------------------------------------------------------
tff(simple_spec,logic,
    $alethic_modal == [
      $constants == $rigid,
      $quantification == $constant,
      $modalities == $modal_system_M ] ).

%----Declarations to fool Vampire when processing this file directly
% tff('$world_type',type,$world: $tType).
% tff('$local_world_decl',type,$local_world: $world).
% tff('$accessible_world_decl',type,$accessible_world: ($world * $world) > $o).
% tff('$in_world_decl',type,$in_world: ($world * $o) > $o).

tff(person_type,type, person: $tType).
tff(geoff_decl,type,geoff: person).
tff(alive_decl,type,alive: (person * $int) > $o).
tff(age_decl,type,age: (person * $int) > $int).

tff(d_person_type,type,d_person: $tType).
tff(d_geoff_decl,type,d_geoff: d_person).
tff(d2person_decl,type,d2person: d_person > person).

tff(int2world_decl,type,int2world: $int > $world ).

tff(long_live_geoff,interpretation,
%----An infinite number of worlds, numbered by naturals
    ( ( ! [I: $int] : ? [W: $world] : int2world(I) = W
%----The type promoter is a bijection (injective and surjective)
      & ! [I1: $int,I2: $int] : 
          ( int2world(I1) = int2world(I2) => I1 = I2 )
      & ! [W: $world] : ? [I: $int] : int2world(I) = W
%----Worlds can access themselves and greater indexed worlds (worlds in the future)
      & ! [P: $int,F: $int] : 
          ( $greatereq(F,P)
         => $accessible_world(int2world(P),int2world(F)) ) )

%----Worlds before 1961 all think geoff was born that year
    & ! [IW: $int] :
        ( $less(IW,1961)
       => $in_world(int2world(IW),
%----Only one domain element for person
            ( ! [P: person] : ? [DP: d_person] : P = d2person(DP)
            & ! [DP: d_person] : DP = d_geoff
            & ? [DP: d_person] : DP = d_geoff
%----The type promoter is a bijection (injective and surjective)
            & ! [X: d_person,Y: d_person] :
                ( d2person(X) = d2person(Y) => X = Y )
            & geoff = d2person(d_geoff)
%----Alive and age interpretation
            & ! [Y: $int] :
                ( $less(Y,IW)
               => ( ~ alive(d2person(d_geoff),Y)
                  & age(d2person(d_geoff),Y) = -1 ) )
            & alive(d2person(d_geoff),IW)
            & age(d2person(d_geoff),IW) = 0
            & ! [Y: $int] :
                ( $greater(Y,IW)
               => ( alive(d2person(d_geoff),Y)
                  & age(d2person(d_geoff),Y) = $difference(Y,IW) ) ) ) )

%----Worlds from 1961 know geoff was born in 1961. geoff lives forever!
    & ! [IW: $int] :
        ( $greatereq(IW,1961)
       => $in_world(int2world(IW),
            ( ! [P: person] : ? [DP: d_person] : P = d2person(DP)
            & ! [DP: d_person] : DP = d_geoff
            & ? [DP: d_person] : DP = d_geoff
            & ! [X: d_person,Y: d_person] :
                ( d2person(X) = d2person(Y) => X = Y )
            & geoff = d2person(d_geoff)
            & ! [Y: $int] :
                ( ( $less(Y,1961)
                 => ( ~ alive(d2person(d_geoff),Y)
                    & age(d2person(d_geoff),Y) = -1 ) )
                & ( ( $greatereq(Y,1961)
                    & $less(Y,IW) )
                 => ( alive(d2person(d_geoff),Y)
                    & age(d2person(d_geoff),Y) = $difference(Y,1961) ) ) )
            & alive(d2person(d_geoff),IW)
            & age(d2person(d_geoff),IW) = $difference(IW,1961)
            & ! [Y: $int] :
                ( $greater(Y,IW)
               => ( alive(d2person(d_geoff),Y)
                  & age(d2person(d_geoff),Y) = $difference(Y,1961) ) ) ) ) ) ) ) ).

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

The consistency of the interpretation formula cannot be confirmed by any ATP system I have.

Representation of Infinite-Infinite Kripke Interpretations

Here's a problem that I think should be provable, but none of the ATP systems I know can (after conversion to TH0, Leo-III does not have the arithmetic power, E, Vampire, and Zipperposition don't do arithmetic (at least in THF), cvc5 gives parse error). With the conjecture commented out as below, the axioms have a an Infinite-Infinite model (I think).

%------------------------------------------------------------------------------
tff(simple_spec,logic,
    $alethic_modal == [
      $constants == $flexible,
      $quantification == $varying,
      $modalities == $modal_system_M ] ).

tff(person_type,type, person: $tType).
tff(geoff_decl,type,  geoff: person).
tff(like_decl,type,   like: person > $o).
tff(id_of_decl,type,  id_of: person > $int).

tff(like_exactly_one_person,axiom,
    ? [P: person] :
      ( like(P)
      & ! [OP: person] :
          ( like(OP)
         => ( OP = P ) ) ) ).

%----Infinite people here. The RHS of the conjunction limits it to an integer 
%----number of people.
tff(infinite_people,axiom-local,
    ! [I: $int] : 
      ( $greatereq(I,0)
     => ( ? [P: person] : id_of(P) = I
        & ! [P1: person,P2: person] : 
            ( ( id_of(P1) = id_of(P2) )
           => ( P1 = P2 ) ) ) ) ).

tff(like_geoff_here,axiom-local,
    like(geoff) ).

tff(like_all,axiom-local,
    ! [X: person] : ( {$possible} @ (like(X)) ) ).
%------------------------------------------------------------------------------

Here's a model in which there are an infinite number of worlds - one for each integer numbered year, an infinite number of ages as integers, and just one person in each world.

%------------------------------------------------------------------------------
tff(simple_spec,logic,
    $alethic_modal == [
      $constants == $flexible,
      $quantification == $varying,
      $modalities == $modal_system_M ] ).

%----Declarations to fool Vampire when processing this file directly
% tff('$world_type',type,$world: $tType).
% tff('$local_world_decl',type,$local_world: $world).
% tff('$accessible_world_decl',type,$accessible_world: ($world * $world) > $o).
% tff('$in_world_decl',type,$in_world: ($world * $o) > $o).

tff(person_type,type,person: $tType).
tff(geoff_decl,type,geoff: person).
tff(like_decl,type,like: person > $o).
tff(id_of_decl,type,id_of: person > $int).

tff(int2person_decl,type, int2person: $int > person ).

tff(int2world_decl,type,int2world: $int > $world ).

tff(like_geoff,interpretation,
%----An infinite number of worlds, numbered by naturals
    ( ( ! [I: $int] : 
          ( $greatereq(I,0)
         => ? [W: $world] : int2world(I) = W )
      & $local_world = int2world(0)
%----The type promoter is a bijection (injective and surjective)
      & ! [I1: $int,I2: $int] : 
          ( ( int2world(I1) = int2world(I2) ) => ( I1 = I2 ) )
      & ! [W: $world] : ? [I: $int] : int2world(I) = W
%----World 0 can access itself (system T)
      & $accessible_world(int2world(0),int2world(0))
%----World 0 can access all other worlds
      & ! [I: $int] : 
          ( $greater(I,0)
         => $accessible_world(int2world(0),int2world(I)) ) )

%----Now interpret each world
%----In world 0 
    & $in_world(int2world(0),
%----The domain for type person is the integers
        ( ( ! [P: person] : ? [I: $int] : P = int2person(I)
%----The type promoter is a bijection (injective and surjective)
          & ! [I1: $int,I2: $int] : 
              ( int2person(I1) = int2person(I2) => I1 = I2 ) )
%----geoff is interpreted as 0
        & ( geoff = int2person(0)
%----id_of coincides with the domain elements
          & ! [I: $int] : id_of(int2person(I)) = I )
%----like is true for 0 (and only 0 by next part for all worlds)
        & like(int2person(0) ) ) )
%----In all worlds
    & ! [IW: $int] :
        ( $greatereq(IW,0)
       => $in_world(int2world(IW),
%----The type promoter is a bijection (injective and surjective)
            ( ( ! [P: person] : ? [I: $int] : P = int2person(I)
              & ! [I1: $int,I2: $int] : 
                  ( int2person(I1) = int2person(I2) => I1 = I2 ) )
%----geoff is interpreted as the world number
            & ( geoff = int2person(IW)
%----id_of coincides with the world
            & id_of(int2person(IW)) = IW )
%----Like the person who is interpreted as this world number (geoff)
            & ( like(int2person(IW)) 
%----Like only this one person
              & ! [ID: $int] :
                  ( like(int2person(ID))
                <=> ID = IW ) ) ) ) ) ) ).
%------------------------------------------------------------------------------

The consistency of the interpretation formula cannot be confirmed by any ATP system I have.