Laws for Feature Algebra (OOP)

 
All presented properties are showed by automated theorem-prover Prover9.
(There is no special order in the presentation of the theorems.)
ID Name Lemma Duals
FT1 idempotence (as a consequence of distance idempotence) $x+x=x$ n/a
FT2 reflexivity (as a consequence of distance idempotence) $x\leq x$ n/a
FT3 transitivity (as a consequence of distance idempotence) $x \leq y \wedge y \leq z \Rightarrow x \leq z$ n/a
FT4 upper bound (as a consequence of distance idempotence) $x \leq x+y$
$y \leq x+y$
n/a
FT5 supremum (sum split) (as a consequence of distance idempotence) $x+y \leq z \Leftrightarrow x \leq z \wedge y \leq z$ n/a
FT6 quasicommutativity (as a consequence of distance idempotence) $\mbox{eqv}(x+y,y+x)$ n/a
FT7 isotony (as a consequence of distance idempotence) $x \leq y \Rightarrow x+z \leq y+z$
$x \leq y \Rightarrow z+x \leq z+y$
n/a
FT8 equivalence of superdistributivity and isotony (as a consequence of distance idempotence) $\forall x \forall y.(f(x)+f(y) \leq f(x+y)) \Leftrightarrow \forall x \forall y.(x \leq y \Rightarrow f(x) \leq f(y))$ n/a

In general, we write x,y... and a,b... for arbitrary semiring elements and p,q... for tests. If other letters are involved we adapted the original notation of the authors.
 
©2007. Peter Höfner