Generate omniscience principles better

minimal.py

import itertools
from principles import *

def powerset(iterable):
    s = list(iterable)
    for r in range(len(s) + 1):
        yield from itertools.combinations(s, r)

class Kripke:
    def __init__(self, terms, sucs=frozenset(), px=frozenset(), abnormal=False):
        self.terms = frozenset(terms)
        self.sucs = frozenset(sucs)
        self.px = frozenset(px)
        self.abnormal = abnormal

    def possibles(self, below=frozenset()):
        px = self.px | frozenset(below)
        remaining = self.terms - px
        for added in powerset(remaining):
            new_px = px | frozenset(added)
            if self.sucs:
                new_sucs_poss = (suc.possibles(added) for suc in self.sucs)
                for configuration in itertools.product(*new_sucs_poss):
                    yield Kripke(self.terms, configuration, new_px, self.abnormal)
            else:
                yield Kripke(self.terms, self.sucs, new_px, self.abnormal)

    def __str__(self):
        if len(self.sucs) > 1:
            raise NotImplementedError
        if len(self.sucs) == 1:
            above = ' --> ' + str(next(iter(self.sucs)))
        else:
            above = ''
        return str(self.px) + above

    def separate(self, formulae):
        holds = []
        fails = []
        for formula in formulae:
            if all(formula.forcedby(s) for s in self.possibles()):
                holds.append(formula)
            else:
                fails.append(formula)
        return holds, fails

def AbnormalKripke(terms, sucs=frozenset(), px=frozenset()):
    return Kripke(terms, sucs, px, abnormal=True)

tautologies = find_tautologies()

two_world_growing_bot = Kripke([0], [AbnormalKripke([0, 1])])
h, f = two_world_growing_bot.separate(tautologies)
for x in h: print(x)
print('------------------------------')
for x in f: print(x)

principles.py

import itertools

class Formula:
    def __lt__(self, other):
        return str(self) < str(other)

    def __eq__(self, other):
        return repr(self) == repr(other)

    def __rshift__(self, other):
        return Impl(self, other)

    def __xor__(self, other):
        # Normalisation: symmetry
        if self < other:
            return Conj(self, other)
        else:
            return Conj(other, self)

    def __or__(self, other):
        # Normalisation: symmetry
        if self < other:
            return Disj(self, other)
        else:
            return Disj(other, self)

    def __invert__(self):
        # Normalisation: triple negation == negation
        if is_doubleneg(self):
            return self.form
        # Normalisation: not exists not not == not exists
        if isinstance(self, Exis) and is_doubleneg(self.form):
            return ~E(maybe_doubleneg_extract(self.form))
        return Nega(self)

def V(f):
    # Normalisation: forall not == not exists
    if isinstance(f, Nega):
        return ~E(f.form)
    return Univ(f)

def E(f):
    return Exis(f)

def paren(f):
    if isinstance(f, BinOp):
        return f'({f})'
    return str(f)

class UniOp(Formula):
    def __init__(self, form):
        self.form = form

    def __str__(self):
        return '{}{}'.format(self.op, paren(self.form))

    def __repr__(self):
        return '{}({})'.format(type(self).__name__, repr(self.form))

    def __eq__(self, other):
        return (self.op, self.form) == (other.op, other.form)

class BinOp(Formula):
    def __init__(self, left, right):
        self.left = left
        self.right = right

    def __str__(self):
        return '{} {} {}'.format(paren(self.left), self.op, paren(self.right))

    def __repr__(self):
        return '{}({}, {})'.format(type(self).__name__, repr(self.left), repr(self.right))

    def __eq__(self, other):
        return (self.left, self.op, self.right) == (other.left, other.op, other.right)

class Impl(BinOp):
    op = '⇒'
    __hash__ = lambda s: hash(repr(s))

    def val(self, tt_row, x=None):
        return (not self.left.val(tt_row, x)) or self.right.val(tt_row, x)

    def rterm(self, term):
        return Impl(self.left.rterm(term), self.right.rterm(term))

    def forcedby(self, world):
        if not self.left.forcedby(world) or self.right.forcedby(world):
            return all(self.forcedby(s) for s in world.sucs)
        else:
            return False

class Conj(BinOp):
    op = '∧'
    __hash__ = lambda s: hash(repr(s))

    def val(self, tt_row, x=None):
        return self.left.val(tt_row, x) and self.right.val(tt_row, x)

    def rterm(self, term):
        return Conj(self.left.rterm(term), self.right.rterm(term))

    def forcedby(self, world):
        return self.left.forcedby(world) and self.right.forcedby(world)

class Disj(BinOp):
    op = '∨'
    __hash__ = lambda s: hash(repr(s))

    def val(self, tt_row, x=None):
        return self.left.val(tt_row, x) or self.right.val(tt_row, x)

    def rterm(self, term):
        return Disj(self.left.rterm(term), self.right.rterm(term))

    def forcedby(self, world):
        return self.left.forcedby(world) or self.right.forcedby(world)

class Univ(UniOp):
    op = '∀x'
    __hash__ = lambda s: hash(repr(s))

    def val(self, tt_row, x=None):
        return all(self.form.val(tt_row, y) for y in range(len(tt_row)))

    def rterm(self, term):
        return self

    def forcedby(self, world):
        if all(self.form.rterm(t).forcedby(world) for t in world.terms):
            return all(self.forcedby(s) for s in world.sucs)
        else:
            return False

class Exis(UniOp):
    op = '∃x'
    __hash__ = lambda s: hash(repr(s))

    def val(self, tt_row, x=None):
        return any(self.form.val(tt_row, y) for y in range(len(tt_row)))

    def rterm(self, term):
        return self

    def forcedby(self, world):
        return any(self.form.rterm(t).forcedby(world) for t in world.terms)

class Nega(UniOp):
    op = '¬'
    __hash__ = lambda s: hash(repr(s))

    def val(self, tt_row, x=None):
        return not self.form.val(tt_row, x)

    def rterm(self, term):
        return Nega(self.form.rterm(term))

    def forcedby(self, world):
        if (world.abnormal or not self.form.forcedby(world)):
            return all(self.forcedby(s) for s in world.sucs)
        else:
            return False

class Pred(Formula):
    op = "Pred"
    __hash__ = lambda s: hash(repr(s))

    def __init__(self, name):
        self.name = name
        self.form = self.name

    def __str__(self):
        return str(self.name)

    def __repr__(self):
        return 'Pred({})'.format(repr(self.name))

    def val(self, tt_row, x=None):
        return tt_row[x]

    def rterm(self, term):
        return TermPred(self.name[:-1], term)

class TermPred(Formula):
    op = "TermPred"
    __hash__ = lambda s: hash(repr(s))

    def __init__(self, name, term):
        self.name = name + str(term)
        self.form = self.name
        self.term = term

    def __str__(self):
        return str(self.name)

    def __repr__(self):
        return 'TermPred({}, {})'.format(repr(self.name), self.term)

    def forcedby(self, world):
        return self.term in world.px

Px = Pred('Px')
P0 = TermPred('P', 0)
P1 = TermPred('P', 1)

def is_tautology(f, n=2):
    tt = list(itertools.product((True, False), repeat=n))
    return all(f.val(row) for row in tt)

def negations(fs):
    for f in fs:
        yield f
        yield ~f
        yield ~~f

def generalisations(fs):
    for f in fs:
        yield V(f)
        yield E(f)

def binaries(fs):
    for f, g in itertools.combinations(fs, 2):
        yield f >> g
        yield g >> f
        yield f ^ g
        yield f | g


def is_doubleneg(f):
    if not isinstance(f, Nega):
        return False
    return isinstance(f.form, Nega)

def maybe_doubleneg_extract(f):
    if is_doubleneg(f):
        return f.form.form
    else:
        return f

def is_doubleneg_of(f, g):
    if not is_doubleneg(f):
        return False
    return f.form.form == g

def is_complex_doubleneg_of(f, g):
    if is_doubleneg_of(f, g):
        return True
    ef = maybe_doubleneg_extract(f)
    if isinstance(ef, UniOp) and isinstance(g, UniOp) and ef.op == g.op:
        return ef.form == g.form or is_doubleneg_of(ef.form, g.form)

def weakening_filter(f):
    if isinstance(f, BinOp):
        if f.left == f.right:
            return True
    if isinstance(f, Impl):
        return is_complex_doubleneg_of(f.right, f.left)
    return False

def iter_omniscience():
    for f in binaries(negations(generalisations(negations((Px, ))))):
        if not weakening_filter(f):
            yield f

def principles():
    return set(iter_omniscience())

def find_tautologies():
    for f in sorted(principles(), key=str):
        if is_tautology(f):
            yield f

if __name__ == '__main__':
    for taut in find_tautologies():
        print(taut)
    print(len(set(map(str, iter_omniscience()))))

principles_found.txt

ExPx v Ex~Px
ExPx v ~ExPx
ExPx v ~VxPx
ExPx v ~~Ex~Px
Ex~Px -> ~VxPx
Ex~Px v Ex~~Px
Ex~Px v VxPx
Ex~Px v ~Ex~Px
Ex~Px v ~~ExPx
Ex~Px v ~~VxPx
Ex~~Px -> ExPx
Ex~~Px -> ~~ExPx
Ex~~Px v ~ExPx
Ex~~Px v ~VxPx
Ex~~Px v ~~Ex~Px
VxPx -> ExPx
VxPx -> Ex~~Px
VxPx -> ~Ex~Px
VxPx -> ~~ExPx
VxPx v ~VxPx
VxPx v ~~Ex~Px
~ExPx -> Ex~Px
~ExPx -> ~VxPx
~ExPx -> ~~Ex~Px
~ExPx v ~~ExPx
~Ex~Px -> ExPx
~Ex~Px -> Ex~~Px
~Ex~Px -> VxPx
~Ex~Px -> ~~ExPx
~Ex~Px -> ~~VxPx
~Ex~Px v ~VxPx
~Ex~Px v ~~Ex~Px
~VxPx -> Ex~Px
~VxPx -> ~~Ex~Px
~VxPx v ~~ExPx
~VxPx v ~~VxPx
~~ExPx -> ExPx
~~ExPx -> Ex~~Px
~~ExPx v ~~Ex~Px
~~Ex~Px -> Ex~Px
~~Ex~Px -> ~VxPx
~~Ex~Px v ~~VxPx
~~VxPx -> ExPx
~~VxPx -> Ex~~Px
~~VxPx -> VxPx
~~VxPx -> ~Ex~Px
~~VxPx -> ~~ExPx

Improving on https://gist.github.com/louisswarren/3f31905b1128ad8cfd4c3395a45b3339