# ai.py - agente inteligente baseado em logica proposicional
#         ILP-503 (Prof. Dr. Silvio do Lago Pereira)
         
BC = [['~j', 'g'],  # nao j ou g
      ['j',  't'],  # j ou t
      ['~g', 'c'],  # nao g ou c
      ['~c']]       # nao c

def neg(p):
    if p[0] == '~': return p[1:] 
    else:           return '~' + p

def ref(h):
    print(h)                          # mostra hipotese  atual
    if h == []: return True           # encontrou  contradicao
    p = neg(h[0])                     # literal para  eliminar
    for f in BC:                      # procura formula normal
        if p in f:                    # contendo esse  literal
            r = [q for q in f if q != p]  # elimina o  literal
            if ref(r + h[1:]):            # refuta  resolvente
               return True                # achou  contradicao
    return False                          # nao ha contradicao

def prove(t):
    print('verdade' if ref([neg(t)]) else 'falso')