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ă.
Exersați scrierea unor formule în logica predicatelor și demonstrația prin rezoluție.
Exercițiile 1-5 sunt preluate din: Uwe Schöning, Logic for Computer Scientists, Birkhäuser, 1989
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ă.