# Lógica proposicional

El módulo `sympy` permite hacer algunos cálculos en lógica proposicional


```python
from sympy import *
```

Vamos a decirle a sympy que renderice las salidas en LaTeX con mathjax


```python
init_printing()
```

## Satisfacibilidad

**Ejemplo** Si es cierto $a\to b$, ¿podemos inferir algo sobre $a\vee c\to b\vee c$? ¿Y sobre $a\wedge c\to b\wedge c$?


```python
a,b,c = symbols("a,b,c")
```

Vamos a usar que $\Gamma \models \alpha$ equivale a que $\Gamma\cup\{\neg \alpha\}$ es insatisfacible


```python
p = a >> b
q = (a|c)>>(b|c)
```


```python
p&~q
```


```python
satisfiable(p&~q)
```




    False



También podíamos ver si $p\to q$ es una tautología por el teorema de la deducción, o lo que es lo mismo, mostrar que siempre es verdadera


```python
simplify(p>>q)
```

Lo mismo con $a\wedge c\to b\wedge c$


```python
simplify(p>>((a&c)>>(b&c)))
```

**Ejemplo** Estudia si el conjunto $\{c\to (a\vee c), b\to(c\to a), d\wedge \neg (c\to a)\}$ es satisfacible


```python
a,b,c,d = symbols("a,b,c,d")
```


```python
satisfiable((c>>(a|b))&(b>>(c>>a))&d&~(c>>a))
```




    False



De ser satisfacible, nos daría un mundo donde lo es


```python
satisfiable(a|b)
```




    {b: True, a: True}



O bien todos los mundos donde lo es, si así se lo pedimos


```python
list(satisfiable(a|b, all_models=True))
```




    [{b: True, a: True}, {b: False, a: True}, {b: True, a: False}]



## Implicación semántica

Podemos detectar si $\Gamma\models a$ con la siguiente función


```python
def implica(gamma,a):
    """ Determina si Gamma implica semanticamente a"""
    p = True
    for x in gamma:
        p = p & x
    p=p&(~a)
    return not(satisfiable(p))
```


```python
implica([a,a>>b],b)
```




    True




```python
implica([a>>b,b>>c],a>>c)
```




    True



Volvamos al primer ejemplo


```python
implica([a>>b], (a|c)>>(b|c))
```




    True



Otro ejemplo


```python
implica([a>>b],a)
```




    False



## Tautologías

Una proposición $a$ es tautología si $\models a$


```python
implica([], a>>(b>>a))
```




    True




```python
implica([],~a>>(a>>b))
```




    True




```python
def tautologia(a):
    return not(satisfiable(~a))
```


```python
tautologia(~a>>(a>>b))
```




    True




```python
tautologia(a>>b)
```




    False




```python
(a>>b).args
```


```python
to_cnf(a>>(b&c))
```


```python
type(_)
```




    And




```python
to_cnf(a>>b)
```


```python
type(_)
```




    Or



## Davis-Putnam
### Forma clausular y operaciones con literales

Vamos a definir la forma clausular de un conjunto de proposiciones


```python
G= {c>>(a|b), b>>(c>>a), d&~(c>>a)}
```


```python
def forma_clausular(G):
    fc = set([])
    for g in G:
        q = to_cnf(g)
        if isinstance(q,And):
            fc.update(q.args)
        else:
            fc.add(q)
    return fc
```


```python
forma_clausular(G)
```


```python
def es_literal(p):
    if isinstance(p,Symbol):
        return True
    if isinstance(p,Not):
        ar = p.args
        if len(ar)==1 and isinstance(ar[0],Symbol):
            return True
    return False
```


```python
es_literal(a)
```




    True




```python
es_literal(~a)
```




    True




```python
es_literal(a&b)
```




    False




```python
v=Or(*[])
```


```python
type(v)
```




    sympy.logic.boolalg.BooleanFalse




```python
v==False
```




    True




```python
def es_clausula(p):
    if p==False:
        return True
    if es_literal(p):
        return True
    if isinstance(p,Or):
        ar = p.args
        return all(es_literal(a) for a in ar)
    return False
```


```python
es_clausula(a&b)
```




    False




```python
es_clausula(a|~b)
```




    True




```python
def complemento(p):
    if isinstance(p,Symbol):
        return ~p
    if isinstance(p,Not):
        return p.args[0]
    return None
```


```python
complemento(a)
```


```python
complemento(~a)
```


```python
l=[1,2,3]
l.remove(3)
2 in l
```




    True




```python
def quita(c,l):
    if c==False:
        return False
    if es_literal(c):
        if c==l:
            return False
        return c
    ar = list(c.args)
    if l in ar:
        ar.remove(l)
        return Or(*ar)
    return c
```


```python
quita(a|b,b)
```


```python
quita(a|b,~b)
```


```python
def primero(xs,cond):
    for x in xs:
        if cond(x):
            return x
    return None
```


```python
primero([1,2,3],lambda x:(x%2)==0)
```


```python
def clausula_a_lista(c):
    if c==False:
        return []
    if es_literal(c):
        return [c]
    return list(c.args)
```


```python
clausula_a_lista(a|b|~c)
```

### Detectando una clausula unit


```python
def clausula_unit(cs):
    l = primero(cs,es_literal)
    if l!=None:
        print("Hemos encontrado una clausula unit ", l)
        csp = [c for c in cs if not(l in clausula_a_lista(c))]
        cspq = [quita(c,complemento(l)) for c in csp]
        pprint(cspq)
        return cspq
    return cs
```


```python
clausula_unit([a,a|b, ~a|c, c|b])
```


```python
Or(a,~a,b)
```


```python
simplify(_)
```

### Quitando tautologías y cláusulas redundantes


```python
def quita_tautologias(cs):
    return [c for c in cs if simplify(c)!=True]
```


```python
quita_tautologias([a|b|~a,a|c])
```


```python
l=[1,2]
```

La siguiente función determina si todos los literales de una cláusula están contenidos en otra cláusula


```python
def contenido(c1,c2):
    return all((l in clausula_a_lista(c2)) for l in clausula_a_lista(c1))
```


```python
contenido(a|b,a|b|c)
```




    True




```python
contenido(a|b,a|c)
```




    False




```python
def quita_redundantes(cs):
    return [c for c in cs if not(any(contenido(d,c) and d!=c for d in cs))]
```


```python
quita_redundantes([a|b,a|b|c])
```

### Encontrando litereales puros


```python
def literal_puro(cs):
    literales = set([])
    for c in cs:
        literales.update(clausula_a_lista(c))
    l = primero(literales, lambda x:not(complemento(x) in literales))
    if l==None:
        return cs
    print("Hemos encontrado un literal puro", l)
    csp = [c for c in cs if not(l in clausula_a_lista(c))]
    print(csp)
    return csp
```


```python
literal_puro([a|b,~a])
```

### Dividiendo cuando no hay literales puros ni cláuslas unit


```python
def divide(cs):
    literales = set([])
    for c in cs:
        literales.update(clausula_a_lista(c))
    l = primero(literales, lambda x:(complemento(x) in literales))
    cl = complemento(l)
    csl = set([quita(c,l) for c in cs if l in clausula_a_lista(c)])
    csnl= set([quita(c,cl) for c in cs if cl in clausula_a_lista(c)])
    csc = set([c for c in cs if not(l in clausula_a_lista(c)) and not(cl in clausula_a_lista(c))])
    parte1=csl.union(csc)
    parte2=csnl.union(csc)
    print("Dividimos usando ",l)
    pprint(parte1)
    pprint(parte2)
    return [csl.union(csc),csnl.union(csc)]
```


```python
divide([a|b,~a|b,a|c, b|c])
```

### Algoritmo de Davis-Putnam


```python
def inconsistente(cs):
    """Detecta si cs es satisfacible usando Davis-Putnam"""
    css = quita_tautologias(quita_redundantes(cs))
    unitpuro=True
    while unitpuro:
        cssn = clausula_unit(css)
        if cssn== css:
            cssn = literal_puro(css)
            if cssn==css:
                unitpuro=False
        if len(cssn)==0:
            print("Hemos llegado al conjunto vacío")
            return False
        if False in cssn:
            print("Hemos encontrado la cláusula vacía")
            return True
        css=cssn

    d = divide(css)
    return inconsistente(d[0]) and inconsistente(d[1])
    
```


```python
inconsistente([~a,a])
```

    Hemos encontrado una clausula unit  Not(a)
    [False]
    Hemos encontrado la cláusula vacía





    True




```python
clausula_unit([a,b])
```


```python
clausula_unit([b])
```


```python
inconsistente([a,b])
```

    Hemos encontrado una clausula unit  a
    [b]
    Hemos encontrado una clausula unit  b
    []
    Hemos llegado al conjunto vacío





    False




```python
inconsistente([~a|b,a,~b])
```

    Hemos encontrado una clausula unit  a
    [b, ¬b]
    Hemos encontrado una clausula unit  b
    [False]
    Hemos encontrado la cláusula vacía





    True



Este último ejemplo es precisamente el modus ponens


```python
inconsistente(forma_clausular([a>>b,a,~b]))
```

    Hemos encontrado una clausula unit  a
    [b, ¬b]
    Hemos encontrado una clausula unit  b
    [False]
    Hemos encontrado la cláusula vacía





    True



**Ejemplo** Veamos que $(a\to (b\to c))\to(\neg (a\to \neg b)\to c)$ es una tautología. Esto equivale a probar 
$$\models (a\to (b\to c))\to(\neg (a\to \neg b)\to c).$$
Por el Teorema de la deducción (dos veces), basta probar que 
$$\{a\to (b\to c), \neg (a\to \neg b)\}\models c,$$
y esto es equivalente a demostrar que el conjunto 
$$\{a\to (b\to c), \neg (a\to \neg b),\neg c\}$$
es insatisfacible



```python
forma_clausular([a>>(b>>c), ~(a>>~b), ~c])
```


```python
inconsistente(_)
```

    Hemos encontrado una clausula unit  Not(c)
    [¬a ∨ ¬b, b, a]
    Hemos encontrado una clausula unit  b
    [¬a, a]
    Hemos encontrado una clausula unit  Not(a)
    [False]
    Hemos encontrado la cláusula vacía





    True



**Ejemplo** Veamos que $$\{(a\to \neg b\vee d)\wedge(b\wedge \neg d\to a\vee c), (d\to (a \leftrightarrow \neg b)\vee (b\wedge \neg c)\}\models (\neg b\to (d\wedge (c\vee \neg d)))\to c\wedge d$$


```python
Gamma={(a>>(~b|d))&((b&~d)>>(a|c)), (d>>(Equivalent(a,~b))|(b|~c)),
       (~b>>(d&(c|~d))),~(c&d)} 
```


```python
forma_clausular(Gamma)
```


```python
inconsistente(forma_clausular(Gamma))
```

    Dividimos usando  Not(c)
    set([¬d, b ∨ d, d ∨ ¬a ∨ ¬b])
    set([b ∨ d, b ∨ ¬d, a ∨ d ∨ ¬b, d ∨ ¬a ∨ ¬b])
    Hemos encontrado una clausula unit  Not(d)
    [b, ¬a ∨ ¬b]
    Hemos encontrado una clausula unit  b
    [¬a]
    Hemos encontrado una clausula unit  Not(a)
    []
    Hemos llegado al conjunto vacío





    False



## Resolventes


```python
Or(Or(a,b),Or(a,c))
```


```python
def resolventes(a,b):
    literales=[l for l in clausula_a_lista(a) if complemento(l) in clausula_a_lista(b)]
    return [Or(quita(a,l),quita(b,complemento(l))) for l in literales]
```


```python
resolventes(~a|b,a|~b)
```
