Sets
Variables and Atoms#
- class logic1.theories.Sets.atomic.VariableSet[source]#
Bases:
VariableSet
[Variable
]The infinite set of all variables belonging to the theory of Sets. Variables are uniquely identified by their name, which is a
str
. This class is a singleton, whose single instance is assigned toVV
.See also
Final methods inherited from parent class:
firstorder.atomic.VariableSet.get()
– obtain several variables simultaneously
firstorder.atomic.VariableSet.imp()
– import variables into global namespace
- __getitem__(index: str) Variable [source]#
Implements abstract method
firstorder.atomic.VariableSet.__getitem__()
.
- fresh(suffix: str = '') Variable [source]#
Return a fresh variable, by default from the sequence G0001, G0002, …, G9999, G10000, … This naming convention is inspired by Lisp’s gensym(). If the optional argument
suffix
is specified, the sequence G0001<suffix>, G0002<suffix>, … is used instead.
- abstract pop() None [source]#
- abstract push() None [source]#
Implement abstract methods
logic1.firstorder.atomic.VariableSet.pop()
andlogic1.firstorder.atomic.VariableSet.push()
.
- logic1.theories.Sets.atomic.VV = VariableSet()#
The unique instance of
VariableSet
.
- class logic1.theories.Sets.atomic.Variable[source]#
Bases:
Variable
[Variable
,Never
]- ==, !=
- __eq__(other: Variable) Eq [source]#
- __ne__(other: Variable) Ne [source]#
Construction of instances of
Eq
andNe
is available via overloaded operators.
- as_latex() str [source]#
LaTeX representation as a string. Implements the abstract method
firstorder.atomic.Term.as_latex()
.
- fresh() Variable [source]#
Returns a variable that has not been used so far. Implements abstract method
firstorder.atomic.Variable.fresh()
.
- static sort_key(term: Variable) str [source]#
A sort key suitable for ordering instances of this class. Implements the abstract method
firstorder.atomic.Term.sort_key()
.
- subs(d: dict[Variable, Variable]) Variable [source]#
Simultaneous substitution of variables for variables.
>>> from logic1.theories.Sets import VV >>> x, y, z = VV.get('x', 'y', 'z') >>> f = x >>> f.subs({x: y, y: z}) y
- vars() Iterator[Variable] [source]#
An iterator that yields this variable. Implements the abstract method
firstorder.atomic.Term.vars()
.
- class logic1.theories.Sets.atomic.AtomicFormula[source]#
Bases:
AtomicFormula
[AtomicFormula
,Variable
,Variable
,Never
]- __le__(other: Formula[AtomicFormula, Variable, Variable, Never]) bool [source]#
Returns True if this atomic formula should be sorted before or is equal to other. Implements abstract method
firstorder.atomic.AtomicFormula.__le__()
.
- __str__() str [source]#
String representation of this atomic formula. Implements the abstract method
firstorder.atomic.AtomicFormula.__str__()
.
- as_latex() str [source]#
Latex representation as a string. Implements the abstract method
firstorder.atomic.AtomicFormula.as_latex()
.
- bvars(quantified: frozenset[Variable] = frozenset({})) Iterator[Variable] [source]#
Iterate over occurrences of variables that are elements of quantified. Implements the abstract method
firstorder.atomic.AtomicFormula.bvars()
.
- classmethod complement() type[AtomicFormula] [source]#
Complement relation. Implements the abstract method
firstorder.atomic.AtomicFormula.complement()
.See also
Inherited method
firstorder.atomic.AtomicFormula.to_complement()
- fvars(quantified: frozenset[Variable] = frozenset({})) Iterator[Variable] [source]#
Iterate over occurrences of variables that are not elements of quantified. Implements the abstract method
firstorder.atomic.AtomicFormula.fvars()
.
- simplify() Formula[AtomicFormula, Variable, Variable, Never] [source]#
Fast basic simplification. The result is equivalent to self. Implements the abstract method
firstorder.atomic.AtomicFormula.simplify()
.
- class logic1.theories.Sets.atomic.Eq[source]#
- class logic1.theories.Sets.atomic.Ne[source]#
Bases:
AtomicFormula
Equations and inequalities between variables.
- logic1.theories.Sets.atomic.Index: TypeAlias = int | float#
An index, which is either a positive integer or the float inf, which is represented by
oo
- class logic1.theories.Sets.atomic.C[source]#
- class logic1.theories.Sets.atomic.C_[source]#
Cardinality constraints. From a mathematical perspective, the instances are constant relation symbols with an index, which is either a positive integer or the float inf, represented as
oo
.C(n)
holds iff there are at leastn
different elements in the universe. This is not a statement about the indexn
but about a range of models where this constant relation holds.In the following example,
f
states that there should be at least 2 elements but not 3 elements or more:>>> from logic1.firstorder import * >>> from logic1.theories.Sets import * >>> x, y, z = VV.get('x', 'y', 'z') >>> f = Ex([x, y], x != y) & All([x, y, z], Or(x == y, y == z, z == x)) >>> qe(f) # quantifier elimination: And(C(2), C_(3))
The class
C_
is dual toC
; more precisely, for every indexn
, we have thatC_(n)
is the dual relation ofC(n)
, and vice versa.The class constructors take care that instances with equal indices are identical:
>>> C(1) is C(1) True >>> C(1) == C(2) False
- property index: Index#
The index of the constant relation symbol