25 mai 2010

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

-}

Niciun comentariu: