Skip to content

Instantly share code, notes, and snippets.

@kachayev

kachayev/logic.py

Last active Jul 11, 2017
Embed
What would you like to do?
Lazy developer's approach to do exercises on Propositional Logic
# -*- 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.