PDF de programación - Logica en Haskell

Lógica en Haskell

José A. Alonso Jiménez

Grupo de Lógica Computacional
Dpto. de Ciencias de la Computación e Inteligencia Artificial
Universidad de Sevilla
Sevilla, 20 de Diciembre de 2007 (Versión de 24 de enero de 2008)

2

Esta obra está bajo una licencia Reconocimiento–NoComercial–CompartirIgual 2.5 Spain
de Creative Commons.

Se permite:

copiar, distribuir y comunicar públicamente la obra

hacer obras derivadas

Bajo las condiciones siguientes:

Reconocimiento. Debe reconocer los créditos de la obra de la manera espe-
cificada por el autor.

No comercial. No puede utilizar esta obra para fines comerciales.

Compartir bajo la misma licencia. Si altera o transforma esta obra, o genera
una obra derivada, sólo puede distribuir la obra generada bajo una licencia
idéntica a ésta.

Al reutilizar o distribuir la obra, tiene que dejar bien claro los términos de la licen-
cia de esta obra.

Alguna de estas condiciones puede no aplicarse si se obtiene el permiso del titular
de los derechos de autor.

Esto es un resumen del texto legal (la licencia completa). Para ver una copia de esta
licencia, visite http://creativecommons.org/licenses/by-nc-sa/2.5/es/ o envie una
carta a Creative Commons, 559 Nathan Abbott Way, Stanford, California 94305, USA.

Índice general

1. Sintaxis y semántica de la lógica proposicional

2. Formas normales y cláusulas

3. Cláusulas

4. Tableros semánticos proposicionales

5. Cálculo de secuentes proposicionales

6. El procedimiento de Davis y Putnam

7. Resolución proposicional

8. Refinamientos de resolución

9. Programación lógica proposicional

10. Unificación de términos de primer orden

11. Implementación de Prolog

A. Verificación de todos los programas

B. Resumen de funciones predefinidas de Haskell

3

5

19

29

45

55

67

79

85

103

113

123

135

137

4

Índice general

Capítulo 1

Sintaxis y semántica de la lógica
proposicional

module SintaxisSemantica where

-- ---------------------------------------------------------------------
-- Librerías auxiliares
--
-- ---------------------------------------------------------------------

import Data.List
import Test.HUnit
import Verificacion

-- ---------------------------------------------------------------------
-- Gramática de fórmulas prosicionales
--
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir los siguientes tipos de datos:
-- * SímboloProposicional para representar los símbolos de proposiciones
-- * Prop para representar las fórmulas proposicionales usando los
--
--
--
-- ---------------------------------------------------------------------

constructores Atom, Neg, Conj, Disj, Impl y Equi para las fórmulas
atómicas, negaciones, conjunciones, implicaciones y equivalencias,
respectivamente.

type SímboloProposicional = String

5

6

Capítulo 1. Sintaxis y semántica de la lógica proposicional

data Prop = Atom SímboloProposicional

| Neg Prop
| Conj Prop Prop
| Disj Prop Prop
| Impl Prop Prop
| Equi Prop Prop
deriving (Eq,Ord)

instance Show Prop where
= p
= "no " ++ show p

show (Atom p)
show (Neg p)
show (Conj p q) = "(" ++ show p ++ " /\\ " ++ show q ++ ")"
show (Disj p q) = "(" ++ show p ++ " \\/ " ++ show q ++ ")"
show (Impl p q) = "(" ++ show p ++ " --> " ++ show q ++ ")"
show (Equi p q) = "(" ++ show p ++ " <--> " ++ show q ++ ")"

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir las siguientes fórmulas proposicionales
-- atómicas: p, p1, p2, q, r, s, t y u.
-- ---------------------------------------------------------------------

p, p1, p2, q, r, s, t, u :: Prop
p
= Atom "p"
p1 = Atom "p1"
p2 = Atom "p2"
= Atom "q"
q
r
= Atom "r"
= Atom "s"
s
= Atom "t"
t
u
= Atom "u"

-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
--
-- tal que (no f) es la negación de f.
-- ---------------------------------------------------------------------

no :: Prop -> Prop

no :: Prop -> Prop
no = Neg

Capítulo 1. Sintaxis y semántica de la lógica proposicional

7

(/\), (\/), (-->), (<-->) :: Prop -> Prop -> Prop

-- ---------------------------------------------------------------------
-- Ejercicio 4: Definir los siguientes operadores
--
-- tales que
f /\ g
--
f \/ g
--
f --> g
--
--
f <--> g
-- ---------------------------------------------------------------------

es la conjunción de f y g
es la disyunción de f y g
es la implicación de f a g
es la equivalencia entre f y g

infixr 5 \/
infixr 4 /\
infixr 3 -->
infixr 2 <-->
(/\), (\/), (-->), (<-->) :: Prop -> Prop -> Prop
(/\)
= Conj
(\/)
= Disj
(-->)
= Impl
(<-->) = Equi

-- ---------------------------------------------------------------------
-- Símbolos proposicionales de una fórmula
--
-- ---------------------------------------------------------------------

símbolosPropFórm :: Prop -> [Prop]

-- ---------------------------------------------------------------------
-- Ejercicio 5: Definir la función
--
-- tal que (símbolosPropFórm f) es el conjunto formado por todos los
-- símbolos proposicionales que aparecen en f. Por ejemplo,
--
-- ---------------------------------------------------------------------

símbolosPropFórm (p /\ q --> p)

==> [p,q]

símbolosPropFórm :: Prop -> [Prop]
símbolosPropFórm (Atom f)
símbolosPropFórm (Neg f)
símbolosPropFórm (Conj f g) = símbolosPropFórm f `union` símbolosPropFórm g
símbolosPropFórm (Disj f g) = símbolosPropFórm f `union` símbolosPropFórm g
símbolosPropFórm (Impl f g) = símbolosPropFórm f `union` símbolosPropFórm g
símbolosPropFórm (Equi f g) = símbolosPropFórm f `union` símbolosPropFórm g

= [(Atom f)]
= símbolosPropFórm f

8

Capítulo 1. Sintaxis y semántica de la lógica proposicional

-- ---------------------------------------------------------------------
-- Interpretaciones
--
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 6: Definir el tipo de datos Interpretación para
-- representar las interpretaciones como listas de fórmulas atómicas.
-- ---------------------------------------------------------------------

type Interpretación = [Prop]

-- ---------------------------------------------------------------------
-- Significado de una fórmula en una interpretación
--
-- ---------------------------------------------------------------------

significado :: Prop -> Interpretación -> Bool

-- ---------------------------------------------------------------------
-- Ejercicio 7: Definir la función
--
-- tal que (significado f i) es el significado de f en i. Por ejemplo,
--
--
-- ---------------------------------------------------------------------

significado ((p \/ q) /\ ((no q) \/ r)) [r]
significado ((p \/ q) /\ ((no q) \/ r)) [p,r]

==>
==>

False
True

significado :: Prop -> Interpretación -> Bool
i = (Atom f) `elem` i
significado (Atom f)
significado (Neg f)
i = not (significado f i)
significado (Conj f g) i = (significado f i) && (significado g i)
significado (Disj f g) i = (significado f i) || (significado g i)
significado (Impl f g) i = significado (Disj (Neg f) g) i
significado (Equi f g) i = significado (Conj (Impl f g) (Impl g f)) i

-- ---------------------------------------------------------------------
-- Interpretaciones de una fórmula
--
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 8: Definir la función
--
subconjuntos :: [a] -> [[a]]
-- tal que (subconjuntos x) es la lista de los subconjuntos de x. Por
-- ejmplo,

Capítulo 1. Sintaxis y semántica de la lógica proposicional

9

subconjuntos "abc"

--
-- ---------------------------------------------------------------------

["abc","ab","ac","a","bc","b","c",""]

==>

subconjuntos :: [a] -> [[a]]
subconjuntos []
subconjuntos (x:xs) = [x:ys | ys <- xss] ++ xss

= [[]]

where xss = subconjuntos xs

interpretacionesFórm :: Prop -> [Interpretación]

-- ---------------------------------------------------------------------
-- Ejercicio 9: Definir la función
--
-- tal que (interpretacionesFórm f) es la lista de todas las
-- interpretaciones de f. Por ejemplo,
--
-- ---------------------------------------------------------------------

interpretacionesFórm (p /\ q --> p)

[[p,q],[p],[q],[]]

==>

interpretacionesFórm :: Prop -> [Interpretación]
interpretacionesFórm f = subconjuntos (símbolosPropFórm f)

-- ---------------------------------------------------------------------
-- Modelos de fórmulas
--
-- ---------------------------------------------------------------------

esModeloFórmula :: Interpretación -> Prop -> Bool

-- ---------------------------------------------------------------------
-- Ejercicio 10: Definir la función
--
-- tal que (esModeloFórmula i f) se verifica si i es un modelo de f. Por
-- ejemplo,
--
--
-- ---------------------------------------------------------------------

esModeloFórmula [r]
((p \/ q) /\ ((no q) \/ r))
esModeloFórmula [p,r] ((p \/ q) /\ ((no q) \/ r))

False
True

==>
==>

esModeloFórmula :: Interpretación -> Prop -> Bool
esModeloFórmula i f = significado f i

-- ---------------------------------------------------------------------
-- Ejercicio 11: Definir la función
--
-- tal que (modelosFórmula f) es la lista de todas las interpretaciones
-- de f que son modelo de F. Por ejemplo,

modelosFórmula :: Prop -> [Interpretación]

10

Capítulo 1. Sintaxis y semántica de la lógica proposicional

modelosFórmula ((p \/ q) /\ ((no q) \/ r))
==> [[p,q,r],[p,r],[p],[q,r]]

--
--
-- ---------------------------------------------------------------------

modelosFórmula :: Prop -> [Interpretación]
modelosFórmula f =

[i | i <- interpretacionesFórm f,

esModeloFórmula i f]

-- ---------------------------------------------------------------------
-- Fórmulas válidas, satisfacibles e insatisfacibles
--
-- -----