2.1 Linguaggi del primo ordine e programmi logici

Una teoria del primo ordine è costituita da un alfabeto, da un linguaggio del primo ordine, da un insieme di assiomi e da un insieme di regole di inferenza. Il linguaggio del primo ordine è costituito da formule ben formate della teoria. Gli assiomi sono un sottoinsieme delle formule ben formate. Gli assiomi e le regole di inferenza permettono di derivare teoremi sulla base della teoria.

Un alfabeto è dato dalle seguenti classi di simboli:

• variabili denotate dalle ultime lettere minuscole dell'alfabeto.
• costanti denotate dalle prime lettere minuscole dell'alfabeto.
• simboli di funzione denotati dalle lettere minuscole f, g, h ....
• simboli di predicati denotati dalle lettere minuscole p, q, r ....
• connettivi logici : $\neg , \vee , \wedge , \Rightarrow, \Leftrightarrow$ .
• quantificatori : $\exists , \forall$.
• simboli di punteggiatura : ')', '(' e ','.

Un linguaggio del primo ordine su un dato alfabeto è un insieme di formule costruite a partire dai simboli di quell'alfabeto.

Nel seguito, indicheremo i linguaggi del primo ordine con la coppia $<\Pi ,\Sigma>$, dove $\Sigma$ è una segnatura e $\Pi$ è un insieme di simboli di predicato.

Per definire le formule ben formate definiamo un termine induttivamente:

• una variabile è un termine
• una costante è un termine
• se f è un simbolo di funzione di arietá n e $t_{1} \ldots t_{n}$ allora f $(t_{1}\ldots t_{n})$è un termine.

Quindi una formula ben formata è definita induttivamente come segue:

• se p è un simbolo di predicato n-ario e $t_{1} \ldots t_{n}$ sono termini, allora p $(t_{1}\ldots t_{n})$ è una formula (atomo).
• se F e G sono formule, allora $(\neg F), (F \wedge G), (F \vee G), (F \Rightarrow G), (F \Leftrightarrow G)$ sono formule.
• se F è una formula e $x$ è una variabile, allora $(\forall x F) e (\exists x F)$ sono formule.

Un letterale è un atomo o la negazione di un atomo.

Una clausola è una formula del tipo

$$\forall x_{1} \ldots \forall x_{s} (L_{1} \vee \ldots \vee L_{m})$$

dove ogni $L_{i}$ è un letterale e $x_{1} \ldots x_{s}$ sono tutte le variabili occorrenti in $L_{1} \vee \ldots \vee L_{m}$.

Poichè in programmazione logica si manipolano clausole, adotteremo una notazione speciale detta forma clausale. Quindi denoteremo la clausola

$$\forall x_{1} \ldots \forall x_{s} (A_{1} \vee \ldots \vee A_{k} \vee \neg B_{1} \vee \ldots \vee \neg B_{n})$$

dove $A_{1}, \ldots ,A_{k}, B_{1}, \ldots ,B_{n}$ sono atomi e $x_{1},\ldots , x_{n}$ sono tutte le variabili occorrenti in tali atomi, per mezzo di

$$A_{1}, \ldots ,A_{k} \leftarrow B_{1}, \ldots ,B_{n}$$

Una clausola di programma è una clausola del tipo

$$A \leftarrow L_{1}, \ldots , L_{n}$$

dove A può essere solo un letterale positivo. Se non tutti gli $L_{i}$ sono letterali positivi, la clausola è detta generale, altrimenti è detta clausola di Horn.

A è detta testa della clausola, mentre $L_{1}, \ldots ,L_{n}$ costituiscono il corpo.

Una clausola del tipo $A \leftarrow$ è detta unitaria, o fatto.

Un goal è una clausola della forma $\leftarrow L_{1}, \ldots , L_{n}$, dove ogni $L_{i}$ è detto sottogoal. Il simbolo $\Box$ denota la clausola vuota, cioè una clausola con corpo e testa vuoti e viene interpretato come una contraddizione.

Un programma logico è un insieme finito non vuoto di clausole di programma. Se almeno una delle clausole è generale, il programma sarà detto generale.

Una level mapping di un programma generale è una funzione dall'insieme di simboli di predicato agli interi non negativi. Il valore della level mapping rispetto ad un simbolo di predicato è detto livello di quel simbolo di predicato.

Un programma generale è stratificato se ha una level mapping tale che, in ogni clausola di programma $A \leftarrow L_{1}, \ldots , L_{n}$ il livello del simbolo di predicato di ogni letterale positivo (risp. negativo) nel corpo è minore o uguale (risp. minore) al livello del simbolo di predicato in A.

Le seguenti definizioni di due classi di programmi logici saranno utili nei capitoli successivi, in particolar modo riguardo alla negazione intensionale.

Un programma logico è detto n.v.i.(not variable introducing) se per ogni sua clausola del tipo $A \leftarrow B$ vale che nel corpo B occorrono solo variabili che occorrono nella testa A.

Un programma logico è detto left linear se ogni testa delle sue clausole non contiene occorrenze multiple della stessa variabile.