Typed First-order Logic (TFF)

New logic features


In logic

In TPTP format

Challenge problem

Geoff is the teacher of Joe. Joe is not stupid but Joe failed. If a student failed then either the student is stupid or there is is some other student with the same teacher who also failed. Therefore there is some student other then Joe and also taught by Geoff, who failed. Optional: Assume that each student has only one teacher, so that, e.g., Geoff is the only teacher of Joe and the other student.