Typed eXtended First-order Logic (TXF)

New logic features

• Formulae as terms
• Boolean variables
• FOOL terms ... tuples, conditionals, let expressions

Problem

• Axioms
• Mel and Zoey live on the island.
• Inhabitants of the island are either knights or knaves.
• Knights always tell the truth, and knaves always lie.
• Zoey says "Mel is a knave".
• Mel says "Neither Zoey nor I are knaves".
• Conjecture
• There is at least one knight and one knave on the island.

In logic

• Type information
• inhabitant is a type
• Statements are true or false (boolean)
• Mel is a inhabitant
• Zoey is a inhabitant
• is_knight takes one inhabitant argument, and returns boolean
• is_knave takes an inhabitant argument, and returns a boolean
• says takes an inhabitant and a statement as arguments, and returns a boolean
• Axioms
• I:inhabitant (is_knight(I)is_knave(I)) ∀ H2:human created_equal(H1,H2)
• I:inhabitantS:boolean (((is_knight(I) ∧ says(I,S)) → S)
• I:inhabitantS:boolean (((is_knave(I) ∧ says(I,S)) → ¬S)
• says(zoey,is_knave(mel))
• says(mel,¬ is_knave(zoey) ∧ ¬ is_knave(mel))
• Conjecture
• Knight:inhabitantKnave:inhabitant (is_knight(Knight) ∧ is_knave(Knave))

In TPTP format

• ```tff(inhabitant_decl,type,inhabitant: \$tType ).
tff(mel_decl,type,mel: inhabitant ).
tff(zoey_decl,type,zoey: inhabitant ).
tff(is_knight_decl,type,is_knight: inhabitant > \$o ).
tff(is_knave_decl,type,is_knave: inhabitant > \$o ).
tff(says_decl,type,says: ( inhabitant * \$o ) > \$o ).

tff(knights_xor_knaves,axiom,
! [I: inhabitant] : ( is_knight(I) <~> is_knave(I) ) ).
tff(knights_tell_truth,axiom,
! [I: inhabitant,S: \$o] : ( ( is_knight(I) & says(I,S) ) => S ) ).
tff(knaves_lie,axiom,
! [I: inhabitant,S: \$o] : ( ( is_knave(I) & says(I,S) ) => ~ S ) ).
tff(zoey_speaks,axiom,
says(zoey,is_knave(mel)) ).
tff(mel_speaks,axiom,
says(mel, ~ is_knave(zoey) & ~ is_knave(mel)) ).

tff(knight_and_knave,conjecture,
? [Knight: inhabitant,Knave: inhabitant] :
( is_knight(Knight) & is_knave(Knave) ) ).
```
• Check the syntax in SystemB4TPTP using TPTP4X.
• Try it in SystemOnTPTP using Vampire.

Challenge problem

Jon is the owner of Odie. Odie bit Jon twice! If a dog bits a person more than once, and (s)he is not the owner of the dog, the (s)he hates the owner of the dog. If a dog bites a person at least once then the person chases the dog, else the person feeds the dog. Jon says that a dog he dos not own bit him. Jon tells the truth. Prove that there exists a dog that Jon chases and another person that Jon hates.