Logica predicatelor - Tema 10

1. Rezoluție a) Formalizați în logica predicatelor unul din exemplele nerezolvate (11 - 23) de pe această pagină.
b) Transformați apoi atât ipotezele cât și negația concluziei în formă clauzală
c) Folosiți metoda rezoluției pentru a deriva clauza vidă.

Rezolvați problema pe hârtie sau într-un fișier în format text/HTML/PDF.
Dacă doriți indicații pentru rezoluție și să verificați dacă ați lucrat corect, puteți folosi versiunea web a demonstratorului de teoreme SPASS. Urmează explicații de folosire.
Aveți ca exemplu problema dragonului de la laboratorul 9, tradusă direct, și în formă clauzală (formă normală conjunctivă).
Prima parte conține câteva informații despre problemă. Treceți numărul problemei rezolvate și numele vostru.
Urmează lista predicatelor și funcțiilor folosite, fiecare cu numărul de argumente (o constantă e o funcție de zero argumente, o propoziție e un predicat cu zero argumente). Includeți funcțiile și constantele definite la skolemizare.
În varianta scrisă direct, am indicat în grupuri separate axiomele și concluziile (aici, una singură).
În forma clauzală, am indicat în secțiunea "conjectures" clauzele din negația concluziei. Alternativ, le-am putea include (în aceeași formă) în prima secțiune (axioms), și omite secțiunea a doua. Demonstrația găsită poate fi diferită.
Atenție, în forma CNF, folosirea lui or() e obligatorie, chiar pentru clauze cu un singur predicat.
În linia de deasupra butonului "Submit", introduceți opțiunea -DocProof pentru a obține o demonstrație detaliată cu pași numerotați.
În rezultat, apar întâi clauzele, de exemplu:
dragon(U) -> dragon(p(U))* fericit(U). Ignorați steluța și semnele ||. Formula se citește considerând negat predicatele din stânga implicației și pozitive cele din dreapta, legate prin disjuncție, deci:
¬ dragon(U) ∨ dragon(p(U)) ∨ fericit(U). Variabilele pot fi redenumite față de enunțul problemei: U, V, W, ...
În partea de jos, găsiți demonstrația (derivarea clauzei vide), cu pașii numerotați, de exemplu:

    3[0:Inp] dragon(U) || zboara(p(U))* -> fericit(U).
    4[0:Inp] verde(U) dragon(U) ||  -> zboara(U)*.
    17[0:Res:4.2,3.1] verde(p(U)) dragon(p(U)) dragon(U) ||  -> fericit(U)*.

Pasul 17 indică regula de rezoluție folosită (Res), și predicatele unificate: 4.2, adică predicatul 2 (numărat de la 0) din formula 4, deci zboara(U) cu 3.1, predicatul 1 din formula 3, deci ¬ zboara(p(U)). Țineți cont că variabilele din clauze sunt diferite, deci unificăm de fapt zboara(U1) cu ¬ zboara(p(U2)). Rezultatul e scris tot cu nume de variabilă începând de la U.
Puteți încerca să găsiți singuri pașii de rezoluție sau ajutându-vă de demonstrator; indicați însă explicit pe hârtie predicatele unificate și rezultatul.

2. Variabila apare în termen? În logica predicatelor, un termen e fie o variabilă, fie o funcție de termeni (constantele sunt asimilate funcțiilor fără parametri)

type term = V of string
            | F of string * term list

Scrieți o funcție care primește un nume de variabilă și un termen și determină (returnează adevărat/fals) dacă variabila respectivă apare sau nu în termen.
Această funcție e utilă pentru unificare/substituție (nu putem unifica o variabilă cu un termen care o conține, pentru că prin substituție s-ar obține un termen infinit).
De exemplu, apare "x" (F("f", [V "y"; F("g", [V "x"])])) = true, variabila x apare în termenul f(y, g(x)). Dacă am verifica pentru numele de variabilă z am obține false.

Marius Minea

Last modified: Sat Nov 28 12:00:00 EET 2015