Sorted by


Refresh


Filtered by

Automaton Type

Select / Deselect All














State Size

Select / Deselect All






Formula Length

Select / Deselect All






Temporal Hierarchy

Select / Deselect All








Spec Patterns

Select / Deselect All











Refresh


Grouped By


Refresh

(¬ q ∧ ¬ r) S (¬ p ∧ ¬ q ∧ ¬ r) Equivalent: (¬ q ∧ ¬ r) S (¬ p ∧ ¬ q ∧ ¬ r) ¬ (p B (q ∨ r)) ¬ (p B q ∨ p B r) ¬ q S (¬ p ∧ ¬ q) ∧ ¬ r S (¬ p ∧ ¬ r)
Complement: p B (q ∨ r) p B q ∨ p B r
NBW
¬ (p S q) Equivalent: ¬ (p S q) ¬ q B (¬ p ∧ ¬ q) ¬ ((p S q) S q) ¬ (p B q ∧ O q) ¬ (p S p S q) ¬ (q ∨ p ∧ Y (p S q)) ¬ q ∧ (¬ p ∨ Z (¬ q B (¬ p ∧ ¬ q))) ¬ q B (¬ q B (¬ p ∧ ¬ q) ∧ ¬ q) ¬ q S (¬ p ∧ ¬ q) ∨ H ¬ q (¬ q B (¬ p ∧ ¬ q)) B (¬ p ∧ ¬ q B (¬ p ∧ ¬ q))
Complement: (p ∨ q) S (q ∧ (p ∨ q)) ¬ (¬ q B (¬ p ∧ ¬ q)) p S q (p S q) S q G p S q p B q ∧ O q p S p S q q ∨ p ∧ Y (p S q)
NBW
¬ q S (¬ p ∧ ¬ q) Equivalent: ¬ (p B q) ¬ q S (¬ p ∧ ¬ q) ¬ ((p B q) B q) ¬ (p B p B q) ¬ (p S q ∨ H p) ¬ (q ∨ p ∧ Z (p B q)) ¬ q ∧ (¬ p ∨ Y (¬ q S (¬ p ∧ ¬ q))) ¬ q B (¬ p ∧ ¬ q) ∧ O ¬ p ¬ q S (¬ q S (¬ p ∧ ¬ q) ∧ ¬ q) (¬ q S (¬ p ∧ ¬ q)) S (¬ p ∧ ¬ q S (¬ p ∧ ¬ q))
Complement: (p ∨ q) B (q ∧ (p ∨ q)) ¬ (¬ q S (¬ p ∧ ¬ q)) p B q (p B q) B q p B p B q p S q ∨ H p q ∨ p ∧ Z (p B q)
NBW
H p Equivalent: O p ¬ O ¬ p ¬ H ¬ p True S p H p p B False O O p F (p B False) F H p H H p G (True S p) G O p p ∧ Z H p p ∨ Y O p
Complement: ¬ (True S p) ¬ (p B False) O ¬ p ¬ O p ¬ H p True S (¬ p ∧ True) H ¬ p ¬ p B (False ∧ ¬ p) ¬ (p ∧ Z H p) O O ¬ p ¬ (p ∨ Y O p) F (¬ p B (False ∧ ¬ p)) ¬ O O p F H ¬ p ¬ F (p B False) ¬ F H p ¬ H H p ¬ G (True S p) H H ¬ p G (True S (¬ p ∧ True)) ¬ G O p ¬ p ∧ Z H ¬ p ¬ p ∨ Y O ¬ p G O ¬ p
NBW
H ¬ p Equivalent: ¬ (True S p) ¬ (p B False) O ¬ p ¬ O p ¬ H p True S (¬ p ∧ True) H ¬ p ¬ p B (False ∧ ¬ p) ¬ (p ∧ Z H p) O O ¬ p ¬ (p ∨ Y O p) F (¬ p B (False ∧ ¬ p)) ¬ O O p F H ¬ p ¬ F (p B False) ¬ F H p ¬ H H p ¬ G (True S p) H H ¬ p G (True S (¬ p ∧ True)) ¬ G O p ¬ p ∧ Z H ¬ p ¬ p ∨ Y O ¬ p G O ¬ p
Complement: O p ¬ O ¬ p ¬ H ¬ p True S p H p p B False O O p F (p B False) F H p H H p G (True S p) G O p p ∧ Z H p p ∨ Y O p
NBW
p B (q ∨ r) Equivalent: p B (q ∨ r) p B q ∨ p B r
Complement: (¬ q ∧ ¬ r) S (¬ p ∧ ¬ q ∧ ¬ r) ¬ (p B (q ∨ r)) ¬ (p B q ∨ p B r) ¬ q S (¬ p ∧ ¬ q) ∧ ¬ r S (¬ p ∧ ¬ r)
NBW
¬ r S ((¬ p ∨ ¬ q) ∧ ¬ r) Equivalent: ¬ ((p ∧ q) B r) ¬ r S ((¬ p ∨ ¬ q) ∧ ¬ r) ¬ (p B r ∧ q B r) ¬ r S (¬ p ∧ ¬ r) ∨ ¬ r S (¬ q ∧ ¬ r)
Complement: (p ∧ q) B r p B r ∧ q B r
NBW
(p ∧ q) W r Equivalent: (p ∧ q) W r p W r ∧ q W r
Complement: ¬ ((p ∧ q) W r) ¬ r U ((¬ p ∨ ¬ q) ∧ ¬ r) ¬ (p W r ∧ q W r) ¬ r U (¬ p ∧ ¬ r) ∨ ¬ r U (¬ q ∧ ¬ r)
NBW
¬ (¬ q U (¬ p ∧ ¬ q)) Equivalent: (p ∨ q) W (q ∧ (p ∨ q)) ¬ (¬ q U (¬ p ∧ ¬ q)) q R ¬ (¬ p ∧ ¬ q) p W q (p W q) W q G (¬ p → O q) p U p W q p U q ∨ G p p W p U q p W p W q q ∨ p ∧ X (p W q) G (O ¬ p → O q)
Complement: ¬ (p W q) ¬ q U (¬ p ∧ ¬ q) ¬ ((p W q) W q) ¬ (p U p W q) ¬ (p U q ∨ G p) ¬ (p W p U q) ¬ (p W p W q) ¬ (q ∨ p ∧ X (p W q)) ¬ p R ¬ (p W q) ¬ q ∧ (¬ p ∨ X (¬ q U (¬ p ∧ ¬ q))) ¬ q U (¬ q U (¬ p ∧ ¬ q) ∧ ¬ q) ¬ q W (¬ p ∧ ¬ q) ∧ F ¬ p (¬ q U (¬ p ∧ ¬ q)) U (¬ p ∧ ¬ q U (¬ p ∧ ¬ q)) (¬ q U (¬ p ∧ ¬ q)) W (¬ p ∧ ¬ q U (¬ p ∧ ¬ q)) (¬ q W (¬ p ∧ ¬ q)) U (¬ p ∧ ¬ q W (¬ p ∧ ¬ q)) F (O ¬ p ∧ H ¬ q) ¬ G (O ¬ p → O q)
NBW
¬ (p U (q ∨ r)) Equivalent: (¬ q ∧ ¬ r) W (¬ p ∧ ¬ q ∧ ¬ r) ¬ (p U (q ∨ r)) ¬ p R ¬ (q ∨ r) ¬ (p U q ∨ p U r) ¬ q W (¬ p ∧ ¬ q) ∧ ¬ r W (¬ p ∧ ¬ r)
Complement: p U (q ∨ r) p U q ∨ p U r
NBW
¬ (p U q) Equivalent: ¬ (p U q) ¬ p R ¬ q ¬ q W (¬ p ∧ ¬ q) ¬ ((p U q) U q) ¬ ((p U q) W q) ¬ ((p W q) U q) ¬ (p U p U q) ¬ (p U q) R ¬ q ¬ (p W q ∧ F q) ¬ (p W q) R ¬ q ¬ (q ∨ p ∧ X (p U q)) ¬ p R ¬ (p U q) ¬ q ∧ (¬ p ∨ X (¬ q W (¬ p ∧ ¬ q))) ¬ q U (¬ p ∧ ¬ q) ∨ G ¬ q ¬ q U (¬ q W (¬ p ∧ ¬ q) ∧ ¬ q) ¬ q W (¬ q U (¬ p ∧ ¬ q) ∧ ¬ q) ¬ q W (¬ q W (¬ p ∧ ¬ q) ∧ ¬ q) (¬ q W (¬ p ∧ ¬ q)) W (¬ p ∧ ¬ q W (¬ p ∧ ¬ q)) ¬ F (q ∧ Z H p) G (¬ q ∨ Y O ¬ p)
Complement: (p ∨ q) U (q ∧ (p ∨ q)) ¬ (¬ p R ¬ q) ¬ (¬ q W (¬ p ∧ ¬ q)) p U q (p U q) U q (p U q) W q (p W q) U q p U q U q p U p U q p W q ∧ F q q ∨ p ∧ X (p U q) F (q ∧ Z H p)
NBW
¬ (p U ¬ q) Equivalent: ¬ (p U ¬ q) q W (¬ p ∧ q) G (Z H p → q) G (Z H p → H q)
Complement: (p ∨ ¬ q) U (¬ q ∧ (p ∨ ¬ q)) ¬ (q W (¬ p ∧ q)) p U ¬ q F (Z H p ∧ ¬ q) ¬ G (Z H p → q) F (Z H p ∧ O ¬ q) ¬ G (Z H p → H q)
NBW
p ∧ G ¬ q Equivalent: ¬ (p → F q) p ∧ G ¬ q ¬ F (O (Z False ∧ p) → q) G (O (Z False ∧ p) ∧ ¬ q)
Complement: p → F q F (O (Z False ∧ p) → q)
NBW
¬ (¬ p U ¬ q) Equivalent: ¬ (¬ p U ¬ q) p R q q W (p ∧ q) q ∧ p ∨ q ∧ X (p R q)
Complement: ¬ (p R q) ¬ p U ¬ q (¬ q ∨ ¬ p) ∧ (¬ q ∨ X (¬ p U ¬ q)) ¬ (q ∧ p ∨ q ∧ X (p R q))
NBW
p W (q ∨ r) Equivalent: p W (q ∨ r) p W q ∨ p W r
Complement: (¬ q ∧ ¬ r) U (¬ p ∧ ¬ q ∧ ¬ r) ¬ (p W (q ∨ r)) ¬ (p W q ∨ p W r) ¬ q U (¬ p ∧ ¬ q) ∧ ¬ r U (¬ p ∧ ¬ r)
NBW