Lazy developer's approach to do exercises on Propositional Logic

logic.py

# -*- coding: utf-8 -*-

from tabulate import tabulate

class Var(object):
    def __init__(self, name):
        self.name = name
        self.value = None

    def bind(self, value):
        self.value = value

    def __str__(self):
        if self.value is None:
            return self.name
        return "%s'%s" % (self.name, "1" if self.value else "0")

class Operation(object):

    def __init__(self, left, right):
        self.left = left
        self.right = right

    def reduction(self):
        l = self.left.value if isinstance(self.left, Var) else self.left.reduction()
        r = self.right.value if isinstance(self.right, Var) else self.right.reduction()
        return self.table[l][r]

    def __str__(self):
        return "(%s %s %s)" % (self.left, self.name, self.right)

class Neg(object):
    table = {0: 1, 1: 0}

    def __init__(self, var):
        self.var = var

    def reduction(self):
        v = self.var.value if isinstance(self.var, Var) else self.var.reduction()
        return self.table[v]

    def __str__(self):
        return "-%s" % (self.var,)

class Conj(Operation):
    name = "^"
    table = {0: {0: 0, 1: 0}, 1: {0: 0, 1: 1}}

class Disj(Operation):
    name = "v"
    table = {0: {0: 0, 1: 1}, 1: {0: 1, 1: 1}}

class Implication(Operation):
    name = "=>"
    table = {0: {0: 1, 1: 1}, 1: {0: 0, 1: 1}}
    
class Bicond(Operation):
    name = "<=>"
    table = {0: {0: 1, 1: 0}, 1: {0: 0, 1: 1}}

def find_vars(eq):
    if isinstance(eq, Var):
        return [eq]

    if isinstance(eq, Neg):
        return find_vars(eq.var)

    return find_vars(eq.left) + find_vars(eq.right)

def rows(size):
    if size == 1:
        yield [1]
        yield [0]
    else:
        for p in rows(size - 1):
            yield p + [1]
            yield p + [0]

def table(eq):
    # find all variables
    vars = find_vars(eq)

    # build headers using unbind variables
    headers = map(str, vars) + [str(eq)]

    # generate all variants
    table = []
    for vals in rows(len(vars)):
        for val, var in zip(vals, vars):
            var.bind(val)

        table.append(vals + [eq.reduction()])

    return tabulate(table, headers=headers)

####

print "#1"
q = Var("q")
p = Var("p")
print table(Conj(q, p))

##1
#  q    p    (q ^ p)
#---  ---  ---------
#  1    1          1
#  1    0          0
#  0    1          0
#  0    0          0

####

print "#2"
p = Var("p")
q = Var("q")
r = Var("r")
print table(Conj(Disj(q, p), Disj(Neg(q), r)))

##2
#  q    p    q    r    ((q v p) ^ (-q v r))
#---  ---  ---  ---  ----------------------
#  1    1    1    1                       1
#  1    1    1    0                       0
#  1    1    0    1                       1
#  1    1    0    0                       1
#  1    0    1    1                       1
#  1    0    1    0                       0
#  1    0    0    1                       0
#  1    0    0    0                       0
#  0    1    1    1                       1
#  0    1    1    0                       0
#  0    1    0    1                       1
#  0    1    0    0                       1
#  0    0    1    1                       1
#  0    0    1    0                       0
#  0    0    0    1                       0
#  0    0    0    0                       0

### 

# a sentence φ is logically equivalent to a sentence ψ
# if and only if every truth assignment that satisfies φ
# satisfies ψ and every truth assignment
# that satisfies ψ satisfies φ
def is_equivalent(eq1, eq2):
    # assuming they are using the same set of vars
    vars = find_vars(eq1)
    repr1 = str(eq1)
    repr2 = str(eq2)

    print "Sentence 1:", repr1
    print "Sentence 2:", repr2
    print "Table size:", 2**len(vars)

    for vals in rows(len(vars)):
        for val, var in zip(vals, vars):
            var.bind(val)

        r1 = eq1.reduction()
        r2 = eq2.reduction()
        if r1 != r2:
            print "Not equivalent"
            print "Using:", ", ".join(map(lambda (val, var): "%s = %s" % (var.name, val), zip(vals, vars)))
            return False

    print "Equivalent"
    return True

print "#3"
p = Var("p")
q = Var("q")
is_equivalent(Neg(Disj(p, q)), Conj(Neg(p), Neg(q)))
# Sentence 1: -(p v q)
# Sentence 2: (-p ^ -q)
# Table size: 4
# Equivalent

print "#4"
p = Var("p")
q = Var("q")
is_equivalent(Neg(Disj(p, q)), Neg(Conj(Neg(p), Neg(q))))
# Sentence 1: -(p v q)
# Sentence 2: -(-p ^ -q)
# Table size: 4
# Not equivalent
# Using: p = 1, q = 1

# a sentence φ logically entails a sentence ψ (written φ ⊨ ψ)
# if and only if every truth assignment that satisfies φ also satisfies ψ
def does_entail(eq1, eq2):
    # assuming they are using the same set of vars
    vars = find_vars(eq1)
    repr1 = str(eq1)
    repr2 = str(eq2)

    print "Sentence 1:", repr1
    print "Sentence 2:", repr2
    print "Table size:", 2**len(vars)

    for vals in rows(len(vars)):
        for val, var in zip(vals, vars):
            var.bind(val)
        if eq1.reduction() and (not eq2.reduction()):
            print "Logical entailment does not hold"
            print "Using:", ", ".join(map(lambda (val, var): "%s = %s" % (var.name, val), zip(vals, vars)))
            return False

    print "Entails"
    return True

print "#5"
p = Var("p")
q = Var("q")
does_entail(Disj(p, q), Conj(p, q))

# #5
# Sentence 1: (p v q)
# Sentence 2: (p ^ q)
# Table size: 4
# Logical entailment does not hold
# Using: p = 1, q = 0

# a sentence φ is consistent with a sentence ψ
# if and only if there is a truth assignment
# that satisfies both φ and ψ
def is_consistent(eq1, eq2):
    # assuming they are using the same set of vars
    vars = find_vars(eq1)
    repr1 = str(eq1)
    repr2 = str(eq2)

    print "Sentence 1:", repr1
    print "Sentence 2:", repr2
    print "Table size:", 2**len(vars)

    for vals in rows(len(vars)):
        for val, var in zip(vals, vars):
            var.bind(val)

        if eq1.reduction() and eq2.reduction():
            print "Consistent"
            return True

    print "Not consistent"
    return False

print "#6"
p = Var("p")
q = Var("q")
is_consistent(Disj(p, q), Disj(Neg(p), Neg(q)))

# #6
# Sentence 1: (p v q)
# Sentence 2: (-p v -q)
# Table size: 4
# Consistent

print "#7"
p = Var("p")
q = Var("q")
is_consistent(Disj(p, q), Conj(Neg(p), Neg(q)))

# #7
# Sentence 1: (p v q)
# Sentence 2: (-p ^ -q)
# Table size: 4
# Not consistent