Introduzione

Per mostrare come si può automatizzare il ragionamento con un linguaggio dove ci sono quantificazioni, usiamo un algoritmo proposto da Mojzesz Presburger nel 1929 per decidere la validità di un sottoinsieme dell'aritmetica.

Linguaggio

Il linguaggio sul quale sarà possibile decidere la verità prevede i seguenti operatori: Per esempio ∀x. ∃y. (x+y)=0 è una formula del nostro linguaggio.

Tale linguaggio semplice permette anche di esprimere operatori derivati come:

Esercizio

H1. Scrivere un tipo di dato form che rappresenta le formule dell'aritmetica di Presburger usando la notazione di deBruijn.

Forma prenex

La prima operazione dell'algoritmo consiste nel trasformare la formula in modo da avere i quantificatori all'inizio. Tale trasformazione è valida solo nella logica classica:

Per la negazione:
¬(∀x. (P x)) equivalente a ∃x. (¬(P x))
¬(∃x. (P x)) equivalente a ∀x. (¬(P x))
Per l'implicazione:
(∀x. (P x)) ⇒ Q equivalente a ∃x. ((P x) ⇒ Q)
(∃x. (P x)) ⇒ Q equivalente a ∀x. ((P x) ⇒ Q)
Q ⇒(∀x. (P x)) equivalente a ∀x. (Q ⇒ (P x))
(Q ⇒ ∃x. (P x)) equivalente a ∃x. (Q ⇒ (P x))
Queste trasformazioni sono valide se non esiste una x dentro Q che è libera. Se questo è il caso, bisogna ridenominare la variabile libera. Dunque, ∃x. ((∀x. (P x)) ⇒ (Q x)) si trasforma in ∃y. ∃x. ((P x) ⇒ (Q y)) e non in ∃x. ∃x. ((P x) ⇒ (Q x)).

Esercizio

H2. Scrivere una funzione lift_quant che calcola la forma prenex di una formula.

Forma DNF

La seconda operazione dell'algoritmo è quella di trasformare la formula in forma DNF (Disjunctive Normal Form) per avere i quantificatori all'inizio, dopo le disgiunzioni, quindi le congiunzioni e finalmente negazione di variabili o variabili.
Dunque prima si espandono le implicazioni:
P ⇒ Q equivalente a ¬P ∨ Q
Secondo, si mettono in fondo le negazioni:
¬(P ∨ Q) equivalente a ¬P ∧ ¬Q
¬(P ∧ Q) equivalente a ¬P ∨ ¬Q
¬(¬P) equivalente a P
Terzo, si mettono le disgiunzioni prima delle congiunzioni:
P ∧ (Q ∨ R) equivalente a (P ∧ Q) ∨ (P ∧ R)
(Q ∧ R) ∧ P equivalente a (Q ∧ P) ∨ (R ∧ P)

Esercizi

H3. Definire un tipo di dato form1 simile a form tranne che non ha l'implicazione, ma ha la congiunzione, la disgiunzione ed il modulo.

H4. Scrivere una funzione normal_form che trasforma una formula di tipo form in una formula equivalente di tipo form1 sotto forma prenex dnf.

*H5. Mettere la formula ¬((x∨¬y)⇒z) in forma DNF.

*H6. Mettere la formula ¬((∃x. (P x)) ⇒(∀x. (Q x))) in forma prenex DNF.

*H7. Mettere la formula (∀x.∃y. (P x y)) ⇒(∃x. (P x x)) in forma prenex DNF.

Eliminazione delle quantificazioni

L'algoritmo si basa sul fatto che si può decidere la validità di una formula dell'aritmetica di Presburger se non ha nessuna variabile. In tal caso, tutte le espressioni sono del tipo F1 = F2 dove dentro F1 ed F2 ci sono solo numeri e +, dunque si può decidere se sono vere o no. Conoscendo il valore delle espressioni è facile conoscere il valore della formula.
Per esempio, se abbiamo (3+5=7) ∨ ¬(2=1+2), la formula è vera.

Dunque, se esiste una procedura che permette di trasformare una formula in un'altra equivalente ma con un quantificatore di meno, iterando questa procedura alla fine abbiamo una formula senza quantificatori.

Eliminazione di una quantificazione

Per trasformare la formula, consideriamo l'ultima quantificazione. Poiché (∀x. (P x)) è equivalente a ¬(∃x. ¬(P x)), si può supporre che l'ultima quantificazione sia una quantificazione esistenziale.

Dunque, occupiamoci d'eliminare il quantificatore di una formula:
∃x. (... ∧ ... ∧ ... ∧ ... ) ∨ ... ∨ (... ∧ ... ∧ ... )

Una formula equivalente è:
(∃x. ... ∧ ... ∧ ... ∧ ... ) ∨ ... ∨ (∃x. ... ∧ ... ∧ ... )

Dunque è sufficiente sapere eliminare il quantificatore di una formula:
∃x. (... ∧ ... ∧ ... ∧ ... )

Si può anche supporre che x compaia dentro ogni sottoformula sotto una congiunzione perché
∃x. ((P x) ∧ Q) è equivalente a (∃x. (P x)) ∧ Q.
Esempio: ∃x. (x = 2) ∧ (y + y = 2) è equivalente a (∃x. (x = 2)) ∧ (y + y = 2).

Solo negazione

Un caso dove si può decidere subito è dato da una formula che contiene solo la negazione:
∃x. (¬(a1.x + E1=E'1) ∧.. ∧ ¬(an.x +En=E'n))

Poiché a1,...,an non sono zero, esiste un tale x.

Nessuna congiunzione

Se la formula non contiene alcuna congiunzione, allora ha solo due forme possibili:
∃x. E1 = E2
o
∃x. ¬(E1 = E2)

Se la variabile x non compare dentro E1 e neanche dentro E2, allora si può semplicemente eliminare la quantificazione: non serve a niente.

Se x compare dentro E1 o dentro E2, si può fattorizzare le x ed avere una formula equivalente che ha la forma: ∃x. a.x + E3 = E4 dove x non compare dentro E3 ed E4, ed a è positivo.
Esempio: ∃x. x + y= x + 1 + x + x è equivalente a ∃x. 2.x + 1 = y.

Aritmetica modulare

La formula ∃x. a.x + E1 = E2 dove x non compare dentro E1 ed E2 corrisponde in matematica al fatto che E1 è uguale a E2 modulo a. Si scrive cosí: E1 = E2 [a].
Esempio: ∃x. 2.x + 1 = y è equivalente a 1 = y [2].

Dunque, con questo nuovo operatore modulo abbiamo eliminato il quantificatore. Bisogna però verificare che si possono decidere formule E1 = E2 [a] con nessuna variabile. Ciò viene fatto calcolando E1-E2 e verificando che il risultato è divisibile per a.
Esempio: 3 = 7 [2] è vero: 3-7=-4 è divisibile per 2.

Si fa nella stessa maniera per ∃x. ¬(a.x + E1 = E2) che risulta in ¬(E1 = E2 [a]). Nel seguito, espandiamo quest'ultima formula in (E1 = E2+1 [a]) ∨ ... ∨ (E1 = E2+(a-1) [a])
Esempio: ¬(x = y [3]) si trasforma in (x = y + 1 [3]) ∨ (x = y + 2 [3]).

Abbiamo aggiunto un nuovo predicato modulo. Dunque una formula senza congiunzioni è anche
∃x. a.x + E1 = E2 [b]

È importante ricordarsi che in questo caso a è sempre un numero intero (proveniente da un prodotto scalare).

Per eliminare il quantificatore dalla prima formula, bisogna usare il gcd (massimo comun divisore) ed una proprietà matematica chiamata l'uguaglianza di Bezout:
∀x.∀y.∀z. ((∃a.∃b. (z = a*x + b*y)) ≡ (∃t. (z = (gcd x y)*t)))

Usando Bezout, abbiamo che ∃x. a.x + E1 = E2 [b] è equivalente a E1 = E2 [(gcd a b)]
Esempio: ∃z. (4.z + x = y [6]) si trasforma in x = y [2].

Almeno una equazione

I casi rimasti sono quando la congiunzione contiene almeno due elementi e almeno un elemento è una equazione o un modulo. Se c'è un'equazione, si può usare l'equazione per semplificare gli altri elementi.

Due equazioni

Abbiamo
a.x + E1 = E2 e b.x + E3 = E4.
Usando c=(lcm a b) (minimo comune multiplo), è equivalente a:
c.x + (c/a).E1 = (c/a).E2 e c.x + (c/b).E3 = (c/b).E4.
È equivalente a:
x + E1 = E2 e (c/a).E2 + (c/b).E3 = (c/a).E1 + (c/b).E4.

Una equazione e un modulo

Abbiamo
a.x + E1 = E2 e b.x + E3 = E4 [d] .
Usando c=(lcm a b) (minimo comune multiplo), è equivalente a:
c.x + (c/a).E1 = (c/a).E2 e c.x + (c/b).E3 = (c/b).E4 [(c/b)*d].
È equivalente a:
x + E1 = E2 e (c/a).E2 + (c/b).E3 = (c/a).E1 + (c/b).E4 [d].

Una equazione e una negazione

Abbiamo
a.x + E1 = E2 e ¬(b.x + E3 = E4) .
Usando c=(lcm a b) (minimo comune multiplo), è equivalente a:
c.x + (c/a).E1 = (c/a).E2 e ¬(c.x + (c/b).E3 = (c/b).E4).
È equivalente a:
x + E1 = E2 e ¬((c/a).E2 + (c/b).E3 = (c/a).E1 + (c/b).E4).

Esempio

∃x. ((x=1) ∧ (y+x=1 [2]) ∧ ¬(x=z))
è equivalente a
(∃x. (x=1)) ∧ ((y=0 [2]) ∧ ¬(z=1))
è equivalente a
(0 = 1 [1]) ∧ ((y=0 [2]) ∧ ¬(z=1))
è equivalente a
((y=0 [2]) ∧ ¬(z=1))

Nessuna equazione ma almeno un modulo

Adesso possiamo supporre che nella congiunzione non vi sia alcuna equazione ma contenga almeno un modulo:

Due moduli

Abbiamo
a.x + E1 = E2 [c] e b.x + E3 = E4 [d].
Usando e=(lcm c d) (minimo comune multiplo), è equivalente a:
((e/c)*a).x + (e/c).E1 = (e/c).E2 [e]
e
((e/d)*b).x + (e/d).E3 = (e/d).E4 [e].

Ciò vuol dire che il sistema iniziale è equivalente ad un altro che ha la forma:
a'.x + E'1 = E'2 [c'] e b'.x + E'3 = E'4 [c'].

Adesso se a' è uguale a b', si ottiene il sistema equivalente:
a'.x + E'1 = E'2 [c'] e E'2 + E'3 = E'1+E'4 [c'].

Altrimenti bisogna cominciare un processo iterativo facendo diminuire la differenza fra a' e b'. Allora il sistema precedente è equivalente a:
a'.x + E'1 = E'2 [c'] e (b'-a').x + E'2 + E'3 = E'1+E'4 [c'] se a' è minore di b'.
oppure
(a'-b').x + E'1 + E'4 = E'2 +E'3 [c'] e b'.x E'3 = E'4 [c']

Iterando il processo si ottiene in ogni caso un sistema equivalente che ha la forma:
a''.x + E''1 = E''2 [c'] e E''3 = E''4 [c'].

Esempio

10.x = z [3] ∧ 5.x = z [2]
è equivalente a:
20.x = 2.z [6] ∧ 15.x = 3.z [6]
è equivalente a:
5.x+z =0 [6] ∧ 15.x = 3.z [6]
è equivalente a:
5.x+z =0 [6] ∧ 10.x = 4.z [6]
è equivalente a:
5.x+z =0 [6] ∧ 5.x = 5.z [6]
è equivalente a:
5.x+z =0 [6] ∧ 6.z = 0 [6]

Un modulo

L'unico caso da considerare adesso è quando c'è solo un modulo e gli altri elementi dentro la congiunzione sono negazioni.

Se una formula del tipo ∃x. a.x + E1 = E2 [b] è vera, allora è vera per un numero infinito di valori di x: se è vera per x1, allora è vera anche per x1+b,x1+2.b,...

Una negazione impedisce solo una possibilità. Poiché nella congiunzione c'è solo un numero finito di negazioni, la validità della congiunzione è equivalente a quella del modulo.
Esempio: (∃x. (2.x+y=0[2])∧ ¬x=0) è equivalente a ∃x. (2.x+y=0[2]), dunque a y=0[2].

Esercizi

H8. Scrivere una funzione decide_ground che decide se una formula di tipo form1 senza variabili è vera.

H9. Scrivere la funzione factor_exp che fattorizza la variabile 0 in una espressione.

H10. Scrivere la funzione elim_quant che elimina una quantificazione.

H11. Scrivere una funzione presburger che implementa l'algoritmo di Presburger.

Esempio

Definiamo il predicato Even che indica se un numero è pari:
(Even x) ≡ (∃y. x=y+y)

Definiamo il predicato Odd che indica se un numero è dispari:
(Odd x) ≡ (∃y. x=y+y+1)

Adesso proviamo il teorema:
∀x. (Even x) ∨ (Odd x)

È equivalente a:
∀x. (∃y. x=y+y) ∨ (∃y. x=y+y+1)

Mettiamo in forma prenex-DNF:
∀x. ∃y1. ∃y2. (x=y1+y1) ∨ (x=y2+y2+1)

È equivalente a:
∀x. ∃y1. (x=y1+y1) ∨ (∃y2. x=y2+y2+1)

Eliminiamo la variabile y2:
∀x. ∃y1. (x=y1+y1) ∨ (x=1 [2])

È equivalente a:
∀x. (∃y1. (x=y1+y1)) ∨ (x=1 [2])

Eliminiamo la variabile y1:
∀x. (x=0 [2]) ∨ (x=1 [2])

È equivalente a:
¬(∃x. ¬((x=0 [2]) ∨ (x=1 [2])))

È equivalente alla formula sotto forma DNF:
¬(∃x. (¬(x=0 [2]) ∧ ¬(x=1 [2])))

Eliminiamo le negazioni di modulo:
¬(∃x. (x=1 [2] ∧ x=0 [2]))

Per eliminare x si usa il primo modulo per semplificare il secondo:
¬(∃x. (x=1 [2] ∧ 0=1 [2]))

È equivalente a:
¬((∃x. (x=1 [2])) ∧ 0=1 [2])

Adesso si può eliminare x:
¬(0=1 [1] ∧ 0=1 [2])

Poiché non ci sono piú variabili, è equivalente a
¬(True ∧ False)

Dunque è vero. La formula iniziale è un teorema.

Laurent Théry

Last modified: Tue Apr 30 01:38:21 MEST 2002