Árvores Genealógicas

Linguagem das Árvores Genealógicas

Este domínio inclui factos como “Zeus é o pai de Atenas” e regras como “A avó de uma dada pessoa é a mãe de um progenitor dessa pessoa”.

Os termos deste domínio são as pessoas ou os deuses do Olimpo (Para desenjoar de famílias reais).
Duas relações unárias determinam o sexo: $$ \lit{Masculino}_1, \lit{Feminina}_1. $$
As relações familiares são representadas por relações binárias (palavras terminadas em “$\neut{}$” são versões neutras): $$ \begin{gathered} \neut{Progenitor}_2, \neut{Irm}_2, \lit{Irmão}_2, \lit{Irmã}_2, \lit{Descendente}_2, \lit{Filha}_2, \cr \lit{Filho}_2, \lit{Cônjuge}_2, \lit{Marido}_2, \lit{Esposa}_2, \neut{Av}_2, \neut{Net}_2, \neut{Ti}_2 \end{gathered} $$
Como cada pessoa tem exatamente um pai e uma mãe biológicos usam-se funções: $$ \lit{Pai}_1, \lit{Mãe}_1. $$

Veja também:

A mãe de uma pessoa é a progenitor feminina. $$ \forall x,m~\fat{Mãe}{x} = m \liff \fat{Feminina}{m} \land \neut{Progenitor}\at{m, x} $$

O marido de uma pessoa é o cônjuge masculino. $$ \forall x,m~\fat{Marido}{m, x} \liff \fat{Masculino}{m} \land \fat{Cônjuge}{m, x}. $$

Masculino e Feminina são conjuntos complementares. $$ \forall x~\fat{Masculino}{x} \liff \neg \fat{Feminina}{x}. $$

Progenitor e descendente são relações inversas. $$ \forall x, y~\neut{Progenitor}\at{x, y} \liff \fat{Descendente}{y, x}. $$

Os axiomas são as regras “iniciais”, que proporcionam o funcionamento básico de um domínio.

Os axiomas também exprimem factos básicos: Leto é a mãe de Apolo.
As regras das árvores genealógicas (e mais algumas nos exercícios) formam os axiomas deste domínio.

As definições são axiomas da forma

$$ \forall x,y~p\at{x,y} \liff \cdots $$

onde uma relação ($p$ neste caso) tem uma forma equivalente ($\liff \cdots$) onde apenas ocorrem expressões “já” definidas.

No domínio das árvores genealógicas as regras assentam apenas nas relações

$$ \lit{Descendente}, \lit{Cônjuge}, \lit{Feminina} $$

Algumas afirmações sobre um domínio são teoremas, isto é são deduzidas, via dedução natural, a partir dos axiomas. Por exemplo (exercício):

$$ \vdash \forall x,y~\neut{Irm}\at{x,y} \liff \neut{Irm}\at{y, x}. $$