Exersați scrierea unor formule în logica predicatelor. Folosiți demonstratorul Z3 dezvoltat la Microsoft pentru a determina dacă formula e realizabilă, obțineți în acest caz un model (adică o interpretare in care formula e adevărată).
Formulele sunt scrise în logica predicatelor. Sintactic, ele respectă standardul SMT-LIB 2.0 (care include și teorii formalizând aritmetica cu întregi, reali, etc), cu unele extensii specifice. Formulele pot fi introduse interactiv direct în pagina indicată. Dacă le salvați într-un fișier, folosiți extensia .smt2 corespunzătoare formatului.
O descriere în formatul SMT-LIB e o secvență de s-expresii (liste ierarhice, un format introdus de limbajul LISP), adică fie un atom (cuvânt, în cazul nostru identificator sau operator), fie o listă de expresii într-o paranteze ( ).
La început declarăm universul U al valorilor:
(declare-sort U)Se poate lucra cu mai multe sorturi (tipuri) disjuncte de valori, dar, la fel ca în logica propozițională clasică vom folosi unul singur.
Un predicat și o funcție se declară la fel:
(declare-fun nume (lista-tipuri-argumente) tip-rezultat)deoarece au aceeași structură sintactică: un nume cu o listă de argumente care pot fi termeni. Cum folosim un singur univers de valori U, toate argumentele vor fi de acest sort (tip). Predicatele au rezultatul de tip Bool, iar funcțiile de tip U. Deobicei, sorturile se scriu cu majusculă, celelalte nume cu litere mici, dar nu e o regulă impusă. De exemplu, (declare-fun f (U U) U) definește o funcție de două argumente, cu valori în același univers.
Formulele (expresiile) cu operatori se scriu tot ca s-expresii, operatorul fiind primul (format prefix):
(not expresie)
(=> expresie expresie)
(= expresie expresie)
iar and și or pot avea oricâte argumente: (and expr1 expr2 ... exprN).
Și predicatele și funcțiile se scriu în aceeași formă, deci pentru p(f(x), y) vom scrie (p (f x) y) (scrierea ne e deja familiară din ML).
Cuantificatorii universal (resp. existențial) se scriu sub forma
(forall ((x U)) expresie) (respectiv exists) ceea ce și
declară variabila x pentru a putea fi folosită în expresie.
Pentru mai multe variabile scriem (forall ((x U) (y U)) expresie) etc.
Atenție la parantezele dublate în jurul variabilelor cuantificate!
Vom folosi doar formule fără variabile libere, unde nu sunt necesare alte declarații de variabile.
Aserțiuni: Formulele de mai sus nu se scriu de sine stătător, ci se specifică cu sintaxa (assert formulă) . Dacă specificăm mai mult aserțiuni înseamnă că dorim ca toate să fie adevărate (ele devin deci legate prin conjuncție).
Realizabilitatea aserțiunilor indicate (deci a formulei rezultante ca și conjuncție) se verifică cu comanda (check-sat). Dacă formula e realizabilă, comanda (get-model) produce un model (un univers și o interpretare a funcțiilor pentru care formula e adevărată).
Mai jos e indicată formalizarea completă a exemplului de la curs cu investitorii și acțiunile (exemplul 9). S-a formalizat negația concluziei pentru a arăta că negația nu e realizabilă împreună cu ipotezele (formează o contradicție), deci concluzia e adevărată (rezultă din ipoteze).
(declare-sort U) (declare-fun buy (U U) Bool) (declare-fun stock (U) Bool) (declare-fun bond (U) Bool) (declare-fun crashDJ () Bool) (declare-fun gold (U) Bool) (declare-fun falls (U) Bool) (declare-fun raterise () Bool) (declare-fun happy (U) Bool) (assert (forall ((b U)) (exists ((o U)) (and (buy b o) (or (stock o) (bond o)))))) (assert (=> crashDJ (forall ((o U)) (=> (and (stock o) (not (gold o))) (falls o))))) (assert (=> raterise (forall ((o U)) (=> (bond o) (falls o))))) (assert (forall ((b U)) (=> (exists ((o U)) (and (buy b o) (falls o))) (not (happy b))))) (assert (not (=> (and crashDJ raterise) (forall ((b U)) (=> (happy b) (exists ((o U)) (and (buy b o) (stock o) (gold o)))))))) (check-sat)Vezi și două rezolvări pentru problema 10, cu unic univers, si cu trei sorturi diferite, ceea ce nu mai necesită predicate pentru categoriile respective, cuantificarea se face deja pe domeniul restrâns.
1. 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))
2. 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)
3. 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.
4. 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.
5. 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.
6. 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ă.