Ternary Logic Laws

• Algebraic Laws:
  • AND_Commutative: \(x \wedge y \Leftrightarrow y \wedge x\)
  • OR_Commutative: \(x \vee y \Leftrightarrow y \vee x\)
  • ANDOR_Distributive: \(x \wedge (y \vee z) \Leftrightarrow x \wedge y \vee x \wedge z\)
  • ORAND_Distributive: \(x \vee y \wedge z \Leftrightarrow (x \vee y) \wedge (x \vee z)\)
  • AND_Associative: \(x \wedge y \wedge z \Leftrightarrow x \wedge y \wedge z\)
  • OR_Associative: \(x \vee y \vee z \Leftrightarrow x \vee y \vee z\)
  • AND_Neutral: \(x \wedge \mathsf{true} \Leftrightarrow x\)
  • OR_Neutral: \(x \vee \mathsf{false} \Leftrightarrow x\)
  • AND_Idempotency: \(x \wedge x \Leftrightarrow x\)
  • OR_Idempotency: \(x \vee x \Leftrightarrow x\)
  • AND_MaxElement: \(x \wedge \mathsf{false} \Leftrightarrow \mathsf{false}\)
  • OR_MaxElement: \(x \vee \mathsf{true} \Leftrightarrow \mathsf{true}\)
  • AND_Absorption: \(x \wedge (x \vee y) \Leftrightarrow x\)
  • OR_Absorption: \(x \vee x \wedge y \Leftrightarrow x\)
  • AND_DeMorgan: \(\neg (x \wedge y) \Leftrightarrow \neg x \vee \neg y\)
  • OR_DeMorgan: \(\neg (x \vee y) \Leftrightarrow \neg x \wedge \neg y\)
  • Involution: \(\neg \neg x \Leftrightarrow x\)
  • AND_KleeneLaw: \(x \wedge \neg x \wedge (y \vee \neg y) \Leftrightarrow x \wedge \neg x\)
  • OR_KleeneLaw: \(x \wedge \neg x \vee y \vee \neg y \Leftrightarrow y \vee \neg y\)
• Expressiveness of Sequential ITE:
  • Neg2SeqITE: \(\neg x \Leftrightarrow (x \Rightarrow \mathsf{false}\mid \mathsf{true})\)
  • And2SeqITE: \(x \wedge y \Leftrightarrow (\mathsf{abs}(x) \Rightarrow (y \Rightarrow \bot \mid \mathsf{false})\mid (x \Rightarrow y\mid \mathsf{false}))\)
  • Or2SeqITE: \(x \vee y \Leftrightarrow (\mathsf{abs}(x) \Rightarrow (y \Rightarrow \mathsf{true}\mid \bot )\mid (x \Rightarrow \mathsf{true}\mid y))\)
  • Inf2SeqITE: \((x \Leftrightarrow y \Rightarrow y\mid \bot ) \Leftrightarrow (x \Rightarrow \bot \vee y\mid \bot \wedge y)\)
  • ParITE2SeqITE: \(x \wedge y \vee \neg x \wedge z \vee y \wedge z \Leftrightarrow (\mathsf{abs}(x) \Rightarrow (y \Rightarrow \bot \vee z\mid \bot \wedge z)\mid (x \Rightarrow y\mid z))\)
  • SeqAnd2SeqITE: \(x \wedge (\neg x \vee y) \Leftrightarrow (x \Rightarrow y\mid \mathsf{false})\)
  • SeqOr2SeqITE: \(x \vee \neg x \wedge y \Leftrightarrow (x \Rightarrow \mathsf{true}\mid y)\)
  • Equality2SeqITE: \((x \Leftrightarrow y) \Leftrightarrow (\mathsf{abs}(x) \Rightarrow \mathsf{abs}(y)\mid (x \Rightarrow (\mathsf{abs}(y) \Rightarrow \mathsf{false}\mid y)\mid (\mathsf{abs}(y) \Rightarrow \mathsf{false}\mid \neg y)))\)
• Expressiveness of Parallel ITE:
  • Neg2ParITE: \(\neg x \Leftrightarrow x \wedge \mathsf{false} \vee \neg x \wedge \mathsf{true} \vee \neg x \wedge x\)
  • And2ParITE: \(x \wedge y \Leftrightarrow x \wedge y \vee \neg x \wedge \mathsf{false} \vee y \wedge \mathsf{false}\)
  • Or2ParITE: \(x \vee y \Leftrightarrow x \wedge \mathsf{true} \vee \neg x \wedge y \vee \mathsf{true} \wedge y\)
  • Inf2ParITE: \((x \Leftrightarrow y \Rightarrow y\mid \bot ) \Leftrightarrow x \wedge \bot \vee y \wedge \bot \vee x \wedge y\)
  • SeqITE2ParITE: \((x \Rightarrow y\mid z) \Leftrightarrow \mathsf{abs}(x) \wedge \bot \vee \neg \mathsf{abs}(x) \wedge (x \wedge y \vee \neg x \wedge z \vee \neg x \wedge x) \vee \neg \mathsf{abs}(x) \wedge \mathsf{abs}(x)\)
  • SeqAnd2ParITE: \(x \wedge (\neg x \vee y) \Leftrightarrow \mathsf{abs}(x) \wedge \bot \vee \neg \mathsf{abs}(x) \wedge x \wedge y \vee \neg \mathsf{abs}(x) \wedge \mathsf{abs}(x)\)
  • SeqOr2ParITE: \(x \vee \neg x \wedge y \Leftrightarrow \mathsf{abs}(x) \wedge \bot \vee \neg \mathsf{abs}(x) \wedge (x \vee y) \vee \neg \mathsf{abs}(x) \wedge \mathsf{abs}(x)\)
  • Guard2ParITE: \((g \Rightarrow t\mid \bot ) \Leftrightarrow g \wedge t \vee \neg g \wedge \bot \vee t \wedge \bot \)
• Expressiveness of Parallel Conjunction and Disjunction:
  • Inf2AndOr: \((x \Leftrightarrow y \Rightarrow x\mid \bot ) \Leftrightarrow x \wedge \bot \vee y \wedge \bot \vee x \wedge y\)
  • ParITE2AndOr: \((\mathsf{abs}(x) \Rightarrow (y \Leftrightarrow z \Rightarrow y\mid \bot )\mid (x \Rightarrow y\mid z)) \Leftrightarrow x \wedge y \vee \neg x \wedge z \vee y \wedge z\)
  • SeqITE2AndOr: \((x \Rightarrow y\mid z) \Leftrightarrow x \wedge y \vee \neg x \wedge z \vee \neg x \wedge x\)
  • SeqAnd2AndOr: \((x \Rightarrow y\mid \mathsf{false}) \Leftrightarrow x \wedge (\neg x \vee y)\)
  • SeqOr2AndOr: \((x \Rightarrow \mathsf{true}\mid y) \Leftrightarrow x \vee \neg x \wedge y\)
  • Guard2AndOr: \((g \Rightarrow t\mid \bot ) \Leftrightarrow g \wedge t \vee \neg g \wedge \bot \)
  • Equality2AndOr: \((x \Leftrightarrow y) \Leftrightarrow \mathsf{abs}(x) \wedge \mathsf{abs}(y) \vee \neg \mathsf{abs}(x) \wedge \neg \mathsf{abs}(y) \wedge (x \wedge y \vee \neg x \wedge \neg y)\)