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

Verification of Models

Σ be an untyped first-order logic language, consisting of ...
- V_Σ, a set of variables
- F_Σ, a set of functions with arity
- P_Σ, a set of predicate with arity
φ be a formula written in Σ
Ι be an interpretation of Σ, consisting of ...
- D_Ι, a set of domain elements.
- F_Ι, a mapping from elements of F applied to arguments from D, to D.
- R_Ι, a mapping from elements of D applied to arguments from D, to {TRUE,FALSE}.
Ι can be a partial interpretation of Σ, but must be enough to interpret φ.

Σ ...
- V_Σ = {Words starting uppercase}
- F_Σ = {geoff/0, brotherOf/2}
- P_Σ = {taller/2}
Ι ...
- D_Ι = {😀, 🕺}
- F_Ι = { geoff → 😀, brotherOf(😀) → 🕺, brotherOf(🕺) → 😀}
- R_Ι = { taller(😀,😀) → FALSE, taller(😀,🕺) → FALSE, taller(🕺,😀) → TRUE, taller(🕺,🕺) → FALSE}
φ ...
- taller(brotherOf(geoff),geoff)

In the TPTP World the interpretation Ι is represented by formulae φ_Ι ...

The domain is represented by an annotated formula with role domain, and a formula that uses equalities to list the domain element values. To ensure that the domain elements written in a domain are understood to be distinct, "distinct object"s or numbers can be used. Otherwise their inequality must also be specified.
The function map is represented by formulae with the role functors, and formulae that use equalities to express the mapping of functions applied to domain elements, to domain element values.
The predicate map is represented by formulae with the role predicates, and formulae that use equalities to express the mapping of functions applied to domain elements, to truth values.

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.

Let E_{φ_Ι} be the set {e that are "domain element"s in φ_Ι}.
Let inI_{φ_Ι}(e) be the d_Ι ∈ D_Ι corresponding to e ∈ E_{φ_Ι}.

For example ...

tff(myI_domain,domain, ! [X: $i] : ( X = "face" | X = "stickman" ) ).

tff(myI_functions,functors, ( geoff = "face" & brotherOf("face") = "stickman" & brotherOf("stickman") = "face" ) ).

tff(myI_predicates,predicates, ( ~ taller("face","face") & ~ taller("face","stickman") & taller("stickman","face") & ~ taller("stickman","stickman") ) ).

E_{φ_Ι} = {"face", "stickman"}
inI_{φ_Ι}("face") = 😀, inI_{φ_Ι}("stickman") = 🕺

Proof that
if φ_Ι ⊨ φ then Ι ⊨ φ

Let Σ' be ...

V'_Σ' = V_Σ
F'_Σ' = F_Σ ∪ E_{φ_Ι}
P'_Σ' = P_Σ

Let Ι' be an interpretation ...

D_Ι' = D_Ι
F_Ι' = F_Ι ∪ {e → inI_Ι(e)} for e ∈ E_{φ_Ι}
P_Ι' = P_Ι

If Ι' ⊨ φ then Ι ⊨ φ, because φ contains nothing from E_{φ_Ι} and Ι' is the same as Ι wrt all other symbols.
Ι' ⊨ φ_Ι, because ...

Let φ_Ι' be the "formulae" that result from applying Ι' to the e ∈ E_{φ_Ι} in φ_Ι.
Ι' ⊨ φ_Ι' iff Ι ⊨ φ_Ι'.
Ι ⊨ φ_Ι' by the construction of Ι
Ι' ⊨ φ_Ι'
By undoing the application of Ι' to the e ∈ E_{φ_Ι} in φ_Ι, Ι' ⊨ φ_Ι

If φ_Ι ⊨ φ then Ι' ⊨ φ (every model of φ_Ι is a model of φ, Ι' is a model of φ_Ι, so Ι' is a model of φ)
If φ_Ι ⊨ φ then Ι ⊨ φ
For example ...

Σ' ...

V'_Σ' = {Words starting uppercase}
F'_Σ'' = {geoff/0, brotherOf/2, "face"/0, "stickman"/0}
P'_Σ' = {taller/2}

Ι' ...

D_Ι' = {😀, 🕺}
F_Ι' = { geoff → 😀, "face" → 😀, "stickman" → 🕺,
brotherOf(😀) → 🕺, brotherOf(🕺) → 😀}
R_Ι' = { taller(😀,😀) → FALSE, taller(😀,🕺) → FALSE, taller(🕺,😀) → TRUE, taller(🕺,🕺) → FALSE}

Ι' ⊨ taller(brotherOf(geoff),geoff), so
Ι ⊨ taller(brotherOf(geoff),geoff)
Ι' ⊨ tff(myI_domain, ...
If tff(myI_domain, ... ⊨ taller(brotherOf(geoff),geoff) then
Ι' ⊨ taller(brotherOf(geoff),geoff)
If tff(myI_domain, ... ⊨ taller(brotherOf(geoff),geoff) then
Ι ⊨ taller(brotherOf(geoff),geoff)