Eqelim Module
Equality elimination: Brand transform etc.
Table of contents
Brand's S- and T-modifications
Functions and values
| Function or value | Description |
Full Usage:
modify_S cl
Parameters: Returns: formula<fol> list list
The list of all the clauses that arise from all the possible
combinations of forward and backward positive equations in the original
clause. If \(n\) is the number of positive equation in the input
clause, \(2^n\) clauses are returned.
|
Applies Brand's S-modification to a clause. It allows to eliminate the symmetry axiom of equality.
Example
Multiple items
module List from Microsoft.FSharp.Collections -------------------- type List<'T> = | op_Nil | op_ColonColon of Head: 'T * Tail: 'T list interface IReadOnlyList<'T> interface IReadOnlyCollection<'T> interface IEnumerable interface IEnumerable<'T> member GetReverseIndex: rank: int * offset: int -> int member GetSlice: startIndex: int option * endIndex: int option -> 'T list static member Cons: head: 'T * tail: 'T list -> 'T list member Head: 'T member IsEmpty: bool member Item: index: int -> 'T with get ... val map: mapping: ('T -> 'U) -> list: 'T list -> 'U list
Evaluates to
|
|
Applies Brand's T-modification to a clause. It allows to eliminate the transitivity axiom of equality.
Example
[`~t1 = w''`; `s1 = w''`; `~t2 = w'`; `s2 = w'`; `~t3 = w`; `s3 = w`; `~s1 = t1`; `~s2 = t2`].
|
Brand's E-modification
Functions and values
| Function or value | Description | ||||
|
E-modifies a clause avoiding the variables names indicated in the input list.
E-modification allows to eliminate the congruence axioms of equality.
The function repeatedly pulls out non-variable immediate subterms \(t\)
of function and predicate symbols (other than equality) using the
following formulas, which are equivalences in the presence of the
congruence and reflexivity axioms:
\begin{align*}
f (\ldots , t, \ldots) = s \ &\Leftrightarrow \ \forall w.\ t = w \Rightarrow f (\ldots , w, \ldots) = s, \\
s = f (\ldots , t, \ldots) \ &\Leftrightarrow \ \forall w.\ t = w \Rightarrow s = f (\ldots , w, \ldots), \\
P (\ldots , t, \ldots) \ &\Leftrightarrow \ \forall w.\ t = w \Rightarrow P(\ldots , w, \ldots).
\end{align*}
Example
[`~y * z = w'`; `~x * y = w`; `w * z = x * w'`].
|
||||
|
Tries to find a nested non-variable subterm inside a term.
Example
``0``.
Example
System.Exception: findnvsubt.
Example
System.Collections.Generic.KeyNotFoundException: An index satisfying the predicate was not found in the collection.
|
||||
|
Tries to find a non-variable term inside a formula.
Example
``0``.
Example
``0``.
Example
System.ArgumentException: find_nvsubterm: not a literal
(Parameter 'fm')
Example
System.Exception: tryfind.
|
||||
Full Usage:
is_nonvar tm
Parameters:
term
-
The input term.
Returns: bool
true, if the input is a non-variable term; otherwise, false.
|
Checks if the input is a non-variable term.
Example
true.
Example
false.
|
||||
|
Brand's E-modification
E-modification allows to eliminate the congruence axioms of equality.
The function repeatedly pulls out non-variable immediate subterms \(t\)
of function and predicate symbols (other than equality) using the
following formulas, which are equivalences in the presence of the
congruence and reflexivity axioms:
\begin{align*}
f (\ldots , t, \ldots) = s \ &\Leftrightarrow \ \forall w.\ t = w \Rightarrow f (\ldots , w, \ldots) = s, \\
s = f (\ldots , t, \ldots) \ &\Leftrightarrow \ \forall w.\ t = w \Rightarrow s = f (\ldots , w, \ldots), \\
P (\ldots , t, \ldots) \ &\Leftrightarrow \ \forall w.\ t = w \Rightarrow P(\ldots , w, \ldots).
\end{align*}
Example
[`~y * z = w'`; `~x * y = w`; `w * z = x * w'`].
|
||||
Replaces terms in a formula based on the given substitution. Example
``f(1,1) = 1``.
|
|||||
Replaces subterms in a term based on the given substitution.
Example
``f(1,1)``.
|
Overall Brand transformation
Functions and values
| Function or value | Description |
Tests the validity of a formula by negating it and splitting in subproblems to be refuted by the MESON procedure with Brand's transformations incorporated.
Note
Prints the depth limits tried to the Example
[19] and prints to the stdout:
|
|
|
Tests the unsatisfiability of a formula using the MESON procedure with Brand's transformations incorporated.
Note
Prints the depth limits tried to the Example
1 and prints to the stdout:
|
Applies E-modification, then S-modification and T-modification; finally
it includes the reflexive clause
Example
[[`x = x`]; [`~f(w) = w'`; `x = w'`; `~0 = w`]; [`~x = w'`; `f(w) = w'`; `~0 = w`]].
|
|
Note
Prints the depth limits tried to the Example
[6] and prints to the stdout:
|