Una FNC (fórmula en forma normal conjuntiva) es una conjunción de cláusulas, donde una cláusula es una disyunción de literales y un literal es un átomo o su negación. Por ejemplo,

(x(1) v -x(3)) & x(2) & (-x(2) v x(3) v x(1))

es una FNC con tres clásulas tales que la primera cláusula tiene 2 literales (x(1) y -x(3)), la segunda tiene 1 (x(2)) y la tercera tiene 3 (-x(2), x(3) y x(1)).

Usaremos las siguientes representaciones:

• Los átomos se representan por enteros positivos. Por ejemplo, 3 representa x(3).
• Los literales se representan por enteros. Por ejemplo, 3 representa el literal positivo x(3) y -5 el literal negativo -x(5).
• Una cláusula es una lista de literales que representa la disyunción se sus literales. Por ejemplo, [3,2,-4] representa a (x(3) v x(2) v -x(4)).
• Una fórmula en forma normal conjuntiva (FNC) es una lista de cláusulas que representa la conjunción de sus cláusulas. Por ejemplo, [[3,2],[-1,2,5]] representa a ((x(3) v x(2)) & (-x(1) v x(2) v x(5))).

Una interpretación I es un conjunto de átomos. Se supone que los átomos de I son verdaderos y los restantes son falsos. Por ejemplo, en la interpretación [2,5]

• el literal x(2) es verdadero (porque 2 ∈ [2,5])
• el literal x(3) es falso (porque 3 ∉ [2,5])
• el literal -x(4) es verdadero (porque 4 ∉ [2,5])
• la cláusula (x(2) v x(3)) es verdadera (porque x(2) es verdadero)
• la cláusula (x(3) v x(4)) es falsa (porque x(3) y x(4) son falsos)
• la FNC ((x(2) v x(5)) & (-x(4) v x(3)) es verdadera porque lo son sus dos cláusulas

En el ejercicio se usarán los siguientes tipos de datos

type Atomo          = Int
type Literal        = Int
type Clausula       = [Literal]
type FNC            = [Clausula]
type Interpretacion = [Atomo]

Definir las siguientes funciones

valorLiteral  :: Interpretacion -> Literal -> Bool
valorClausula :: Interpretacion -> Clausula -> Bool
valor         :: Interpretacion -> FNC -> Bool

tales que

• (valorLiteral i l) es el valor del literal l en la interpretación i. Por ejemplo,

valorLiteral [3,5] 3     ==  True
valorLiteral [3,5] 4     ==  False
valorLiteral [3,5] (-3)  ==  False
valorLiteral [3,5] (-4)  ==  True

• (valorClausula i c) es el valor de la cláusula c en la interpretación i. Por ejemplo,

valorClausula [3,5] [2,3,-5]  ==  True
valorClausula [3,5] [2,4,-1]  ==  True
valorClausula [3,5] [2,4,1]   ==  False

• (valor i f) es el valor de la fórmula en FNC f en la interpretación i. Por ejemplo,

valor [1,3] [[1,-2],[3]]  ==  True
valor [1]   [[1,-2],[3]]  ==  False
valor [1]   []            ==  True

Nota: Escribir la solución en el módulo Evaluacion_de_FNC para poderlo usar en los siguientes ejercicios.

Soluciones

module Evaluacion_de_FNC where

type Atomo          = Int
type Literal        = Int
type Clausula       = [Literal]
type FNC            = [Clausula]
type Interpretacion = [Atomo]

-- Definición de valorLiteral
-- ==========================

valorLiteral :: Interpretacion -> Literal -> Bool
valorLiteral i l
  | l > 0     = l `elem` i
  | otherwise = negate l `notElem` i

-- Definiciones de valorClausula
-- =============================

-- 1ª definición
valorClausula :: Interpretacion -> Clausula -> Bool
valorClausula i c = or [valorLiteral i l | l <- c]

-- 2ª definición
valorClausula2 :: Interpretacion -> Clausula -> Bool
valorClausula2 i = any (valorLiteral i)

-- Definiciones de valor de FNC
-- ============================

-- 1ª definición
valor :: Interpretacion -> FNC -> Bool
valor i f = and [valorClausula i c | c <- f]

-- 2ª definición
valor2 :: Interpretacion -> FNC -> Bool
valor2 i = all (valorClausula i)