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))
  • ∀ I:inhabitant ∀ S:boolean (((is_knight(I) ∧ says(I,S)) → S)
  • ∀ I:inhabitant ∀ S:boolean (((is_knave(I) ∧ says(I,S)) → ¬S)
  • says(zoey,is_knave(mel))
  • says(mel,¬ is_knave(zoey) ∧ ¬ is_knave(mel))
• Conjecture
  • ∃ Knight:inhabitant ∃ Knave: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 using TPTP4X in SystemB4TPTP.
• Check the axioms are consistent with Vampire-SAT in SystemOnTPTP.
• Try prove it using Vampire in SystemOnTPTP.
• View the derivation using IDV in SystemOnTSTP.
• Verify the derivation using GDV in SystemOnTSTP.

Challenge problem