With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

No credit card required

All in the Family

Now let’s move on and try something more interesting. We’re going to go back to the family-relationships example from the previous chapter and prove that if two people are cousins, then they have a common grandparent.

In our family relations, we need to define what cousins are in logical terms: we’ll say that two people are cousins if they each have a parent who’s a sibling of one of the other’s parents. In FOPL, that’s this: a: b: Cousin(a, b) m: n: Sibling(m, n) Parent(m, a) Parent(n, b).

We want to prove that d: e: Cousin(d, e) g: Grandparent(g, d) Grandparent(g, e).

Like the proof of the excluded middle, we can do this without branching the tree. The proof does have a fair bit of jumping around. ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

No credit card required