Give the given constants bottom status.
Set the status of the given constants to the top value (as free as possible)
List all constants whose status is different in this
and
that
List all constants whose status is different in this
and
that
Determine whether the formula lc1 - lc2 = 0 & phi
is shielded
(for arbitrary phi
)
Determine whether the formula lc1 - lc2 = 0 & phi
is shielded
(for arbitrary phi
)
Given a constraint from which all shielded parts have been removed, determine which constants have to be considered as non-free
Only used for runtime assertion purposes
Determine whether c
is a formula of the shape
a*x + t = 0 & phi
, where a != 0
and
x
is a quasi-universal constant that is maximal in
a*x + t = 0
.
Determine whether c
is a formula of the shape
a*x + t = 0 & phi
, where a != 0
and
x
is a quasi-universal constant that is maximal in
a*x + t = 0
.
Determine the (disjunctively connected) unshielded part of a formula
Class to represent the set of constants that are considered as "free" (i.e., that are only unifiable with themselves). Objects of this class are stored in the nodes of proof tree and are updated when the proof is expanded in order to eventually reach a fixed point.
TODO: avoid the creation of new objects whenever possible