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.

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

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

Exerciții cu structura formulelor de ordinul I

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

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 ...

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

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