from sympy import *

"""
Explanation: Lógica proposicional
El módulo sympy permite hacer algunos cálculos en lógica proposicional
End of explanation
"""


init_printing()

"""
Explanation: Vamos a decirle a sympy que renderice las salidas en LaTeX con mathjax
End of explanation
"""


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

"""
Explanation: 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$?
End of explanation
"""


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

p&~q

satisfiable(p&~q)

"""
Explanation: Vamos a usar que $\Gamma \models \alpha$ equivale a que $\Gamma\cup{\neg \alpha}$ es insatisfacible
End of explanation
"""


simplify(p>>q)

"""
Explanation: 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
End of explanation
"""


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

"""
Explanation: Lo mismo con $a\wedge c\to b\wedge c$
End of explanation
"""


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

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

"""
Explanation: Ejemplo Estudia si el conjunto ${c\to (a\vee c), b\to(c\to a), d\wedge \neg (c\to a)}$ es satisfacible
End of explanation
"""


satisfiable(a|b)

"""
Explanation: De ser satisfacible, nos daría un mundo donde lo es
End of explanation
"""


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

"""
Explanation: O bien todos los mundos donde lo es, si así se lo pedimos
End of explanation
"""


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))

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

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

"""
Explanation: Implicación semántica
Podemos detectar si $\Gamma\models a$ con la siguiente función
End of explanation
"""


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

"""
Explanation: Volvamos al primer ejemplo
End of explanation
"""


implica([a>>b],a)

"""
Explanation: Otro ejemplo
End of explanation
"""


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

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

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

tautologia(~a>>(a>>b))

tautologia(a>>b)

(a>>b).args

to_cnf(a>>(b&c))

type(_)

to_cnf(a>>b)

type(_)

"""
Explanation: Tautologías
Una proposición $a$ es tautología si $\models a$
End of explanation
"""


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

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

forma_clausular(G)

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

es_literal(a)

es_literal(~a)

es_literal(a&b)

v=Or(*[])

type(v)

v==False

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

es_clausula(a&b)

es_clausula(a|~b)

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

complemento(a)

complemento(~a)

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

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

quita(a|b,b)

quita(a|b,~b)

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

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

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

clausula_a_lista(a|b|~c)

"""
Explanation: Davis-Putnam
Forma clausular y operaciones con literales
Vamos a definir la forma clausular de un conjunto de proposiciones
End of explanation
"""


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

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

Or(a,~a,b)

simplify(_)

"""
Explanation: Detectando una clausula unit
End of explanation
"""


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

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

l=[1,2]

"""
Explanation: Quitando tautologías y cláusulas redundantes
End of explanation
"""


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

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

contenido(a|b,a|c)

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

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

"""
Explanation: La siguiente función determina si todos los literales de una cláusula están contenidos en otra cláusula
End of explanation
"""


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

literal_puro([a|b,~a])

"""
Explanation: Encontrando litereales puros
End of explanation
"""


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)]

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

"""
Explanation: Dividiendo cuando no hay literales puros ni cláuslas unit
End of explanation
"""


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])
    

inconsistente([~a,a])

clausula_unit([a,b])

clausula_unit([b])

inconsistente([a,b])

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

"""
Explanation: Algoritmo de Davis-Putnam
End of explanation
"""


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

"""
Explanation: Este último ejemplo es precisamente el modus ponens
End of explanation
"""


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

inconsistente(_)

"""
Explanation: 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
End of explanation
"""


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

forma_clausular(Gamma)

inconsistente(forma_clausular(Gamma))

"""
Explanation: 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$$
End of explanation
"""


Or(Or(a,b),Or(a,c))

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]

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

"""
Explanation: Resolventes
End of explanation
"""


