Interpretation Representation and Model Verification

by Geoff Sutcliffe, Alex Steen, Pascal Fontaine


Motivation


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(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] :
      ( ( 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. How about merging them to, e.g., ...
%------------------------------------------------------------------------------
fof(equality_lost,interpretation,
    ( ! [X] : ( X = "a" | X = "f" | X = "john" | X = "gotA") 
    & ( a = "a"
      & f = "f"
      & john = "john"
      & grade("a") = "a"
      & grade("f") = "a"
      & grade("john") = "f"
      & grade("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.

FOF_Finite.s.p is the proof problem to verify the (counter) model using the technique discussed in Verification of Models.


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 ...
%------------------------------------------------------------------------------
%----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 (actually
%----not) the case being created equal is the same as really being equal.
tff(man_type,type,           man: $tType ).
tff(grade_type,type,         grade: $tType ).
tff(john_decl,type,          john: man ).
tff(a_decl,type,             a: grade ).
tff(f_decl,type,             f: grade ).
tff(grade_of_decl,type,      grade_of: man > grade ).
tff(created_equal_decl,type, created_equal: ( man * man ) > $o ).

tff(all_created_equal,axiom,
    ! [H1: man,H2: man] : created_equal(H1,H2) ).
tff(john_failed,axiom,
    grade_of(john) = f ).
tff(someone_got_an_a,axiom,
    ? [H: man] : grade_of(H) = a ).
tff(distinct_grades,axiom,
    a != f ).
tff(equality_lost,conjecture,
    ! [H1: man,H2: man] :
      ( created_equal(H1,H2)
    <=> ( H1 = H2 ) ) ).

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

... and a finite interpretation (a countermodel for the conjecture) is ...
%------------------------------------------------------------------------------
tff(man_type,type,           man: $tType ).
tff(grade_type,type,         grade: $tType ).
tff(john_decl,type,          john: man ).
tff(a_decl,type,             a: grade ).
tff(f_decl,type,             f: grade ).
tff(grade_of_decl,type,      grade_of: man > grade ).
tff(created_equal_decl,type, created_equal: ( man * man ) > $o ).

tff(d_man_type,type,         d_man: $tType).
tff(d_grade_type,type,       d_grade: $tType).
tff(d_to_man_decl,type,      d_to_man: d_man > man ).
tff(d_to_grade_decl,type,    d_to_grade: d_grade > grade ).

tff(d_john_decl,type,        d_john: d_man ).
tff(d_got_A_decl,type,       d_got_A: d_man ).
tff(d_a_decl,type,           d_a: d_grade ).
tff(d_f_decl,type,           d_f: d_grade ).

tff(equality_lost,interpretation,
%----The two man domain elements are d_john and d_got_A
    ( ! [X: d_man] : ( X = d_john | X = d_got_A )
    & $distinct(d_john,d_got_A)
%----The type promoter is a bijection (injective and surjective)
    & ! [X: d_man,Y: d_man] : ( d_to_man(X) = d_to_man(Y) => X = Y )
    & ! [X: man] : ? [DX: d_man] : d_to_man(DX) = X
%----The two grade domain elements are d_a and d_f
    & ! [X: d_grade]: ( X = d_a | X = d_f )
    & $distinct(d_a,d_f)
%----The type promoter is a bijection (injective and surjective)
    & ! [X: d_grade,Y: d_grade] : ( d_to_grade(X) = d_to_grade(Y) => X = Y )
    & ! [X: grade] : ? [DX: d_grade] : d_to_grade(DX) = X
%----Interpret terms via the type-promoted domain elements
    & ( a = d_to_grade(d_a)
      & f = d_to_grade(d_f)
      & john = d_to_man(d_john)
      & grade_of(d_to_man(d_john)) = d_to_grade(d_f)
      & grade_of(d_to_man(d_got_A)) = d_to_grade(d_a) )
%----Interpret atoms as true of false
    & ( created_equal(d_to_man(d_john),d_to_man(d_john))
      & created_equal(d_to_man(d_john),d_to_man(d_got_A))
      & created_equal(d_to_man(d_got_A),d_to_man(d_john))
      & created_equal(d_to_man(d_got_A),d_to_man(d_got_A)) ) ) ).
%----To clarify, if John was not equal to the man who got an A, it would be
%----     & ~ created_equal(d_to_man(d_john),d_to_man(d_got_A))
%----     & ~ created_equal(d_to_man(d_got_A),d_to_man(d_john))

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

Hmmm, should the types be inside the interpretation?

TFF_Finite.s.p is the proof problem to verify the (counter) model using the technique discussed in Verification of Models.


Representation of TXF Interpretations


Representation of THF Interpretations


Representation of Infinite Interpretations

I'm just spitballing here, but I don't see any problem with relaxing the format for finite interpretations to allow infinite interpretations, with domains of integer size or even real size. Consider the following TFF example that requires an integer size model ...
%------------------------------------------------------------------------------
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) ) ).

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

How's this for an explicit infinite model using 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(d_to_person_decl,type,   d_to_person: $int > person ).

tff(equality_lost,interpretation,
%----The type promoter is a bijection (injective and surjective)
    ( ! [ID1: $int,ID2: $int] : ( d_to_person(ID1) = d_to_person(ID2) => ID1 = ID2 )
    & ! [D: person] : ? [ID: $int] : d_to_person(ID) = D
%----Mapping people to integers
    & bob = d_to_person(0)
    & ! [N: $int] : 
        child_of(d_to_person(N)) = d_to_person($sum(N,1))
%----Interpretation of descendancy
    & ! [A: $int,D: $int] : 
        ( is_descendant(d_to_person(A),d_to_person(D)) <=> $less(A,D) ) ) ).

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

TFF_Infinite.s.p is the proof problem to verify the (counter) model using the technique discussed in Verification of Models.


Representation of Finite-Finite Kripke Interpretations

This can be done in only a typed logic.

Record world information in one formula, using a new defined type $ki_world, a new defined predicate $in_ki_world with type $ki_world > $o, a new defined predicate $accessible_ki_world with type ($ki_world * $ki_world) > $o, and a new defined constant $initial_ki_world with type $ki_world. Syntactically distinct constants of type $ki_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.

Here's a problem that has a counter model with a finite number of worlds each of which has a finite domain (hence "Finite-Finite Kripke Interpretation") ...

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

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(necessary_healthy_fruit_everywhere,axiom,
    ! [F: fruit] : {$necessary} @ (healthy(F)) ).

tff(rotten_apple_everywhere,axiom,
    rotten(apple) ).

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

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

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

After using NTF2THF to embed the problem into TH0, Nitpick finds this counter model ...
%------------------------------------------------------------------------------
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(w1_decl,type,w1: $ki_world).
tff(w2_decl,type,w2: $ki_world).
tff(d_fruit_type,type,d_fruit: $tType).
tff(d_to_fruit,type, d_to_fruit: d_fruit > fruit )
tff(d_apple_decl,type,d_apple: d_fruit).
tff(d_banana_decl,type,d_banana: d_fruit).

tff(fruity_worlds,interpretation,
    ( ! [W: $ki_world] : ( W = w1 | W = w2 )
    & $initial_ki_world = w1
    & ( $accessible_ki_world(w1,w2) ) 
    & ! [W: $ki_world] : $accessible_ki_world(W,W)     %----Logic is T
    & ( $in_ki_world(w1)
     => ( ! [X: d_fruit] : ( X = d_apple | X = d_banana )
        & $distinct(d_apple,d_banana)
        & ! [X: d_fruit,Y: d_fruit] : ( d_to_fruit(X) = d_to_fruit(Y) => X = Y )
        & ! [X: fruit] : ? [DX: d_fruit] : d_to_fruit(DX) = X
        & ( apple = d_to_fruit(d_apple)
          & banana = d_to_fruit(d_banana) )
        & ( healthy(d_to_fruit(d_apple))
          & healthy(d_to_fruit(d_banana))
          & rotten(d_to_fruit(d_apple))
          & rotten(d_to_fruit(d_banana)) ) ) )
    & ( $in_ki_world(w2)
     => ( ! [X: d_fruit] : ( X = d_apple | X = d_banana )
        & $distinct(d_apple,d_banana)
        & ! [X: d_fruit,Y: d_fruit] : ( d_to_fruit(X) = d_to_fruit(Y) => X = Y )
        & ! [X: fruit] : ? [DX: d_fruit] : d_to_fruit(DX) = X
        & ( apple = d_to_fruit(d_apple)
          & banana = d_to_fruit(d_banana) )
        & ( healthy(d_to_fruit(d_apple))
          & healthy(d_to_fruit(d_banana))
          & rotten(d_to_fruit(d_apple))
          & ~ rotten(d_to_fruit(d_banana)) ) ) )) ).

%----Logic 4, if I wanted it.
% tff(ki_system_4,axiom,
%     ! [W1: $ki_world,W2: $ki_world,W3: $ki_world]
%       ( ( $accessible_ki_world(W1,W2)
%         & $accessible_ki_world(W2,W3) )
%      => $accessible_ki_world(W1,W3) ) ).

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

NTF_Finite-Finite.s.p is the proof problem to verify the (counter) model using the technique discussed in Verification of Models.


Representation of Finite-Infinite Kripke Interpretations

This example requires (I think) only three worlds, but they have to have infinite domains. The current world has the start "state" null and a sequence of other states using red xor green flips. One of the other two world starts with a red sequence, and the other starts with a green sequence. As sequences with different colours are distinct, the two world need to have different infinite domains. I think.
%------------------------------------------------------------------------------
tff(simple_spec,logic,
    $alethic_modal == [
      $constants == $rigid,
      $quantification == $constant,
      $modalities == $modal_system_T ] ).

tff(colour_type,type, colour: $tType ).
tff(sequence_type,type, sequence: $tType ).

tff(red_decl,type, red: colour ).
tff(green_decl,type, green: colour ).
tff(null_decl,type, null: sequence ).
tff(flip_decl,type, flip: ( colour * sequence ) > sequence ).
tff(state_decl,type, state: sequence > $o ).

tff(only_two_different_colours,axiom,
    ! [C: colour] : ( ( C = red ) <~> ( C = green ) ) ).

tff(null_not_flip,axiom,
    ! [C: colour,S: sequence] : ( null != flip(C,S) ) ).

tff(different_flips_1,axiom,
    ! [S: sequence] : ( flip(red,S) != flip(green,S) ) ).

tff(different_flips_2,axiom,
    ! [C: colour,S1: sequence,S2: sequence] :
      ( ( flip(C,S1) = flip(C,S2) ) => ( S1 = S2 ) ) ).

tff(next_state,axiom,
    ! [S: sequence] :
      ( state(S)
     => ( state(flip(red,S)) <~> state(flip(green,S)) ) ) ).

tff(start_state,axiom-local,
    state(null)).

tff(possible_states,axiom-local,
    ! [S: sequence] :
      ( ( {$possible} @ (state(flip(red,S))) )
      & ( {$possible} @ (state(flip(green,S))) ) ) ).
%------------------------------------------------------------------------------


Representation of Infinite-Finite Kripke Interpretations

This example requires (I think) an infinite number of worlds. The interpretation in the current world will have an infinite domain, but all the other worlds' domains need only a single element (one of the domain elements from the current world). All the domain elements of the current world need to have a corresponding world with that domain element.
%------------------------------------------------------------------------------
tff(simple_spec,logic,
    $alethic_modal == [
      $constants == $flexible,
      $quantification == $varying,
      $modalities == $modal_system_T ] ).

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

%----Infinite people. 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_and_only_geoff,axiom,
    ( like(geoff)
    & ! [P: person] :
        ( like(P)
       => P = geoff ) ) ).

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

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

Here's a model with an integer number of worlds.
%------------------------------------------------------------------------------
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(d_to_person_decl,type, d_to_person: $int > person ).
tff(d_id_of_decl,type,id_of: person > $int).

tff(w_to_ki_world_decl,type,w_to_ki_world: $int > $ki_world ).
%----To fool Vampire
tff(ki_world_type,type,$ki_world: $tType).
tff(initial_ki_world_decl,type,$initial_ki_world : $ki_world).
tff(in_ki_world_decl,type,$in_ki_world: $ki_world > $o).
tff(accessible_ki_world_decl,type,$accessible_ki_world: ($ki_world * $ki_world) > $o).

tff(ki_name,interpretation,
%----An infinite number of worlds, numbered by naturals
    ( ! [IW: $int] : 
        ( $greatereq(IW,0)
       => ? [W: $ki_world] : w_to_ki_world(IW) = W )
    & $initial_ki_world = w_to_ki_world(0)
%----The type promoter is a bijection (injective and surjective)
    & ! [IW1: $int,IW2: $int] : ( ( w_to_ki_world(IW1) = w_to_ki_world(IW2) ) => ( IW1 = IW2 ) )
    & ! [W: $ki_world] : ? [IW: $int] : w_to_ki_world(IW) = W
%----World 0 can access itself (system T)
    & $accessible_ki_world(w_to_ki_world(0),w_to_ki_world(0))
%----World 0 can access all other worlds
    & ! [IW: $int] : 
        ( $greater(IW,0)
       => $accessible_ki_world(w_to_ki_world(0),w_to_ki_world(IW)) )

%----Now interpret each world
%----The type promoter is a bijection (injective and surjective)
    & ! [ID1: $int,ID2: $int] : ( d_to_person(ID1) = d_to_person(ID2) => ID1 = ID2 )
    & ! [D: person] : ? [ID: $int] : d_to_person(ID) = D
%----In world 0 
    & ( $in_ki_world(w_to_ki_world(0))
%----There are infinite domain elements
     => ( ! [P: person] : ? [ID: $int] : P = d_to_person(ID)
%----geoff is interpreted as 0
        & geoff = d_to_person(0)
%----id_of coincides with the domain elements
        & ! [I: $int] : id_of(d_to_person(I)) = I
%----like is true for 0
        & like(d_to_person(0) ) ) )
%----In other worlds there is one domain element
    & ! [W: $int] :
        ( ( $greater(W,0)
          & $in_ki_world(w_to_ki_world(W)) )
%----There is a domain element for geoff, and that's the only domain element
       => ( ? [GID: $int] : 
              ( geoff = d_to_person(GID)
              & ! [ID: $int] :
                  ( geoff = d_to_person(ID)
                 => ID = GID ) )
%----geoff is interpreted as the same domain element as the world number
          & geoff = d_to_person(W)
          & id_of(d_to_person(W)) = W
          & like(d_to_person(W)) ) ) ) ).

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


Representation of Infinite-Infinite Kripke Interpretations

Consider the following NTF example that requires an Infinite-Infinite model ...
%------------------------------------------------------------------------------
tff(simple_spec,logic,
    $alethic_modal == [
      $constants == $rigid,
      $quantification == $constant,
      $modalities == $modal_system_S5 ] ).

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(before_geoff_born,axiom,
    ! [Year: $int] :
      ( $less(Year,1961)
     => ~ alive(geoff,Year) ) ).

tff(geoff_born,axiom,
    alive(geoff,1961) ).

tff(geoff_alive_now,axiom,
    alive(geoff,2022) ).

tff(geoff_age,axiom,
    ! [Year: $int] :
      ( ( alive(geoff,Year)
       => age(geoff,Year) = $difference(Year,1961) )
      & ( ~ alive(geoff,Year)
       => age(geoff,Year) = -1 ) ) ).

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] :
              ( $greatereq(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 will be a Infinite-Infinite model, when I find one ...
[an error occurred while processing this directive]


Visualization of Interpretations

Visualizing a finite interpretation: Here's a TFF interpretation encoded as a derivation that can be
viewed in IDV:
%------------------------------------------------------------------------------
thf(a,negated_conjecture,
    a: grade,
    introduced(language,[level(0)]) ).

thf(f,negated_conjecture,
    f: grade,
    introduced(language,[level(0)]) ).

thf(john,negated_conjecture,
    john: human,
    introduced(language,[level(0)]) ).

thf(grade_of,negated_conjecture,
    grade_of: human > grade,
    introduced(language,[level(0)]) ).

thf(created_equal,negated_conjecture,
    created_equal: (human * human) > $o,
    introduced(language,[level(0)]) ).

tcf(grade_of_john,plain,
    "john": human,
    inference(interpretation,[level(1)],[grade_of]) ).

tcf(grade_of_gotA,plain,
    "gotA": human,
    inference(interpretation,[level(1)],[grade_of]) ).

tcf(created_equal_john,plain,
    "john": human,
    inference(interpretation,[level(1)],[created_equal]) ).

tcf(created_equal_gotA,plain,
    "gotA": human,
    inference(interpretation,[level(1)],[created_equal]) ).

tcf(created_equal_john_john,plain,
    "john": human,
    inference(interpretation,[level(2)],[created_equal_john]) ).

tcf(created_equal_john_gotA,plain,
    "gotA": human,
    inference(interpretation,[level(2)],[created_equal_john]) ).

tcf(created_equal_gotA_john,plain,
    "john": human,
    inference(interpretation,[level(2)],[created_equal_gotA]) ).

tcf(created_equal_gotA_gotA,plain,
    "gotA": human,
    inference(interpretation,[level(2)],[created_equal_gotA]) ).

tcf(d_a,conjecture,
    "a": grade,
    inference(interpretation,[level(3)],[a,grade_of_gotA]) ).

tcf(d_f,conjecture,
    "f": grade,
    inference(interpretation,[level(3)],[f,grade_of_john]) ).

tcf(d_john,conjecture,
    "john": human,
    inference(interpretation,[level(3)],[john]) ).

tcf(d_gotA,conjecture,
    "gotA": human,
    inference(interpretation,[level(3)],[]) ).

cnf(d_true,conjecture,
    $true,
    inference(interpretation,[level(3)],[created_equal_john_john,created_equal_gotA_gotA]) ).

%----Note this is not the true example, made some things false for illustration
cnf(d_false,conjecture,
    $false,
    inference(interpretation,[level(3)],[created_equal_john_gotA,created_equal_gotA_john]) ).

fof(o_type,axiom,
    $o,
    inference(type,[level(4)],[d_true,d_false]) ).

fof(human_type,axiom,
    human,
    inference(type,[level(4)],[d_john,d_gotA]) ).

fof(grade_type,axiom,
    grade,
    inference(type,[level(4)],[d_a,d_f]) ).

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

Visualizing an Kripke interpretation reachability relation: Draw the graph, e.g., using Graphviz.


Verification of Models

Let ... For example ... In the TPTP World the interpretation Ι is represented by formulae φΙ ... Currently the TPTP World specifies the roles fi_domain, fi_functors, and fi_predicates. The plan is to drop the fi_ prefixes, and allow infinite models.

For example ...

Proof that

    if φΙ ⊨ φ then Ι ⊨ φ

For example ...