Generate all tautologies

tautologies.py

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()