Menu Close

Categoría: RA2019

RA2019: Demostración en Isabelle de la corrección de un compilador

En la primera parte de la clase de hoy del curso de Razonamiento automático se ha estudiado cómo demostrar en Isabelle la corrección de un compilador de expresiones aritméticas.

La clase se ha basado en la siguiente teoría Isabelle

chapter ‹Tema 10: Caso de estudio: Compilación de expresiones›
 
theory T10_Caso_de_estudio_Compilacion_de_expresiones
 
imports Main
begin
 
text ‹El objetivo de este tema es contruir un compilador de expresiones
  genéricas (construidas con variables, constantes y operaciones
  binarias) a una máquina de pila y demostrar su corrección.›
 
section ‹Las expresiones y el intérprete›
 
text ‹Definición. Las expresiones son las constantes, las variables
  (representadas por números naturales) y las aplicaciones de operadores
  binarios a dos expresiones.›
 
type_synonym 'v binop = "'v ⇒ 'v ⇒ 'v"
 
datatype 'v expr = 
  Const 'v 
| Var nat 
| App "'v binop" "'v expr" "'v expr" 
 
text ‹Definición. [Intérprete] 
  La función "valor" toma como argumentos una expresión y un entorno
  (i.e. una aplicación de las variables en elementos del lenguaje) y
  devuelve el valor de la expresión en el entorno.›
 
fun valor :: "'v expr ⇒ (nat ⇒ 'v) ⇒ 'v" where
  "valor (Const b)     ent = b"
| "valor (Var x)       ent = ent x"
| "valor (App f e1 e2) ent = (f (valor e1 ent) (valor e2 ent))"
 
text ‹Ejemplo. A continuación mostramos algunos ejemplos de evaluación 
  con el intérprete.›
 
lemma 
  "valor (Const 3) id = 3 ∧
   valor (Var 2) id = 2 ∧
   valor (Var 2) (λx. x+1) = 3 ∧ 
   valor (App (+) (Const 3) (Var 2)) (λx. x+1) = 6 ∧
   valor (App (+) (Const 3) (Var 2)) (λx. x+4) = 9" 
  by simp
 
section ‹La máquina de pila›
 
text ‹Nota. La máquina de pila tiene tres clases de intrucciones:
  · cargar en la pila una constante,
  · cargar en la pila el contenido de una dirección y
  · aplicar un operador binario a los dos elementos superiores de la 
    pila.›
 
datatype 'v instr = 
  IConst 'v 
| ILoad nat 
| IApp "'v binop"
 
text ‹Definición. [Ejecución]
  La ejecución de la máquina de pila se modeliza mediante la función 
  "ejec" que toma una lista de intrucciones, una memoria (representada 
  como una función de las direcciones a los valores, análogamente a los 
  entornos) y una pila (representada como una lista) y devuelve la pila
  al final de la ejecución.›
 
fun ejec :: "'v instr list ⇒ (nat ⇒ 'v) ⇒ 'v list ⇒ 'v list" where
  "ejec []     ent vs = vs"
| "ejec (i#is) ent vs = 
     (case i of
        IConst v ⇒ ejec is ent (v#vs)
      | ILoad x  ⇒ ejec is ent ((ent x)#vs)
      | IApp f   ⇒ ejec is ent ((f (hd vs) (hd (tl vs)))#(tl(tl vs))))"
 
text ‹  A continuación se muestran ejemplos de ejecución.›
 
lemma
  "ejec [IConst 3]          id                  [7] = [3,7] ∧
   ejec [ILoad 2, IConst 3] id                  [7] = [3,2,7] ∧
   ejec [ILoad 2, IConst 3] (λx. x+4)           [7] = [3,6,7] ∧
   ejec [ILoad 2, IConst 3, IApp (+)] (λx. x+4) [7] = [9,7]"
  by simp
 
section ‹El compilador›
 
text ‹Definición. El compilador "comp" traduce una expresión en una 
  lista de instrucciones.›
 
fun comp :: "'v expr ⇒ 'v instr list" where
  "comp (Const v)     = [IConst v]"
| "comp (Var x)       = [ILoad x]"
| "comp (App f e1 e2) = (comp e2) @ (comp e1) @ [IApp f]"
 
text ‹A continuación se muestran ejemplos de compilación.›
 
lemma
  "comp (Const 3)                   = [IConst 3] ∧
   comp (Var 2)                     = [ILoad 2] ∧
   comp (App (+) (Const 3) (Var 2)) = [ILoad 2, IConst 3, IApp (+)]"
  by simp
 
section ‹Corrección del compilador›
 
text ‹Para demostrar que el compilador es correcto, probamos que el
  resultado de compilar una expresión y a continuación ejecutarla es lo
  mismo que interpretarla; es decir,›
 
theorem "ejec (comp e) ent [] = [valor e ent]" 
  apply (induct e)
    apply auto
  oops
 
text ‹El teorema anterior no puede demostrarse por inducción en e. Para
  demostrarlo, lo generalizamos a›
 
theorem "∀vs. ejec (comp e) ent vs = (valor e ent)#vs"
  oops
 
text ‹En la demostración del teorema anterior usaremos el siguiente 
  lema.›
 
lemma
  "∀ vs. ejec (xs@ys) ent vs = ejec ys ent (ejec xs ent vs)" (is "?P xs")
proof (induct xs)
  show "?P []" by simp
next
  fix a xs
  assume "?P xs"
  then show "?P (a#xs)" by (cases "a", auto)
qed
 
― ‹La demostración estructurada es› 
lemma 
  "∀ vs. ejec (xs@ys) ent vs = ejec ys ent (ejec xs ent vs)" 
proof (induct xs)
  case Nil
  then show ?case 
    by simp
next
  case (Cons a xs)
  then show ?case 
    by (cases "a"; simp)
qed
 
― ‹La demostración detallada es› 
lemma 
  "∀ vs. ejec (xs@ys) ent vs = ejec ys ent (ejec xs ent vs)" (is "?P xs")
proof (induct xs)
  show "?P []" by simp
next
  fix a xs
  assume HI: "?P xs"
  then show "?P (a#xs)"
  proof (cases "a")
    case (IConst x1)
    then show ?thesis using HI by simp
  next
    case (ILoad x2)
    then show ?thesis using HI by simp
  next
    case (IApp x3)
    then show ?thesis using HI by simp
  qed
qed
 
― ‹Una demostración más detallada del lema es la siguiente:›
lemma ejec_append:
  "∀vs. ejec (xs@ys) ent vs = ejec ys ent (ejec xs ent vs)" (is "?P xs")
proof (induct xs)
  show "?P []" by simp
next
  fix a xs
  assume HI: "?P xs"
  then show "?P (a#xs)"
  proof (cases "a")
    fix v 
    assume C1: "a = IConst v"
    show " ∀vs. ejec ((a#xs)@ys) ent vs = ejec ys ent (ejec (a#xs) ent vs)"
    proof
      fix vs
      have "ejec ((a#xs)@ys) ent vs = ejec (((IConst v)#xs)@ys) ent vs"
        using C1 by simp
      also have "… = ejec (xs@ys) ent (v#vs)" 
        by simp
      also have "… = ejec ys ent (ejec xs ent (v#vs))" 
        using HI by simp
      also have "… = ejec ys ent (ejec ((IConst v)#xs) ent vs)" 
        by simp
      also have "… = ejec ys ent (ejec (a#xs) ent vs)" using C1 
        by simp
      finally show "ejec ((a#xs)@ys) ent vs = 
                    ejec ys ent (ejec (a#xs) ent vs)" .
    qed
  next
    fix n 
    assume C2: "a=ILoad n"
    show " ∀vs. ejec ((a#xs)@ys) ent vs = ejec ys ent (ejec (a#xs) ent vs)"
    proof
      fix vs
      have "ejec ((a#xs)@ys) ent vs = ejec (((ILoad n)#xs)@ys) ent vs"
        using C2 by simp
      also have "… = ejec (xs@ys) ent ((ent n)#vs)" 
        by simp
      also have "… = ejec ys ent (ejec xs ent ((ent n)#vs))" 
        using HI by simp
      also have "… = ejec ys ent (ejec ((ILoad n)#xs) ent vs)" 
        by simp
      also have "… = ejec ys ent (ejec (a#xs) ent vs)" 
        using C2 by simp
      finally show "ejec ((a#xs)@ys) ent vs = 
                    ejec ys ent (ejec (a#xs) ent vs)" .
    qed
  next
    fix f 
    assume C3: "a=IApp f"
    show "∀vs. ejec ((a#xs)@ys) ent vs = ejec ys ent (ejec (a#xs) ent vs)"
    proof
      fix vs
      have "ejec ((a#xs)@ys) ent vs = ejec (((IApp f)#xs)@ys) ent vs"
        using C3 by simp
      also have "… = ejec (xs@ys) ent ((f (hd vs) (hd (tl vs)))#(tl(tl vs)))" 
        by simp
      also have "… = ejec ys 
                          ent 
                          (ejec xs ent ((f (hd vs) (hd (tl vs)))#(tl(tl vs))))" 
        using HI by simp
      also have "… = ejec ys ent (ejec ((IApp f)#xs) ent vs)" 
        by simp
      also have "… = ejec ys ent (ejec (a#xs) ent vs)" 
        using C3 by simp
      finally show "ejec ((a#xs)@ys) ent vs = 
                    ejec ys ent (ejec (a#xs) ent vs)" .
    qed
  qed
qed
 
text ‹La demostración automática del teorema es›
 
theorem "∀vs. ejec (comp e) ent vs = (valor e ent)#vs"
  by (induct e) (auto simp add: ejec_append)
 
text ‹La demostración estructurada del teorema es›
theorem "∀vs. ejec (comp e) ent vs = (valor e ent)#vs"
proof (induct e)
  case (Const x)
  then show ?case by simp
next
  case (Var x)
  then show ?case by simp
next
  case (App x1a e1 e2)
  then show ?case by (simp add: ejec_append)
qed
 
text ‹La demostración detallada del teorema es›
theorem "∀vs. ejec (comp e) ent vs = (valor e ent)#vs"
proof (induct e)
  fix v
  show "∀vs. ejec (comp (Const v)) ent vs = (valor (Const v) ent)#vs" 
    by simp
next
  fix x
  show "∀vs. ejec (comp (Var x)) ent vs = (valor (Var x) ent) # vs" 
    by simp
next
  fix f e1 e2
  assume HI1: "∀vs. ejec (comp e1) ent vs = (valor e1 ent) # vs"
    and HI2: "∀vs. ejec (comp e2) ent vs = (valor e2 ent) # vs"
  show "∀vs. ejec (comp (App f e1 e2)) ent vs = 
             (valor (App f e1 e2) ent) # vs"
  proof
    fix vs
    have "ejec (comp (App f e1 e2)) ent vs
          = ejec ((comp e2) @ (comp e1) @ [IApp f]) ent vs" 
      by simp
    also have "… = ejec ((comp e1) @ [IApp f]) ent (ejec (comp e2) ent vs)"
      using ejec_append by blast
    also have "… = ejec [IApp f] 
                         ent 
                         (ejec (comp e1) ent (ejec (comp e2) ent vs))" 
      using ejec_append by blast
    also have "… =  ejec [IApp f] ent (ejec (comp e1) ent ((valor e2 ent)#vs))"
      using HI2 by simp
    also have "… = ejec [IApp f] ent ((valor e1 ent)#((valor e2 ent)#vs))"
      using HI1 by simp
    also have "… = (f (valor e1 ent) (valor e2 ent))#vs" by simp
    also have "… = (valor (App f e1 e2) ent) # vs" by simp
    finally 
    show "ejec (comp (App f e1 e2)) ent vs = (valor (App f e1 e2) ent) # vs" 
      by blast
  qed
qed
 
end

RA2019: Reducción de SAT a Clique en Haskell

En la segunda parte de la clase de hoy del curso de Razonamiento automático se ha estudiado una implementación de la reducción del problema SAT al problema Clique.

En primer lugar se ha estudiado una implementación del problema del Clique en la que se ha definido los grafos no ordenados (como pares de nodos), los cliques y cómo calcular los clique de un tamaño dado.

A continuación se ha estudiado cómo asociar a una fórmula en forma normal conjuntiva un grafo tal que la fórmula es satisfacible si, y sólo si, el grafo tiene un clique cuyo tamaño sea el número de cláusulas de la fórmula

Los códigos usados en la presentación son los siguientes:

Código del prolblema del Clique

-- Cliques.hs
-- El problema del clique.
-- José A. Alonso Jiménez
-- Sevilla, 6 de febrero de 2020
-- ---------------------------------------------------------------------
 
module Cliques where
 
import Data.List
 
-- ---------------------------------------------------------------------
-- Un grafo no dirigido se representa por la lista de sus arcos. Por
-- ejemplo, el grafo
--              1  -- 2 -- 4
--                    | \  |
--                    |  \ |
--                    3 -- 5
-- se representa por [(1,2),(2,3),(2,4),(2,5),(3,5),(4,5)].
 
--
-- Definir el tipo Grafo.
-- ---------------------------------------------------------------------
 
type Grafo a = [(a,a)]
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    nodos :: Eq a => Grafo a -> [a]
-- tal que (nodos g) es la lista de los nodos del grafo g. Por ejemplo,
--    nodos [(1,2),(2,3),(2,4),(2,5),(3,5),(4,5)]  ==  [1,2,3,4,5]
-- ---------------------------------------------------------------------
 
nodos :: Eq a => Grafo a -> [a]
nodos g = nub (concat [[x,y] | (x,y) <- g])
 
-- ---------------------------------------------------------------------
-- Ejercicio: Definir la función
--    conectados :: Eq a => Grafo a -> a -> a -> Bool
-- tal que (conectados g x y) se verifica si el grafo no dirigido g
-- posee un arco con extremos x e y. Por ejemplo,
--    conectados [(1,2),(2,3),(2,4),(2,5),(3,5),(4,5)] 3 2  ==  True
--    conectados [(1,2),(2,3),(2,4),(2,5),(3,5),(4,5)] 2 3  ==  True
--    conectados [(1,2),(2,3),(2,4),(2,5),(3,5),(4,5)] 3 4  ==  False
-- ---------------------------------------------------------------------
 
conectados :: Eq a => Grafo a -> a -> a -> Bool
conectados g x y =
  (x,y) `elem` g || (y,x) `elem` g 
 
-- ---------------------------------------------------------------------
-- Ejercicio: Definir la función
--    parejas :: [a] -> [(a,a)]
-- tal que (parejas xs) es la lista de las parejas formados por los
-- elementos de xs y sus siguientes en xs. Por ejemplo,
--    parejas [1..4] == [(1,2),(1,3),(1,4),(2,3),(2,4),(3,4)]
-- ---------------------------------------------------------------------
 
parejas :: [a] -> [(a,a)]
parejas xs =
  [(x,y) | (x:ys) <- tails xs
         , y <- ys]
 
-- ---------------------------------------------------------------------
-- Ejercicio. Un clique (en español, pandilla) de un grafo g es un
-- conjunto de nodos de g tal que todos sus elementos están conectados
-- en g.
--
-- Definir la función
--    esClique :: Eq a => Grafo a -> [a] -> Bool
-- tal que (esClique g xs) se verifica si el conjunto de nodos xs del
-- grafo g es un clique de g.Por ejemplo,
--    esClique [(1,2),(2,3),(2,4),(2,5),(3,5),(4,5)] [2,3,5]  ==  True
--    esClique [(1,2),(2,3),(2,4),(2,5),(3,5),(4,5)] [2,3,4]  ==  False
-- ---------------------------------------------------------------------
 
esClique :: Eq a => Grafo a -> [a] -> Bool
esClique g xs =
  and [conectados g x y | (x,y) <- parejas xs]
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    cliques :: Eq a => Grafo a -> [[a]]
-- tal que (cliques g) es la lista de los cliques del grafo g. Por
-- ejemplo, 
--    λ> cliques [(1,2),(2,3),(2,4),(2,5),(3,5),(4,5)]
--    [[],[1],[2],[1,2],[3],[2,3],[4],[2,4],
--     [5],[2,5],[3,5],[2,3,5],[4,5],[2,4,5]]
-- ---------------------------------------------------------------------
 
cliques :: Eq a => Grafo a -> [[a]]
cliques g =
  [xs | xs <- subsequences (nodos g)
      , esClique g xs]
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función 
--    kSubconjuntos :: [a] -> Int -> [[a]]
-- tal que (kSubconjuntos xs k) es la lista de los subconjuntos de xs
-- con k elementos. Por ejemplo,
--    ghci> kSubconjuntos "bcde" 2
--    ["bc","bd","be","cd","ce","de"]
--    ghci> kSubconjuntos "bcde" 3
--    ["bcd","bce","bde","cde"]
--    ghci> kSubconjuntos "abcde" 3
--    ["abc","abd","abe","acd","ace","ade","bcd","bce","bde","cde"]
-- ---------------------------------------------------------------------
 
kSubconjuntos :: [a] -> Int -> [[a]]
kSubconjuntos _ 0      = [[]]
kSubconjuntos [] _     = []
kSubconjuntos (x:xs) k = 
  [x:ys | ys <- kSubconjuntos xs (k-1)] ++ kSubconjuntos xs k  
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    kCliques :: Eq a => Grafo a -> Int -> [[a]]
-- tal que (cliques g k) es la lista de los cliques del grafo g de
-- tamaño k. Por ejemplo, 
--    λ> kCliques [(1,2),(2,3),(2,4),(2,5),(3,5),(4,5)] 3
--    [[2,3,5],[2,4,5]]
--    λ> kCliques [(1,2),(2,3),(2,4),(2,5),(3,5),(4,5)] 2
--    [[1,2],[2,3],[2,4],[2,5],[3,5],[4,5]]
-- ---------------------------------------------------------------------
 
-- 1ª definición
kCliques1 :: Eq a => Grafo a -> Int -> [[a]]
kCliques1 g k =
  [xs | xs <- cliques g
      , length xs == k]
 
-- 2ª definición
kCliques :: Eq a => Grafo a -> Int -> [[a]]
kCliques g k =
  [xs | xs <- kSubconjuntos (nodos g) k
      , esClique g xs]
 
-- Comparación de eficiencia
-- =========================
 
--    λ> kCliques1 [(n,n+1) | n <- [1..20]] 3
--    []
--    (4.28 secs, 3,204,548,608 bytes)
--    λ> kCliques [(n,n+1) | n <- [1..20]] 3
--    []
--    (0.01 secs, 3,075,768 bytes)

Código de la reducción de SAT a Clique

-- SAT_Clique.hs
-- Reducción de SAT a Clique.
-- José A. Alonso Jiménez
-- Sevilla, 6 de febrero de 2020
-- ---------------------------------------------------------------------
 
module SAT_Clique where
 
import SAT
import Cliques
import Data.List
import Test.QuickCheck
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    nodosFNC :: FNC -> [(Int,Literal)]
-- tal que (nodosFNC f) es la lista de los literales de las cláuslas de
-- f junto con el número de la cláusula. Por ejemplo,
--    λ> nodosFNC [[1,-2,3],[-1,2],[-2,3]]
--    [(0,1),(0,-2),(0,3),(1,-1),(1,2),(2,-2),(2,3)]
-- ---------------------------------------------------------------------
 
nodosFNC :: FNC -> [(Int,Literal)]
nodosFNC f = 
  [(i,x) | (i,xs) <- zip [0..] f
         , x <- xs]
 
-- ---------------------------------------------------------------------
-- Ejercicio. El grafo correspondiente a una fórmula f en FNC tiene como
-- nodos (nodosFNC f). Hay un arco entre los nodos correspondientes a
-- cláusulas distintas cuyos literales no son complementarios. Por
-- ejemplo, 
-- 
-- Definir la función
--    grafoFNC :: FNC -> Grafo (Int,Literal)
-- tal que (grafo FNC f) es el grafo de f. Por ejemplo, 
--    λ> grafoFNC [[1,-2,3],[-1,2],[-2,3]]
--    [ ((0,1),(1,2)),  ((0,1),(2,-2)), ((0,1),(2,3)),
--      ((0,-2),(1,-1)),((0,-2),(2,-2)),((0,-2),(2,3)),
--      ((0,3),(1,-1)), ((0,3),(1,2)),  ((0,3),(2,-2)),((0,3),(2,3)),
--      ((1,-1),(2,-2)),((1,-1),(2,3)),
--      ((1,2),(2,3))]
--    λ> grafoFNC [[1,2],[1,-2],[-1,2],[-1,-2]]
--    [((0,1),(1,1)),((0,1),(1,-2)),((0,1),(2,2)),((0,1),(3,-2)),
--     ((0,2),(1,1)),((0,2),(2,-1)),((0,2),(2,2)),((0,2),(3,-1)),
--     ((1,1),(2,2)),((1,1),(3,-2)),
--     ((1,-2),(2,-1)),((1,-2),(3,-1)),((1,-2),(3,-2)),
--     ((2,-1),(3,-1)),((2,-1),(3,-2)),
--     ((2,2),(3,-1))]
-- ---------------------------------------------------------------------
 
grafoFNC :: FNC -> Grafo (Int,Literal)
grafoFNC f = 
  [ ((i,x),(i',x'))
  | ((i,x),(i',x')) <- parejas (nodosFNC f)
  , i' /= i
  , x' /= complementario x]
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    cliquesFNC :: FNC -> [[(Int,Literal)]]
-- tal que (cliquesFNCf) es la lista de los cliques del grafo de f. Por
-- ejemplo, 
--    λ> cliquesFNC [[1,-2,3],[-1,2],[-2,3]]
--    [[], [(0,1)], [(1,2)], [(0,1),(1,2)], [(2,-2)],
--     [(0,1),(2,-2)], [(2,3)], [(0,1),(2,3)], [(1,2),(2,3)],
--     [(0,1),(1,2),(2,3)], [(0,-2)], [(2,-2),(0,-2)], [(2,3),(0,-2)],
--     [(1,-1)], [(2,-2),(1,-1)], [(2,3),(1,-1)], [(0,-2),(1,-1)],
--     [(2,-2),(0,-2),(1,-1)], [(2,3),(0,-2),(1,-1)], [(0,3)],
--     [(1,2),(0,3)], [(2,-2),(0,3)], [(2,3),(0,3)],
--     [(1,2),(2,3),(0,3)], [(1,-1),(0,3)],
--     [(2,-2),(1,-1),(0,3)], [(2,3),(1,-1),(0,3)]]
-- ---------------------------------------------------------------------
 
cliquesFNC :: FNC -> [[(Int,Literal)]]
cliquesFNC f = cliques (grafoFNC f)
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    cliquesCompletos :: FNC -> [[(Int,Literal)]]
-- tal que (cliquesCompletos f) es la lista de los cliques del grafo de
-- f que tiene elmismo número de elementos que el número de cláusulas de
-- f. Por ejemplo,
--    λ> cliquesCompletos [[1,-2,3],[-1,2],[-2,3]]
--    [[(0,1),(1,2),(2,3)],   [(2,-2),(0,-2),(1,-1)],
--     [(2,3),(0,-2),(1,-1)], [(1,2),(2,3),(0,3)],
--     [(2,-2),(1,-1),(0,3)], [(2,3),(1,-1),(0,3)]]
--    λ> cliquesCompletos [[1,2],[1,-2],[-1,2],[-1,-2]]
--    []
-- ---------------------------------------------------------------------
 
cliquesCompletos :: FNC -> [[(Int,Literal)]]
cliquesCompletos cs = kCliques (grafoFNC cs) (length cs)
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    esSatisfaciblePorClique :: FNC -> Bool
-- tal que (esSatisfaciblePorClique f) se verifica si f no contiene la
-- cláusula vacía, tiene má de una cláusula y posee algún clique
-- completo. Por ejemplo, 
--    λ> esSatisfaciblePorClique [[1,-2,3],[-1,2],[-2,3]]
--    True
--    λ> esSatisfaciblePorClique [[1,2],[1,-2],[-1,2],[-1,-2]]
--    False
-- ---------------------------------------------------------------------
 
esSatisfaciblePorClique :: FNC -> Bool
esSatisfaciblePorClique f =
     [] `notElem` f'
  && (length f' <= 1 || not (null (cliquesCompletos f')))
  where f' = nub (map (nub . sort) f) 
 
-- ---------------------------------------------------------------------
-- Ejercicio. Comprobar con QuickCheck que toda fórmula es satisfacible
-- si, y solo si, es satisfacible por Clique.
-- ---------------------------------------------------------------------
 
prop_esSatisfaciblePorClique :: FNC -> Bool
prop_esSatisfaciblePorClique f =
  esSatisfacible f == esSatisfaciblePorClique f
 
-- La comprobación es
--    λ> quickCheckWith (stdArgs {maxSize=7}) prop_esSatisfaciblePorClique
--    +++ OK, passed 100 tests.
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    modelosCliqueFNC :: FNC -> [Interpretacion]
-- tales que (modelosCliqueFNC f) es la lista de los modelos de f
-- calculados mediante los cliques completos del grafo de f. Por ejemplo,
--    λ> modelosCliqueFNC [[1,-2,3],[-1,2],[-2,3]]
--    [[],[1,2,3],[2,3],[3]]
--    λ> modelosCliqueFNC [[1,-2,3],[3,2],[-2,3]]
--    [[1,2,3],[1,3],[2,3],[3]]
-- ---------------------------------------------------------------------
 
modelosCliqueFNC :: FNC -> [Interpretacion]
modelosCliqueFNC f 
  | [] `elem` f'   = []
  | length f' == 1 = [[a | c <- f', a <- c, a > 0]]
  |otherwise       = sort (nub (map nub [ modeloClique xs
                                        | xs <- cliquesCompletos f]))
  where f' = nub (map (nub . sort) f) 
        modeloClique xs = [x | (_,x) <- xs, x > 0]
 
-- ---------------------------------------------------------------------
-- Ejercicio. Comprobar con QuickCheck que, para toda fórmula f en FNC,
-- todos los elementos de (modelosCliqueFNC f) son modelos de f.
-- ---------------------------------------------------------------------
 
prop_modelosPorClique :: FNC -> Bool
prop_modelosPorClique f =
  and [esModelo i f | i <- modelosCliqueFNC f]
 
-- La comprobación es
--    λ> quickCheckWith (stdArgs {maxSize=7}) prop_modelosPorClique
--    +++ OK, passed 100 tests.

RA2019: El algoritmo de Davis-Putnam en Haskell

En la primera parte de la clase de hoy del curso de Razonamiento automático se ha estudiado una implementación del algoritmo de Davis-Putnam en Haskell y comprobado su corrección con QuickCheck.

En primer lugar se ha estudiado una implementación de la lógica clausal en Haskell en la que se han definido los átomos, literales, cláusulas, fórmulas en forma normal conjuntiva (FNC), interpretaciones, modelos y la clasificación de FNC en satisfacibles, insatisfacibles y válidas.

A continuación se ha estudiado una implementación del algoritmo de Davis-Putnam en Haskell.

Los códigos y las transparencias usados en la presentación son los siguientes:

Código de SAT en Haskell

-- SAT.hs
-- El problema SAT para fóemulas en FNC.
-- José A. Alonso Jiménez <jalonso@us,es>
-- Sevilla, 4 de febrero de 2020
-- ---------------------------------------------------------------------
 
module SAT where
 
import Data.List
 
-- ---------------------------------------------------------------------
-- § Átomos, literales, cláusulas y FNC
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
-- Ejercicio. Usareremos las siguientes representaciones:
-- + Los átomos se representan por enteros positivos. Por ejemplo, 3
--   representa x(3). 
-- + Los literales se representa por enteros. Por ejemplo, 3 reprsenta
--   el literal positivo x(3) y -5 el literal negativo -x(3).
-- + Una cláusula es una lista de literales que representa su
--   disyunción. 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 su conjunción. Por ejemplo, [[3,2],[-1,2,5]]
--   representa a (x(3) v x(2)) & (-x(1) v x(2) v x(5)).
--
-- Definir los tipo de datos Atomo, Literal, Clausula y FNC.
-- ---------------------------------------------------------------------
 
type Atomo    = Int
type Literal  = Int
type Clausula = [Literal]
type FNC      = [Clausula]
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    complementario :: Literal -> Literal
-- tal que (complementario l) es el complementario de l. Por ejemplo,
--    complementario 3  ==  -3
--    complementario (-3)  ==  3
-- ---------------------------------------------------------------------
 
complementario :: Literal -> Literal
complementario l = (-1) * l
 
-- ---------------------------------------------------------------------
-- § Átomos de cláusulas y de FNC
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    atomosClausula :: Clausula -> [Prop]
-- tal que (atomosClausula c) es el conjunto de los átomos de c. Por
-- ejemplo, 
--    atomosClausula [1,3,-1] == [1,3]
-- ---------------------------------------------------------------------
 
atomosClausula :: Clausula -> [Atomo]
atomosClausula c = nub (map abs c)
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    unionGeneral :: Eq a => [[a]] -> [a]
-- tal que (unionGeneral x) es la unión de los conjuntos de la lista de
-- conjuntos x. Por ejemplo,
--    unionGeneral []                 ==  []
--    unionGeneral [[1]]              ==  [1]
--    unionGeneral [[1],[1,2],[2,3]]  ==  [1,2,3]
-- ---------------------------------------------------------------------
 
unionGeneral :: Eq a => [[a]] -> [a]
unionGeneral []     = []
unionGeneral (x:xs) = x `union` unionGeneral xs 
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    atomosFNC :: FNC -> [Prop]
-- tal que (atomosFNC f) es el conjunto de los átomos de f. Por ejemplo, 
--    atomosFNC [[1,2],[4,-2]] == [1,2,4]
-- ---------------------------------------------------------------------
 
atomosFNC :: FNC -> [Atomo]
atomosFNC f = unionGeneral [atomosClausula c | c <- f]
 
-- ---------------------------------------------------------------------
-- § Interpretaciones 
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
-- Ejercicio. Una interpretación I es un conjunto de átomos. Se supone
-- que los átomos de I son verdaderos y los restantes son falsos.
--
-- Definir el tipo de dato Interpretacion.
-- ---------------------------------------------------------------------
 
type Interpretacion = [Atomo]
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    interpretacionesClausula :: Clausula -> [Interpretacion]
-- tal que (interpretacionesClausula c) es el conjunto de
-- interpretaciones de c. Por ejemplo,
--    interpretacionesClausula [1,2,-1]  ==  [[],[1],[2],[1,2]]
--    interpretacionesClausula []        ==  [[]]
-- ---------------------------------------------------------------------
 
interpretacionesClausula :: Clausula -> [Interpretacion]
interpretacionesClausula c = subsequences (atomosClausula c)
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    interpretaciones :: FNC -> [Interpretacion]
-- tal que (interpretaciones f) es el conjunto de interpretaciones de
-- f. Por ejemplo, 
--    interpretaciones [[1,-2],[-1,2]] == [[],[1],[2],[1,2]]
--    interpretaciones []              == [[]]
-- ---------------------------------------------------------------------
 
interpretaciones :: FNC -> [Interpretacion]
interpretaciones f = subsequences (atomosFNC f)
 
-- ---------------------------------------------------------------------
-- § Modelos de literales, cláusulas y FNC 
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    esModeloLiteral :: Interpretacion -> Literal -> Bool
-- tal que (esModeloLiteral i l) se verifica si i es modelo de l. Por
-- ejemplo, 
--    esModeloLiteral [3,5] 3     ==  True
--    esModeloLiteral [3,5] 4     ==  False
--    esModeloLiteral [3,5] (-3)  ==  False
--    esModeloLiteral [3,5] (-4)  ==  True
-- ---------------------------------------------------------------------
 
esModeloLiteral :: Interpretacion -> Literal -> Bool
esModeloLiteral i l
  | l > 0     = l `elem` i
  | otherwise = complementario l `notElem` i
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    esModeloClausula :: Interpretacion -> Clausula -> Bool
-- tal que (esModeloClausula i c) se verifica si i es modelo de c . Por
-- ejemplo, 
--    esModeloClausula [3,5] [2,3,-5]  ==  True
--    esModeloClausula [3,5] [2,4,-1]  ==  True
--    esModeloClausula [3,5] [2,4,1]  ==  False
-- ---------------------------------------------------------------------
 
esModeloClausula :: Interpretacion -> Clausula -> Bool
esModeloClausula i c = or [esModeloLiteral i l | l <- c]
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    modelosClausula :: Clausula -> [Interpretacion]
-- tal que (modelosClausula c) es la lista de los modelos de c. Por
-- ejemplo, 
--    modelosClausula [-1,2]  ==  [[],[2],[1,2]]
--    modelosClausula [-1,1]  ==  [[],[1]]
--    modelosClausula []      ==  []
-- ---------------------------------------------------------------------
 
modelosClausula :: Clausula -> [Interpretacion]
modelosClausula c =
  [i | i <- interpretacionesClausula c,
       esModeloClausula i c]
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    esModelo :: Interpretacion -> FNC -> Bool
-- tal que (esModelo i f) se verifica si i es modelo de f. Por ejemplo,
--    esModelo [1,3] [[1,-2],[3]]  ==  True
--    esModelo [1]   [[1,-2],[3]]  ==  False
--    esModelo [1]   []            ==  True
-- ---------------------------------------------------------------------
 
esModelo :: Interpretacion -> FNC -> Bool
esModelo i s =
  and [esModeloClausula i c | c <- s]
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    modelos :: FNC -> [Interpretacion]
-- tal que (modelos f) es la lista de los modelos de f. Por ejemplo, 
--    modelos [[-1,2],[-2,1]]    ==  [[],[1,2]]
--    modelos [[-1,2],[-2],[1]]  ==  []
--    modelos [[1,-1,2]]         ==  [[],[1],[2],[1,2]]
-- ---------------------------------------------------------------------
 
modelos :: FNC -> [Interpretacion]
modelos s =
  [i | i <- interpretaciones s,
       esModelo i s] 
 
-- ---------------------------------------------------------------------
-- § Cláusulas válidas, satisfacibles e insatisfacibles                
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    esSatisfacibleClausula :: Clausula -> Bool
-- tal que (esSatisfacibleClausula c) se verifica si la cláusula c es
-- satisfacible. Por ejemplo, 
--    esSatisfacibleClausula [1,2,-1]  ==  True
--    esSatisfacibleClausula [1,2,-3]  ==  True
--    esSatisfacibleClausula []        ==  False
-- ---------------------------------------------------------------------
 
-- 1ª definición
esSatisfacibleClausula1 :: Clausula -> Bool
esSatisfacibleClausula1 c =
  or [esModeloClausula i c | i <- interpretacionesClausula c]
 
-- 2ª definición
esSatisfacibleClausula :: Clausula -> Bool
esSatisfacibleClausula = not . null 
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    esInsatisfacibleClausula :: Clausula -> Bool
-- tal que (esInsatisfacibleClausula c) se verifica si la cláusula c es
-- insatisfacible. Por ejemplo, 
--    esInsatisfacibleClausula [1,2,-1]  ==  False
--    esInsatisfacibleClausula [1,2,-3]  ==  False
--    esInsatisfacibleClausula []        ==  True
-- ---------------------------------------------------------------------
 
-- 1ª definición
esInsatisfacibleClausula1 :: Clausula -> Bool
esInsatisfacibleClausula1 c =
   and [not (esModeloClausula i c) | i <- interpretacionesClausula c]
 
-- 2ª definición
esInsatisfacibleClausula :: Clausula -> Bool
esInsatisfacibleClausula  = null
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    esValidaClausula :: Clausula -> Bool
-- tal que (esValidaClausula c) se verifica si la cláusula c es
-- válida. Por ejemplo, 
--    esValidaClausula [1,2,-1]  ==  True
--    esValidaClausula [1,2,-3]  ==  False
--    esValidaClausula []        ==  False
-- ---------------------------------------------------------------------
 
-- 1ª definición
esValidaClausula1 :: Clausula -> Bool
esValidaClausula1 c =
  and [esModeloClausula i c | i <- interpretacionesClausula c]
 
-- 2ª definición
esValidaClausula :: Clausula -> Bool
esValidaClausula c =
  not (null [l | l <- c, complementario l `elem` c])
 
-- ---------------------------------------------------------------------
-- § FNC válidas, satisfacible e insatisfacibles
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    esSatisfacible :: FNC -> Bool
-- tal que (esSatisfacible f) se verifica si la FNC f es
-- satistacible. Por ejemplo, 
--    esSatisfacible [[-1,2],[-2,1]]  ==  True
--    esSatisfacible [[-1,2],[-2,2]]  ==  True
--    esSatisfacible [[-1,1],[-2,2]]  ==  True
--    esSatisfacible []               ==  True
-- ---------------------------------------------------------------------
 
esSatisfacible :: FNC -> Bool
esSatisfacible s =
  not (null (modelos s))
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    esInsatisfacible :: FNC -> Bool
-- tal que (esInsatisfacible f) se verifica si la FNC f es
-- insatisfacible. Por ejemplo,
--    esInsatisfacible [[-1,2],[-2,1]]  ==  False
--    esInsatisfacible [[-1],[1]]       ==  True
-- ---------------------------------------------------------------------
 
esInsatisfacible :: FNC -> Bool
esInsatisfacible f =
  null (modelos f)
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    esValida :: FNC -> Bool
-- tal que (esValida f) se verifica si f es válida. Por ejemplo, 
--    esValida [[-1,2],[-2,1]]  ==  False
--    esValida [[-1,1],[-2,2]]  ==  True
--    esValida []               ==  True
-- ---------------------------------------------------------------------
 
-- 1ª definición
esValida1 :: FNC -> Bool
esValida1 f =
  modelos f == interpretaciones f
 
-- 2ª definición
esValida :: FNC -> Bool
esValida f =
  and [esValidaClausula c | c <- f]

Presentación del algoritmo de Davis-Putnam

La presentación se ha basado en las 12 primeras páginas del siguiente tema

Descargar (PDF, 283KB)

Código del algoritmo de Davis-Putnam en Haskell

-- DavisPutnam.hs
-- El procedimiento de Davis y Putnam para SAT
-- José A. Alonso Jiménez <jalonso@us,es>
-- Sevilla, 4 de febrero de 2020
-- ---------------------------------------------------------------------
 
module SAT_DavisPutnam where
 
import SAT
import Data.List 
import Test.QuickCheck
 
-- ---------------------------------------------------------------------
-- § Eliminación de tautologías
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    esTautologia :: Clausula -> Bool
-- tal que (esTautologia c) se verifica si c es una tautología. Por
-- ejemplo, 
--    esTautologia [1,2,-1]  ==  True
--    esTautologia [1,2,-3]  ==  False
--    esTautologia []        ==  False
-- ---------------------------------------------------------------------
 
esTautologia :: Clausula -> Bool
esTautologia = esValidaClausula
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    eliminaTautologias :: FNC -> FNC
-- tal que (eliminaTautologias s) es el conjunto obtenido eliminando las
-- tautologías de s. Por ejemplo,
--    eliminaTautologias [[1,2],[1,3,-1]]  ==  [[1,2]]
-- ---------------------------------------------------------------------
 
eliminaTautologias :: FNC -> FNC
eliminaTautologias s =
  [c | c <- s, not (esTautologia c)]
 
-- ---------------------------------------------------------------------
-- § Eliminación de cláusulas unitarias
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    esUnitaria :: Clausula -> Bool
-- tal que (esUnitaria c) se verifica si la cláusula c es unitaria . Por
-- ejemplo, 
--    esUnitaria [3]    ==  True
--    esUnitaria [-3]   ==  True
--    esUnitaria [3,2]  ==  False
--    esUnitaria []     ==  False
-- ---------------------------------------------------------------------
 
esUnitaria :: Clausula -> Bool
esUnitaria [_] = True
esUnitaria _   = False
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    eliminaClausulaUnitaria :: Literal -> FNC -> FNC
-- tal que (eliminaClausulaUnitaria l s) es el conjunto obtenido al
-- reducir s por la eliminación de la cláusula unitaria formada por el
-- literal l. Por ejemplo,
--    λ> eliminaClausulaUnitaria (-1) [[1,2,-3],[1,-2],[-1],[3]]
--    [[2,-3],[-2],[3]]
--    λ> eliminaClausulaUnitaria (-2) [[2,-3],[-2],[3]]
--    [[-3],[3]]
--    λ> eliminaClausulaUnitaria (-3) [[-3],[3],[1]]
--    [[],[1]]
-- ---------------------------------------------------------------------
 
eliminaClausulaUnitaria :: Literal -> FNC -> FNC
eliminaClausulaUnitaria l s =
  [delete (complementario l) c | c <- s, notElem l c]
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    clausulaUnitaria :: FNC -> Maybe Literal
-- tal que (clausulaUnitaria s) es la primera cláusula unitaria de s, si
-- s tiene cláusulas unitarias y nada en caso contrario. Por ejemplo,
--    clausulaUnitaria [[1,2],[1],[-2]]  ==  Just 1
--    clausulaUnitaria [[1,2],[1,-2]]  ==  Nothing
-- ---------------------------------------------------------------------
 
clausulaUnitaria :: FNC -> Maybe Literal
clausulaUnitaria [] = Nothing
clausulaUnitaria (c:cs) 
  | esUnitaria c = Just (head c)
  | otherwise    = clausulaUnitaria cs
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    eliminaClausulasUnitarias :: FNC -> FNC
-- tal que (eliminaClausulasUnitarias s) es el conjunto obtenido
-- aplicando el proceso de eliminación de cláusulas unitarias a s. Por
-- ejemplo, 
--    λ> eliminaClausulasUnitarias [[1,2,-3],[1,-2],[-1],[3],[5]]
--    [[],[5]]
--    λ> eliminaClausulasUnitarias [[1,2],[-2],[-1,2,-3]]
--    []
--    λ> eliminaClausulasUnitarias [[-1,2],[1],[3,5]]
--    [[3,5]]
-- ---------------------------------------------------------------------
 
eliminaClausulasUnitarias :: FNC -> FNC
eliminaClausulasUnitarias s 
  | elem [] s                     = s
  | clausulaUnitaria s == Nothing = s 
  | otherwise                     =
      eliminaClausulasUnitarias (eliminaClausulaUnitaria c s)
  where Just c = clausulaUnitaria s
 
-- ---------------------------------------------------------------------
-- Eliminación de literales puros                                     --
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    literales :: FNC -> [Literal]
-- tal que (literales f) es el conjunto de literales de f. Por ejemplo,
--    literales [[1,2,-3],[1,2,-1]]  ==  [1,2,-3,-1]
-- ---------------------------------------------------------------------
 
literales :: FNC -> [Literal]
literales = unionGeneral
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    esLiteralPuro :: Literal -> FNC -> Bool
-- tal que (esLiteralPuro l f) se verifica si l es puro en f. Por
-- ejemplo, 
--    esLiteralPuro 1 [[1,2],[1,-2],[3,2],[3,-2]]  ==  True
--    esLiteralPuro 2 [[1,2],[1,-2],[3,2],[3,-2]]  ==  False
-- ---------------------------------------------------------------------
 
esLiteralPuro :: Literal -> FNC -> Bool
esLiteralPuro l f =
  and [notElem l' c | c <- f]
  where l' = complementario l
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    eliminaLiteralPuro :: Literal -> FNC -> FNC
-- tal que (eliminaLiteralPuro l f) es el conjunto obtenido eliminando
-- el literal puro l de f. Por ejemplo,
--    eliminaLiteralPuro 1 [[1,2],[1,-2],[3,2],[3,-2]]  ==  [[3,2],[3,-2]]
--    eliminaLiteralPuro 3 [[3,2],[3,-2]]  ==  []
-- ---------------------------------------------------------------------
 
eliminaLiteralPuro :: Literal -> FNC -> FNC
eliminaLiteralPuro l f =
  [c | c <- f, l `notElem` c]
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    literalesPuros :: FNC -> [Literal]
-- tal que (literalesPuros f) es el conjunto de los literales puros de
-- f. Por ejemplo, 
--    literalesPuros [[1,2],[1,-2],[3,2],[3,-2]]  ==  [1,3]
-- ---------------------------------------------------------------------
 
literalesPuros :: FNC -> [Literal]
literalesPuros f =
  [l | l <- literales f, esLiteralPuro l f] 
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    eliminaLiteralesPuros :: FNC -> FNC
-- tal que (eliminaLiteralesPuros f) es el conjunto obtenido aplicando a
-- f el proceso de eliminación de literales puros. Por ejemplo,
--    eliminaLiteralesPuros [[1,2],[1,-2],[3,2],[3,-2]]  ==  []
--    eliminaLiteralesPuros [[1,2],[3,-5],[-3,5]]  ==  [[3,-5],[-3,5]]
-- ---------------------------------------------------------------------
 
eliminaLiteralesPuros :: FNC -> FNC
eliminaLiteralesPuros f 
  | null lp   = f
  | otherwise = 
      eliminaLiteralesPuros (eliminaLiteralPuro (head lp) f)
  where lp = literalesPuros f
 
-- ---------------------------------------------------------------------
-- § Bifurcación
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    bifurcacion :: FNC -> Literal -> (FNC,FNC)
-- tal que (bifurcacion f l) es la bifurcación de f según el literal
-- l. Por ejemplo, 
--    λ> bifurcacion [[1,-2],[-1,2],[2,-3],[-2,-3]] 1
--    ([[-2],[2,-3],[-2,-3]],[[2],[2,-3],[-2,-3]])
-- ---------------------------------------------------------------------
 
bifurcacion :: FNC -> Literal -> (FNC,FNC)
bifurcacion f l =
  ([delete l c  | c <- f, elem l c]  ++ cláusulas_sin_l_ni_l',
   [delete l' c | c <- f, elem l' c] ++ cláusulas_sin_l_ni_l')
  where l'                    = complementario l
        cláusulas_sin_l_ni_l' = [c | c <- f, notElem l c, notElem l' c]
 
-- ---------------------------------------------------------------------
-- § Algoritmo de Davis y Putnam (DP)
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    tieneClausulasUnitarias :: FNC -> Bool
-- tal que (tieneClausulasUnitarias f) se verifica si f tiene cláusulas
-- unitarias. Por ejemplo, 
--    tieneClausulasUnitarias [[1,2],[1],[-2]]  ==  True
--    tieneClausulasUnitarias [[1,2],[1,-2]]  ==  False
-- ---------------------------------------------------------------------
 
tieneClausulasUnitarias :: FNC -> Bool
tieneClausulasUnitarias f =
  clausulaUnitaria f /= Nothing
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    tieneLiteralesPuros :: FNC -> Bool
-- tal que (tieneLiteralesPuros f) se verifica si f tiene literales
-- puros. Por ejemplo, 
--    tieneLiteralesPuros [[1,2],[1,-2],[3,2],[3,-2]]    ==  True
--    tieneLiteralesPuros [[1,2],[-1,-2],[-3,2],[3,-2]]  ==  False
-- ---------------------------------------------------------------------
 
tieneLiteralesPuros :: FNC -> Bool
tieneLiteralesPuros f =
  not (null (literalesPuros f))
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    esInsatisfaciblePorDP :: FNC -> Bool
-- tal que (esInsatisfaciblePorDP f) se verifica si f es insatisfacible
-- mediante el algoritmo de Davis y Putnam. Por ejemplo, 
--    esInsatisfaciblePorDP [[1,2],[1,2,-1]]                ==  False
--    esInsatisfaciblePorDP [[1,2,-3],[1,-2],[-1],[3],[5]]  ==  True
--    esInsatisfaciblePorDP [[1,2],[-2],[-1,2,-3]]          ==  False
--    esInsatisfaciblePorDP [[-1,2],[1],[3,5]]              ==  False
--    esInsatisfaciblePorDP [[1,2],[1,-2],[3,2],[3,-2]]     ==  False
--    esInsatisfaciblePorDP [[1,2],[3,-4],[-3,4]]           ==  False
-- ---------------------------------------------------------------------
 
esInsatisfaciblePorDP :: FNC -> Bool
esInsatisfaciblePorDP f =
  esInsatisfaciblePorDP' (eliminaTautologias f)
 
esInsatisfaciblePorDP' :: FNC -> Bool
esInsatisfaciblePorDP' f
  | null f = False
  | elem [] f = True
  | tieneClausulasUnitarias f = 
      esInsatisfaciblePorDP' (eliminaClausulasUnitarias f)
  | tieneLiteralesPuros f =
      esInsatisfaciblePorDP' (eliminaLiteralesPuros f)
  | otherwise = 
      (esInsatisfaciblePorDP' s1) && (esInsatisfaciblePorDP' s2)
  where l       = head (head f)
        (s1,s2) = bifurcacion f l
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    esSatisfaciblePorDP :: FNC -> Bool
-- tal que (esSatisfaciblePorDP f) se verifica si f es satisfacible
-- mediante el algoritmo de Davis y Putnam. Por ejemplo, 
--    esSatisfaciblePorDP [[1,2],[1,2,-1]]                ==  True
--    esSatisfaciblePorDP [[1,2,-3],[1,-2],[-1],[3],[5]]  ==  False
-- ---------------------------------------------------------------------
 
esSatisfaciblePorDP :: FNC -> Bool
esSatisfaciblePorDP = not . esInsatisfaciblePorDP 
 
-- ---------------------------------------------------------------------
-- § Corrección del algoritmo de Davis y Putnam                       --
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
-- Ejercicio. Comprobar con QuickCheck que el algoritmo De Davis y
-- Putnam es correcto; es decir, para toda fórmula f, f es
-- insatisfacible según el algoritmo de Davis y Putnam si,y solo si, f
-- es insatisfacible.
-- ---------------------------------------------------------------------
 
prop_CorreccionDP :: FNC -> Bool
prop_CorreccionDP f =
  esInsatisfaciblePorDP f == esInsatisfacible f
 
-- La comprobación es
--    λ> quickCheckWith (stdArgs {maxSize=10}) prop_CorreccionDP
--    +++ OK, passed 100 tests.

RA2019: Deducción natural de primer orden con Isabelle/HOL

En la clase de hoy del curso de Razonamiento automático se ha presentado la deducción natural de primer orden Isabelle/HOL. La presentación se basa en los ejemplos del tema 8 del curso de Lógica informática que, a su vez, se basa en el capítulo 2 del libro de Huth y Ryan Logic in Computer Science (Modelling and reasoning about systems).

La página al lado de cada ejemplo indica la página de las transparencias donde se encuentra la demostración.

Para cada ejemplo se presentan distintas demostraciones. La primera intenta reflejar la demostración de las transparencias, las siguientes van eliminando detalles de la prueba hasta la última que es automática.

A los largos de los ejemplos se van comentando los elementos del lenguaje conforme van entrando en el juego.

La teoría con los ejemplos presentados en la clase es la siguiente:

RA2019: Sintaxis y semántica de la lógica de primer orden

En la segunda parte de la clase de hoy del curso Razonamiento automático se ha presentado la sintaxis y la semántica de la lógica de primer orden como respuestas a las siguientes preguntas:

  • ¿cómo se puede representar el conocimiento con la lógica de primer orden?,
  • ¿qué es una fórmula de primer orden?,
  • ¿qué significa que una fórmula verdadera? y
  • ¿qué significa que un argumento sea correcto?

Como ejemplos de representación hemos visto cómo representar conocimiento geográfico, del mundo de los bloques y conocimiento astronómico. En los distintos ejemplos hemos resaltado los tipos de símbolos lógicos utilizados.

A partir de los ejemplos de representación del conocimiento, se han definido los símbolos lógicos (variables, conectivas, cuantificadores e igualdad) y los símbolos no lógicos (constantes, predicados y funciones) que forman el alfabeto del lenguaje de la lógica de primer orden.

A partir del alfabeto, se definen los términos, las fórmulas atómicas y las fórmulas del lenguaje.

Como medio del reconocimiento de fórmulas, se introducen los árboles de análisis. Con ello, respondemos a la segunda de las preguntas iniciales.

En segundo lugar hemos estudiado la semántica, comenzando con distintas cuestiones sobre qué significa que una fórmula sea verdadera para resaltar su dependencia del universo, la interpretación de los símbolos no lógico y de las asignaciones a las variables libres.

Se han definido las estructuras de un lenguaje, las asignaciones a las variables y las interpretaciones de un lenguaje.

Se ha definido el valor de un término o de una fórmula en una interpretación. Con ello, respondemos a la tercera de las preguntas iniciales.

Las transparencias de esta clase son las del tema 8a.

Como práctica, se ha propuesto la 8ª relación de ejercicios.

RA2019: Deducción natural proposicional con Isabelle/HOL (2)

En la clase de hoy del curso de Razonamiento automático se ha completado la presentación de la deducción natural con Isabelle/HOL.

La presentación se basa en los ejemplos del tema 2 del curso de Lógica informática que, a su vez, se basa en el capítulo 2 del libro de Huth y Ryan Logic in Computer Science (Modelling and reasoning about systems).

La página al lado de cada ejemplo indica la página de las transparencias donde se encuentra la demostración.

Para cada ejemplo se presentan distintas demostraciones. La primera intenta reflejar la demostración de las transparencias, las siguientes van eliminando detalles de la prueba hasta la penúltima que es automática y la última es aplicativa.

A los largos de los ejemplos se van comentando los elementos del lenguaje conforme van entrando en el juego.

La teoría con los ejemplos presentados en la clase es la siguiente:

RA2019: Deducción natural proposicional con Isabelle/HOL (1)

En la clase de hoy del curso de Razonamiento automático se ha comenzado la presentación de la deducción natural con Isabelle/HOL.

La presentación se basa en los ejemplos del tema 2 del curso de Lógica informática que, a su vez, se basa en el capítulo 2 del libro de Huth y Ryan Logic in Computer Science (Modelling and reasoning about systems).

La página al lado de cada ejemplo indica la página de las transparencias donde se encuentra la demostración.

Para cada ejemplo se presentan distintas demostraciones. La primera intenta reflejar la demostración de las transparencias, las siguientes van eliminando detalles de la prueba hasta la penúltima que es automática y la última es aplicativa.

A los largos de los ejemplos se van comentando los elementos del lenguaje conforme van entrando en el juego.

La teoría con los ejemplos presentados en la clase es la siguiente:

RA2019: Ejercicios de cuantificadores sobre listas en Isabelle/HOL

En la segunda parte de la clase de hoy del curso de Razonamiento automático se han comentado las soluciones de la 4ª relación de ejercicios de cuantificadores sobre listas. Para cada propiedad se dan tres demostraciones en Isabelle/HOL: la primera automática, la segunda estructurada y la tercera totalmente detallada mostrando todos los lemas de HOL que se utilizan en cada paso.

La teoría con las soluciones de los ejercicios es la siguiente