Sets

Simplification

This module implements deep simplification through the generation and propagation of internal representations during recursion. It is an adaptation of the standard simplifier from [DolzmannSturm-1997] tailored to the specific requirements of Sets.

Internal Representations

class logic1.theories.Sets.simplify.InternalRepresentation

Bases: InternalRepresentation[AtomicFormula, Variable, Variable, Never]

Implements the abstract methods add(), extract(), and next_() of it super class abc.simplify.InternalRepresentation. Required by Sets.simplify.Simplify for instantiating the type variable abc.simplify.ρ of abc.simplify.Simplify.

Simplification and Validity

class logic1.theories.Sets.simplify.Simplify

Bases: Simplify[AtomicFormula, Variable, Variable, Never, InternalRepresentation, Options]

Deep simplification in the style of [DolzmannSturm-1997]. Implements the abstract methods create_initial_representation and simpl_at of its super class abc.simplify.Simplify.

The simplifier should be called via simplify(), as described below. In addition, this class inherits abc.simplify.Simplify.is_valid(), which should be called via is_valid(), as described below.

User Interface

logic1.theories.Sets.simplify.simplify(f: Formula[AtomicFormula, Variable, Variable, Never], assume: Iterable[AtomicFormula] = []) → Formula[AtomicFormula, Variable, Variable, Never]

An example

>>> from logic1.firstorder import *
>>> from logic1.theories.Sets import *
>>> a, b, c, d = VV.get('a', 'b', 'c', 'd')
>>> simplify(And(a == b, b == c, c == d,  d == c), assume=[a == b])
And(a == c, a == d)

logic1.theories.Sets.simplify.is_valid(f: Formula[AtomicFormula, Variable, Variable, Never], assume: Iterable[AtomicFormula] = []) → bool | None

Some examples

>>> from logic1.firstorder import *
>>> from logic1.theories.Sets import *
>>> a, b, c, d = VV.get('a', 'b', 'c', 'd')

>>> is_valid(a == d, assume=[a == b, b == c, c == d])
True

>>> is_valid(a == d, assume=[a == b, b != c, c == d])
False

>>> is_valid(a == d, assume=[a != b, b != c, c != d])  # Returns None