Typed eXtended First-order Logic (TXF)

New logic features

Predicate and function arguments can be boolean, i.e., formulae
Typed variables, can be boolean
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.

Challenge problem

Jon is the owner of Odie. Odie bit Jon twice! If a dog bites a person more than once, and (s)he is not the owner of the dog, then (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 does not own bit him. Jon tells the truth. Prove that there exists a dog that Jon chases and another person that Jon hates.

Typed eXtended First-order Logic (TXF)

New logic features

Problem

In logic

In TPTP format

Challenge problem