Variations and Verification

Multiple Interpretations

• Uninterpreted functor is interpreted as each domain element
• Uninterpreted predicate is interpreted as true and false

Compact Variations

fof(equality_lost,fi_predicates,
    ( human("john") & human("got_a")
    & ~ human("a")  & ~ human("f") 
    & ! [X] : ~ created_equal("a",X)
    & ! [X] : ~ created_equal("f",X)
    & ! [X] : ~ created_equal(X,"a")
    & ! [X] : ~ created_equal(X,"f")
    & created_equal("john","john")  & created_equal("john","got_a")
    & created_equal("got_a","john") & created_equal("got_a","got_a") ) ).

• FM-Darwin's version

Verification

• Directly interpret each formula
• Add interpretation to formulae and find trusted model