Crociere FOL

$D=\{\}$

$F=\{\text{nome/1}\}$

• nome(i) funziona che associa elemento del dominio il suo nome

$P=\{\text{irociera/1, itinerario/1, segue/2}\}$

• crociera(x)è true se x è una crociera
• itinerario(x) è true se x è un itinerario
• destinazione(x) è true se x è una destinazione
• segue(x,y) è true se x (crociera) segue y (itinerario)
• tocca(x,y) è true se x (crociera) tocca y (destinazione)
• lunamiele(x) è true se x (crociera) è di tipo luna di miele
• perfamiglie(x) è true se x (crociera) è di tipo per famiglie

Esercizio 2

Ogni crociera segue esattamente un itinerario:

$$\forall c\text{crociera}(c)⟹(\exists i_1\text{itinerario}(i_1)\wedge \text{segue}(c,i_1)\wedge \nexists i_2\text{itinerario}(i_2)\wedge (i_1\ne i_2)\wedge \text{segue}(c,i_2))$$

Esercizio 3

Gli itinerari hanno un nome univoco (non esistono due o più itinerari cono lo stesso nome)

$$\forall i_1,i_2(\text{itinerario}(i_1)\wedge \text{tinerario}(i_2)\wedge (i_1\ne i_2)⟹\text{nome}(i_1)\ne \text{nome}(i_2))$$

Esercizio 4

Ogni crociera tocca un certo insieme non vuoto di destinazioni.

\forall c\ \text{crociera}(c) \implies \exists d \ \text{destinazione}(d) \wedge \text{tocca}(c,d)

Esercizio 5

Le crociere si dividono in crociere di luna di miele e crociere per famiglia.

$$\forall c\text{crociera(c)}⟹(\text{lunamiale}(c)\vee \text{perfamiglie}(c))\wedge \neg (\text{lunamiale}(c)\wedge \text{perfamiglie}(c))$$