Kinship
This is a relatively larger example of using the natural logic described before for describing families.
Here is mine:
// Sam is a person
Sam(u) person(u).
// Dani is a person
Dani(v) person(v).
// Leo is a boy
Leo(p) person(p) male(p).
// Anna is a girl
Anna(q) person(q) female(q).
// Arthur is a boy
Arthur(r) person(r) male(r).
// Sam is Leo's, Anna's and Arthur's father
father(u, p) father(u, q) father(u, r).
// Dani is Leo's, Anna's and Arthur's mother
mother(v, p) mother(v, q) mother(v, r).
These describe basic facts about my family.
Here are some general statements about families in general:
for (let x: person(x)) {
for (let y: person(y)) {
// Every father is a male parent
if (father(x, y)) {
male(x) parent(x, y).
}
// Every mother is a female parent
if (mother(x, y)) {
female(x) parent(x, y).
}
// Every male parent is a father
if (parent(x, y) male(x)) {
father(x, y).
}
// Every female parent is a mother
if (parent(x, y) female(x)) {
mother(x, y).
}
// If A is a parent of B then B is a child of A
if (parent(x, y)) {
child(y, x).
}
// Every son is a male child
if (son(x, y)) {
male(x) child(x, y).
}
if (male(x) child(x, y)) {
son(x, y).
}
// Every daughter is a female child
if (daughter(x, y)) {
female(x) child(x, y).
}
if (female(x) child(x, y)) {
daughter(x, y).
}
// If A is an ancestor of B then B is a descendent of A
if (ancestor(x, y)) {
descedent(y, x).
}
if (parent(x, y)) {
// Every parent is an ancestor
ancestor(x, y).
// Every parent is an ancestor of its descendents
for (let z: person(z)) {
if (ancestor(y, z)) {
ancestor(x, z).
}
}
}
// If there is a person z who is a parent of x and y
// then x and y are siblings
for (let z: person(z)) {
if (parent(z, x) parent(z, y)) {
sibling(x, y).
}
}
if (sibling(x, y)) {
sibling(y, x).
if (male(x)) {
brother(x, y).
}
if (female(x)) {
sister(x, y).
}
}
if (brother(x, y)) {
male(x) sibling(x, y).
}
if (sister(x, y)) {
female(x) sibling(x, y).
}
}
}
With the basic facts about my family and the general statements about families in general, we can ask things that were only indirectly stated.
For example:
// Who is a child of Sam?
let x, y: Sam(x) child(y, x)?
You can run that query by clicking on the run button below:
The query returns three bindings, one for each of my kids.
This is kinda of exciting because child(u, p)
, child(u, q)
, child(u, r)
was never something that we explicitly stated, but rather something that was inferred from the basic facts and the general statements about families.
Here is another example:
// Who are Anna's brothers?
let x, y: Anna(x) brother(y, x)?
And again, you get back two responses that were never explicitly stated before, but were rather inferred from the logical form of the program.
Neat, huh?