Demonstrarea unui scop cf. unui set de clauze Horn

-- Un nucleu pentru demonstrarea unui scop conform unui set de clauze Horn.

-- Procedura de inferenta: rezolutie

-- Metoda de demonstrare: reducere la absurd

-- Strategie control: parcurgere in adincime a arborelui AND-OR al demonstratiei

-- CG mai, 2010

module Resolution where

data Subst a = VoidSubst | Bindings [(String,a)] deriving Show

solve goal all_props = solve' [goal] all_props VoidSubst where

solve' [] props subst = (True,subst) -- Frunza

solve' goals [] subst = (False,subst)

solve' (goal:goals) (prop:props) subst = -- nod OR

let (flag1,subst1) = unify goal (head prop) subst

in if flag1

then let (flag2,subst2) = solve' ((tail prop)++goals) all_props subst1 --nod AND

in if flag2 then (True,subst2)

else solve' (goal:goals) props subst

else solve' (goal:goals) props subst

unify term1 term2 subst = (term1==term2,VoidSubst)

--- O reprezentare simpla pentru termeni fara variabile

data Constant = Maria | Ion | Fred | Gigi deriving (Eq,Show)

data Predicate a = Iubeste a a | Human a | Prieten a a deriving (Eq,Show)

{-

1. Un termen este reprezentat ca un tuplu (predicat val1 val2 ... valn)

De exemplu tuplul (Iubeste Maria Ion) sta pentru iubeste(Maria,Ion)

2. O propozitie este o implicatie (clauza Horn) term1 ^ term2 ^ ... ^ termn => term, n>=1,

si este reprezentata prin lista [term, term1, term2, ..., termn]

De exemplu,

[Human Ion, Iubeste Maria Ion, Human Maria] sta pentru propozitia

iubeste(Maria,Ion) ^ human(Maria) => human(Ion)

3. Propozitia particulara True => term (axioma) este reprezentata prin term

De exemplu,

[Human Maria] sta pentru propozitia True => human(Maria)

4. Propozitiile sunt date ca o lista [prop1,prop2,...,propm]

-}

propozitii = [

[Human Maria],

[Human Ion, Iubeste Maria Ion, Human Maria],

[Human Fred, Human Ion, Prieten Ion Fred],

[Human Gigi],

[Prieten Ion Fred],

[Iubeste Maria Ion]

]

{-

solve (Human Ion) propozitii

solve (Human Fred) propozitii

solve (Human Gigi) propozitii

-}