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]

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[α, τ, χ, σ], assume: Iterable[α] = []) → Formula[α, τ, χ, σ]

Simplify f modulo assume.

Parameters:

• f – The formula to be simplified

• assume – A list of atomic formulas that are assumed to hold. The simplification result is equivalent modulo those assumptions.

Returns:

A simplified equivalent of f modulo assume.

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[α, τ, χ, σ], assume: Iterable[α] = []) → bool | None

Simplification-based heuristic test for vailidity of a formula.

Mathematical definition

A first-order formula is valid if it holds for all values all free variables.

Parameters:

• f – The formula to be tested for validity

• assume – A list of atomic formulas that are assumed to hold. The result of the validity test is correct modulo these assumptions.

Returns:

Returns True or False if abc.simplify.Simplify.simplify() succeeds in heuristically simplifying f to T or F, respectively. Returns None in the sense of “don’t know” otherwise.

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