Logica predicatelor - Laborator 8 și 9

Exerciții folosind rezoluția

Folosirea unui demonstrator

Pentru a verifica că am scris corect formulele și a produce demonstrații vom folosi un demonstrator de teoreme. Pe calculatoarele din laborator e instalat demonstratorul Prover9, ales pentru sintaxa simplă de scriere a formulelor. Mai jos e formalizat exemplul cu indicele Dow Jones de la curs.

formulas(assumptions).
  all x (inv(x) -> exists c (buys(x, c) & (stock(c) | bond(c)))).
  DJcrash -> all x (stock(x) & -gold(x) -> falls(x)).
  TBrise -> all x (bond(x) -> falls(x)).
  all x (inv(x) & exists c (buys(x, c) & falls(c)) -> -happy(x)).
end_of_list.

formulas(goals).
  DJcrash & TBrise
    -> all x (inv(x) & happy(x) -> exists c (buys(x, c) & stock(c) & gold(c))).
end_of_list.
Problema a fost împărțită în două secțiuni: cea de ipoteze (assumptions) și cea de concluzii (goals) -- aici, o singură concluzie. Ambele se încheie cu end_of_list.
Fiecare formulă se încheie cu punct. Spațiile nu contează, și se poate scrie pe mai multe rânduri.
Conectorii logici se scriu: negație -, conjuncție &, disjuncție |, implicație ->, echivalență <->. Cuantificatorul universal e all și cel existențial exists.
Precedența e cea uzuală, întâi operatorii unari, apoi &, | și ->.

Demonstratorul se folosește din linia de comandă, indicând fișierul cu descrierea problemei.
prover9 -f numefișier Dacă sistemul găsește o demonstrație, va afișa pașii ei, indicând la fiecare cum a fost obținută formula respectivă. De exemplu
14 -TBrise | -bond(x) | falls(x). [clausify(3)]. e obținut prin transformare în formă clauzală din a treia ipoteză:
3 TBrise -> (all x (bond(x) -> falls(x)))
Formula 13 bond(f1(c1)) | -DJcrash | gold(f1(c1)) | falls(f1(c1)). [resolve(10,a,11,b)]
e obținută prin rezoluție din literalul întâi (a) din (10) și al doilea (b) din (11):
10 stock(f1(c1)) | bond(f1(c1)).
11 -DJcrash | -stock(x) | gold(x) | falls(x).
În formula (10) remarcăm introducerea unei constante Skolem c1 (pentru investitor) și a unei funcții skolem f1 (pentru ceea ce cumpără investitorul).
Urmăriți și ceilalți pași de rezoluție, pentru a vă obișnui cu aplicarea ei.

Acest demonstrator și multe altele pot fi accesate și online. Sintaxa folosită (TPTP) e însă ușor diferită și necesită mai multe paranteze, am preferat această variantă.

Exerciții propuse pentru rezoluție

Exercițiile 1-5 sunt preluate din: Uwe Schöning, Logic for Computer Scientists, Birkhäuser, 1989

L1. Arătați că următoarea formulă nu e realizabilă:
∀ x ∀ y . (¬ P(x) ∨ ¬ P(f(a)) ∨ Q(y)) ∧ P(y) ∧ (¬ P(g(b, x)) ∨ ¬ Q(b))

L2. Arătați că următoarea mulțime de clauze nu e realizabilă:
¬ P(x) ∨ Q(x) ∨ R(x, f(x))
¬ P(x) ∨ Q(x) ∨ S(f(x))
T(a)
P(a)
¬ R(a,z) ∨ T(z)
¬ T(x) ∨ ¬ Q(x)
¬ T(y) ∨ ¬ S(y)

L3. Formalizați următoarele afirmații despre proprietățile unui grup algebric cu operația ⚪ , folosind predicatul P(x,y,z) pentru a reprezenta că z = x ⚪ y.
a) (rezolvat): ⚪ e o operație internă (rezultatul aparține grupului): ∀ x ∀ y ∃ z P(x, y, z)
b) ⚪ e o operație asociativă
c) ⚪ are element neutru la stânga și orice element are invers la stânga.
Demonstrați apoi prin rezoluție că există element neutru la dreapta și invers la dreapta.

L4. Exprimați în logica predicatelor:
a) Orice dragon e fericit dacă toți dragonii care sunt puii săi pot zbura.
b) Dragonii verzi pot zbura.
c) Un dragon e verde dacă e pui al unui dragon verde.
Arătați prin rezoluție că afirmațiile de mai sus implică: Toți dragonii verzi sunt fericiți.

L5. Exprimați în logica predicatelor:
a) Orice bărbier bărbierește toate persoanele care nu se bărbieresc pe sine.
b) Niciun bărbier nu bărbierește vreo persoană care se bărbierește pe sine.
Arătați prin rezoluție că ele implică: Nu există bărbieri.

L6. Arătați prin rezoluție: Dacă într-o relație binară simetrică și tranzitivă orice element e în relație cu măcar un element, atunci relația e reflexivă.

L7. Arătați prin rezoluție: O relatie ireflexivă și tranzitivă e asimetrică. (O relație R e asimetrică dacă oricând avem x R y nu avem și y R x).

L8. Formalizați afirmațiile (presupunând că un meci e fie câștigat fie pierdut, nu există meciuri egale).
A: Oricine a câștigat un meci a pierdut un meci.
B: Nimeni nu a câștigat toate meciurile.
E adevărat că B → A ? Demonstrați prin rezoluție.

L9. Formalizați afirmațiile:
A: Pentru orice film există un film care n-a fost văzut de toți care l-au văzut pe primul.
B: Orice film a fost văzut de cineva.
C: Cineva a văzut toate filmele.
E adevărat că A → B? Demonstrați sau infirmați prin rezoluție.
Pot fi adevărate simultan A, B și C? Demonstrați sau infirmați prin rezoluție.

Proprietăți de relații exprimate ca dicționare

C1. Folosind funcțiile standard exists și for_all pentru dicționare, exprimați următoarele proprietăți:
a) Dicționarul reprezintă funcția identitate
b) Orice valoare din dicționar apare și ca și cheie
c) Orice cheie din dicționar apare și ca valoare
d) Dicționarul reprezintă o permutare
e) Dicționarul reprezintă o permutare cu cel puțin un ciclu de lungime mai mare ca 2.
f) Două dicționare reprezintă unul inversul celuilalt
g) Dicționarul reprezintă o involuție (e propria sa inversă) Care din aceste proprietăți sunt legate între ele și cum? Argumentați.

Exerciții cu structura formulelor de ordinul I

În problemele de mai jos folosim următorul tip pentru termeni (un termen e fie o variabilă, fie o funcție de termeni; constantele sunt asimilate funcțiilor fără parametri) și respectiv formule cu predicate:
type term = V of string
            | F of string * term list
type predform = Pr of string * term list
                | Neg of predform
                | And of predform * predform
                | Or of predform * predform
                | Forall of string * predform
De exemplu, ∀ x ∀ y . P(x, y) ∧ (Q(f(x)) → ¬ R(y)) se reprezintă (după convertirea implicației) ca
Forall ("x", Forall("y", And (Pr("P", [V "x"; V "y"]), Or (Neg (Pr("Q", [F("f", [V "x"])])), Neg (Pr("R", [V "y"]))))))

C2. Tipărirea
a) Scrieti o funcție recursivă care tipărește un termen.
b) Folosind funcția de mai sus, scrieți o funcție care tipărește un predicat.
De exemplu, printterm (F ("f", [V "x"; F ("g", [F ("a", []); V "y"]) ])) va tipări f(x, g(a, y)).

C3. Variabile libere Scrieți o funcție care ia ca parametru o formulă în logica predicatelor și returnează mulțimea numelor tuturor variabilelor libere din formulă (o mulțime de șiruri).
De exemplu, freevars (And (Forall ("y", Pr("P", [V "x"; V "y"])), Forall ("x", Or (Pr("Q", [V "z"]), Pr("R", [V "x"]))))) e mulțimea {x, z}. Deși x e variabilă legată îm al doilea conjunct, ea e variabilă liberă în primul.

Indicație Pentru orice formulă structurată, mulțimea variabilelor libere e reuniunea mulțimilor pentru formulele componente. Pentru o formulă cu cuantificator, se exclude variabila cuantificată.

Scriem o funcție ajutătoare vars_of_term, întrucât atât un predicat, P(t1, t2, ... tn) și un termen-funcție f(t1, t2, ... tn) conțin o listă de termeni [t1; t2; ... tn] (argumentele), și fiecare din acești termeni poate avea (recursiv) argumente (o altă listă de termeni, etc.).
E util ca funcția vars_of_term să ia ca parametru suplimentar o mulțime inițială de variabile și să returneze, adăugată la aceasta, mulțimea variabilelor din termen.
Putem scrie două funcții mutual recursive folosind sintaxa let rec funcție1 = definiție1 and funcție2 = definiție2 în care fiecare definiție poate folosi ambele nume definite. Parametrul accset de mai jos e mulțimea la care se adaugă variabilele din termenul dat ca al doilea parametru:

let rec vars_of_term accset = function
  | V s -> ...
  | F (f, tlist) -> vars_of_termlist ...
and vars_of_termlist ... = List.fold_left ...
Vezi și problema C5, unde exemplul dat calculează mulțimea numelor de funcții, nu de variabile.
În final, scriem funcția dorită freevars care ia ca parametru o formulă și o prelucrează recursiv prin descompunere structurală, pe fiecare din variantele posibile.

C4. Cuantificare existențială Scrieți o funcție care ia ca parametru o formulă și tipărește pentru fiecare cuantificator existențial lista tuturor variabilelor cuantificate universal ai căror cuantificatori se aplică subformulei respective (adică în interiorul cărora se află cuantificatorul existențial).
Adăugați la tipul pentru formulă cu predicate o variantă pentru cuantificatorul existențial.
Această funcție e utilă pentru skolemizare, unde fiecare variabilă cuantificată existențial e înlocuită cu o funcție nouă având ca argumente toate variabilele corespunzătoare cuantificatorilor universali în interiorul cărora se află.
De exemplu, pentru formula ∀ x ∃ y . R(x, y) ∨ ∀ z ∃ t . P(x, t) ∧ S(y, z) pentru ∃ y se va tipări lista [x] iar pentru ∃ t, lista [x; z]. Cum nu s-a cerut decât tipărirea, funcția nu returnează un rezultat propriu-zis, ci va avea tipul unit (prin consecință, dacă expresiile din corpul funcției sunt apeluri la funcțiile print... care returnează unit).

Indicație Funcția va lua ca parametru suplimentar o listă (inițial vidă). La fiecare parcurgere a unui cuantificator universal, apelul recursiv se face adăugând la listă variabila cuantificată.

C5. Număr de parametri Scrieți o funcție care ia ca parametru o formulă și care verifică faptul că fiecare funcție și predicat din formulă e folosit(ă) consecvent cu același număr de parametri.
De exemplu, check_arity (And(Pr("P", [V "x"]), Pr("P", [V "y"; V "z"]))) va returna false, pentru că predicatul P apare odată cu un argument și odată cu două.
La fel și pentru Pr("P", [F ("f", [F ("f", [V "x"; V "y"])])]) care folosește f cu 1 și 2 argumente.

Indicație Rezolvăm întâi o problemă simplă similară: scriem o funcție care returnează mulțimea tuturor numelor de funcții dintr-un termen. Mai exact, funcția ia ca prim parametru o mulțime de nume, și returnează această mulțime la care adaugă toate numele de funcție din termen. Această reformulare ajută la aplicarea repetată pe o listă de termeni, ca în problema 2.
Numele de variabile nu ne interesează, deci în cazul de bază funcția returnează mulțimea dată ca parametru, fără nicio schimbare. Pentru o funcție, adăugăm numele funcției la mulțimea primită, și iterăm recursiv funcția peste toți termenii argument. Prelucrarea cu List.fold_left are ca efect transmiterea la fiecare pas mai departe a mulțimii actualizate.

let rec funnames m = function
  | V s -> m
  | F (f, tlist) -> List.fold_left funnames (S.add f m) tlist
Pentru problema cerută sunt necesare două funcții, una pentru fiecare tip: termen și formulă; ele lucrează similar. Fiecare din funcții ia ca parametru suplimentar nu o mulțime, ci un dicționar de la șiruri la întregi, care va memora pentru fiecare funcție/predicat din formulă numărul de argumente. La fiecare nume de funcție/predicat întâlnit, funcția nu va face doar o adăugare, ca în exemplul de mai sus, ci întăi verifică, în caz că numele e deja în dicționar, dacă numărul stocat de argumente corespunde cu cel al listei din termenul curent. Pentru noul dicționar vom avea deci o expresie de forma
try if nr. de argumente din dicționar <> nr. din listă then failwith "numar diferit" else dicționar nemodificat
with Not_found -> dicționar actualizat cu nume si nr. argumente

C6. Redenumiri Scrieți o funcție care ia ca parametru o formulă cu cuantificatori și redenumește fiecare variabilă legată, adăugând un sufix unic (de exemplu bazat pe un număr).
De exemplu, rename (And (Forall ("x", Exists ("y", Pr("P", [V "x"; V "y"]))), Forall ("x", Pr("Q", [V "x"; V "z"])))) va returna
And (Forall ("x_1", Exists ("y_2", Pr("P", [V "x_1"; V "y_2"]))), Forall ("x_3", Pr("Q", [V "x_3"; V "z"]))), numerotând cei trei cuantificatori și variabilele corespunzătoare. z nu e redenumită, fiind variabilă liberă.
Indicație Folosiți aceeași structură de cod ca la temele pentru formule propoziționale în care se numărau diverse elemente componente. În plus, similar cu problema anterioară, transmiteți la fiecare apel pentru o subformulă un parametru de tip dicționar (corespondență între nume vechi și nume nou), pentru a o putea redenumi consecvent. De exemplu, următoarea funcție redenumește variabilele conform dicționarului dat parametru și numără operatorii de negație.

let rencnt m =
  let rec rc1 n = function
    | V s -> (n, try V (M.find s m) with Not_found -> V s)
    | Neg e -> let (n1, r1) = rc1 (n+1) e in (n1, Neg r1)
    | And (e1, e2) -> let (n1, r1) = rc1 n e1 in
                      let (n2, r2) = rc1 n1 e2 in
                      (n2, And(r1, r2))
  in rc1 1
În rezolvarea problemei propuse, dicționarul trebuie actualizat la fiecare cuantificator, adăugând coresponența dintre numele vechi și nou al variabilei cuantificate. Numărul dat ca parametru se incrementează tot la fiecare cuantificator (nu la negație, ca în exemplu), pe baza lui generându-se noul nume. Pentru termeni, scriem o funcție separată: aici, dicționarul nu se modifică, doar se folosește; utilizăm List.map pentru a prelucra cu aceeași funcție lista de termeni-argument.
Marius Minea
Last modified: Tue Nov 14 8:40:00 EET 2017