Typed Higher-order Logic (THF)

New logic features


In logic

In TPTP format

Challenge problem

Andrew, Betty, and Charlie are (different) people. Andrew and Betty loves themselves, neither love Charlie, and Andrew does not love Betty. Selfish love is a relationship between two (different) people in which the first person loves themself, and does not love anyone else. Prove that there exists a property of a person that is true for Andrew but not for Betty.