Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Generate all tautologies
from itertools import product, permutations
from pyaccum import accumulate
class Proposition:
def __invert__(self):
return Impl(self, bottom)
def __or__(self, other):
return Disj(self, other)
def __rshift__(self, other):
return Impl(self, other)
def __xor__(self, other):
return Conj(self, other)
def evaluate(self):
raise NotImplementedError
def __hash__(self):
return 1
class Symbol(Proposition):
def __init__(self, name):
self.name = name
self.value = None
self.dependencies = {self}
def __str__(self):
return self.name
def set_value(self, value):
self.value = value
def evaluate(self):
return self.value
bottom = Symbol('#')
P = Symbol('P')
Q = Symbol('Q')
R = Symbol('R')
#
# Formulae
#
class Formula(Proposition):
def __init__(self, *components):
self.components = set()
for component in components:
if isinstance(component, type(self)):
self.components.update(component.components)
else:
self.components.add(component)
self.dependencies = set.union(*(c.dependencies for c in self.components))
class Impl(Formula):
def __init__(self, premise, conclusion):
# (P -> (Q -> R)) <=> (P ^ Q -> R)
if isinstance(conclusion, Impl):
self.premise = Conj(premise, conclusion.premise)
self.conclusion = conclusion.conclusion
else:
self.premise = premise
self.conclusion = conclusion
self.dependencies = premise.dependencies.union(conclusion.dependencies)
def __str__(self):
if self.conclusion is bottom:
return '~{}'.format(self.premise)
return '({} -> {})'.format(self.premise, self.conclusion)
def __repr__(self):
if self.conclusion is bottom:
return '~{}'.format(self.premise)
return '({} >> {})'.format(self.premise, self.conclusion)
def evaluate(self):
return not(self.premise.evaluate()) or self.conclusion.evaluate()
class Conj(Formula):
def __str__(self):
return repr(self)
def __repr__(self):
return '({})'.format(' ^ '.join(sorted(str(c) for c in self.components)))
def evaluate(self):
return all(c.evaluate() for c in self.components)
class Disj(Formula):
def __str__(self):
return '({})'.format(' v '.join(sorted(str(c) for c in self.components)))
def __repr__(self):
return '({})'.format(' | '.join(sorted(str(c) for c in self.components)))
def evaluate(self):
return any(c.evaluate() for c in self.components)
#
# Tautology test
#
def is_tautology(prop):
atomics = prop.dependencies
truth_values = product((True, False), repeat=len(atomics))
assignments = ({k: v for k, v in zip(atomics, t)} for t in truth_values)
for assignment in assignments:
for atomic in atomics:
atomic.set_value(assignment[atomic])
if not prop.evaluate():
return False
return True
#
# Proposition generation
#
# Should use set actually
@accumulate(set)
def trees(symbols, level):
yield from symbols
if level > 0:
prev_trees = trees(symbols, level - 1)
for tree in prev_trees:
yield Impl(tree, bottom)
for left, right in permutations(prev_trees, 2):
yield Impl(left, right)
yield Conj(left, right)
yield Disj(left, right)
#
# Testing
#
assert(str(P >> Q) == '(P -> Q)')
assert((P >> Q).dependencies == {P, Q})
assert(repr(P >> (Q >> (P >> R))) == repr((P ^ Q) >> R))
assert(repr(Conj(P, Q, R)) == repr((P ^ Q ^ R)) == '(P ^ Q ^ R)')
assert((P | Q ^ P ^ P ^ P).dependencies == {P, Q})
assert(str(Disj(P, Q, R)) == str(P | Q | R) == '(P v Q v R)')
assert(str((P ^ Q ^ R) | P | Q) == '((P ^ Q ^ R) v P v Q)')
assert(str((P ^ R) >> ~Q | bottom) == '(# v ~(P ^ Q ^ R))')
# Order of traversal shoudn't matter
assert(sorted(map(str, trees((P, Q, R, bottom), 2)))
== sorted(map(str, trees((P, bottom, R, Q), 2))))
assert(is_tautology(P >> P))
assert(is_tautology((P ^ Q) >> P))
assert(is_tautology((P >> Q) | (Q >> P)))
assert(is_tautology(P | ~P))
assert(is_tautology(~(P ^ ~P)))
assert(not(is_tautology(P | Q)))
assert(not(is_tautology(P >> Q)))
def main():
all_propositions = trees((P, Q, R), 2)
n = 0
for prop in all_propositions:
if is_tautology(prop):
print(prop)
n += 1
print("Found", n)
if __name__ == '__main__':
main()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment