Skip to content

Instantly share code, notes, and snippets.

@marquicus
Forked from gvx/formula.py
Created March 15, 2021 15:23
Show Gist options
  • Save marquicus/c02316d2b17176fe715e54c659a351c3 to your computer and use it in GitHub Desktop.
Save marquicus/c02316d2b17176fe715e54c659a351c3 to your computer and use it in GitHub Desktop.
Propositional logic library for Python 3, that can valuate an expression and check whether it is a tautology
"""
formula.py - propositional formulas for Python
by Robin Wellner
Hereby, I waive all rights to this library, as described at <http://creativecommons.org/publicdomain/zero/1.0/>
Examples:
foo = Atom('foo')
bar = Atom('bar')
disjuction = foo | bar
conjunction = foo & bar
implication = foo >> bar
if_and_only_if = foo << bar
inverse = ~foo
simple_tautology = foo | ~foo
simple_negative_tautology = foo & ~foo
#Valuation:
#Formula.v(true_set)
print(simple_tautology.v({foo}) # prints True
print(negative_tautology.v({foo}) # prints True
print(inverse.v({bar}) # prints True
#Tautology checking:
#Formula.t()
#returns a set of atoms which cause Formula.v to return False (a counterexample)
#or None if the formula is a tautology
print(simple_tautology.t()) # prints None
print(implication.t()) # prints {foo}
"""
class Formula:
def __invert__(self):
return Not(self)
def __and__(self, other):
return And(self, other)
def __or__(self, other):
return Or(self, other)
def __rshift__(self, other):
return Implies(self, other)
def __lshift__(self, other):
return Iff(self, other)
def __eq__(self, other):
return self.__class__ == other.__class__ and self.eq(other)
def v(self, v):
raise NotImplementedError("Plain formula can not be valuated")
def _t(self, left, right):
while True:
found = True
for item in left:
if item in right:
return None
if not isinstance(item, Atom):
left.remove(item)
tup = item._tleft(left, right)
left, right = tup[0]
if len(tup) > 1:
v = self._t(*tup[1])
if v is not None:
return v
found = False
break
for item in right:
if item in left:
return None
if not isinstance(item, Atom):
right.remove(item)
tup = item._tright(left, right)
left, right = tup[0]
if len(tup) > 1:
v = self._t(*tup[1])
if v is not None:
return v
found = False
break
if found:
return set(left)
def t(self):
return self._t([], [self])
class BinOp(Formula):
def __init__(self, lchild, rchild):
self.lchild = lchild
self.rchild = rchild
def __str__(self):
return '(' + str(self.lchild) + ' ' + self.op+ ' ' + str(self.rchild) + ')'
def eq(self, other):
return self.lchild == other.lchild and self.rchild == other.rchild
class And(BinOp):
op = '∧'
def v(self, v):
return self.lchild.v(v) and self.rchild.v(v)
def _tleft(self, left, right):
return (left + [self.lchild, self.rchild], right),
def _tright(self, left, right):
return (left, right + [self.lchild]), (left, right + [self.rchild])
class Or(BinOp):
op = '∨'
def v(self, v):
return self.lchild.v(v) or self.rchild.v(v)
def _tleft(self, left, right):
return (left + [self.lchild], right), (left + [self.rchild], right)
def _tright(self, left, right):
return (left, right + [self.lchild, self.rchild]),
class Implies(BinOp):
op = '→'
def v(self, v):
return not self.lchild.v(v) or self.rchild.v(v)
def _tleft(self, left, right):
return (left + [self.rchild], right), (left, right + [self.lchild])
def _tright(self, left, right):
return (left + [self.lchild], right + [self.rchild]),
class Iff(BinOp):
op = '↔'
def v(self, v):
return self.lchild.v(v) is self.rchild.v(v)
def _tleft(self, left, right):
return (left + [self.lchild, self.rchild], right), (left, right + [self.lchild, self.rchild])
def _tright(self, left, right):
return (left + [self.lchild], right + [self.rchild]), (left + [self.rchild], right + [self.lchild])
class Not(Formula):
def __init__(self, child):
self.child = child
def v(self, v):
return not self.child.v(v)
def __str__(self):
return '¬' + str(self.child)
def eq(self, other):
return self.child == other.child
def _tleft(self, left, right):
return (left, right + [self.child]),
def _tright(self, left, right):
return (left + [self.child], right),
class Atom(Formula):
def __init__(self, name):
self.name = name
def __hash__(self):
return hash(self.name)
def v(self, v):
return self in v
def __str__(self):
return str(self.name)
__repr__ = __str__
def eq(self, other):
return self.name == other.name
from formula import Atom
a = Atom('a')
b = Atom('b')
c = Atom('c')
def dop(f, e):
print("Formula: ", f)
print("Valuation for", e, ": ", f.v(e))
print("Counterexample: ", f.t())
dop(a | b, {a})
dop(a >> b, {a})
dop(a << b, {a})
dop(a & b, {a,b})
dop(a & b >> (c >> a), {b,c})
dop(a & b | b & c, {b,c})
dop(~a & ~~~b, {})
dop(a >> (b >> c), {a, b})
dop(a >> (b >> c), {a, b, c})
dop(a >> b >> c, {a, c})
dop(((c | ~b) >> (b | c)) >> (b | c), {a, c})
dop(a | ~a, {})
dop(a >> a, {a})
dop(a << a, {})
dop((a >> b) | (b >> a), {})
dop((~a | b) | (~b | a), {})
dop((~a | a) | (~b | b), {})
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment