Home SQEMA SQEMA @ FMI Samples Thesis
Current: (((<0>[0][0]p And [0]q) -> (p -> q)) And (((<0>p Or <0>q) And ([0]p Or [0]q)) -> ([0][0]p And [0][0]q)))
Nominal Formula: ((Not (C1 -> <0>C2) Or (C1 And [0][0](C2 Or <0>-1C1))) And (Not (C1 -> <0>C3) Or (C1 And [0][0]C3)) And (Not (C1 -> <0>C4) Or (C1 And [0][0]C4)) And (Not (C1 -> <0>C5) Or (C1 And [0][0](C5 Or <0>-1C1))) And ((C1 And <0>-1C1) Or (C1 And [0]0)) And ((C1 And [0]0) Or (C1 And [0][0]<0>-1C1)) And (C1 And ([0]0 Or [0][0]0)))
First-Order Formula: For-All y1 For-All y2 For-All y3 For-All y4((Not (xRy1) Or For-All z1((xRz1) -> For-All z2((z1Rz2) -> ((z2 = y1) Or (xRz2))))) And (Not (xRy2) Or For-All z3((xRz3) -> For-All z4((z3Rz4) -> (z4 = y2)))) And (Not (xRy3) Or For-All z5((xRz5) -> For-All z6((z5Rz6) -> (z6 = y3)))) And (Not (xRy4) Or For-All z7((xRz7) -> For-All z8((z7Rz8) -> ((z8 = y4) Or (xRz8))))) And ((xRx) Or For-All z9Not (xRz9)) And (For-All z10Not (xRz10) Or For-All z11((xRz11) -> For-All z12((z11Rz12) -> (xRz12)))) And (For-All z13Not (xRz13) Or For-All z14((xRz14) -> For-All z15Not (z14Rz15))))
Legend:
Variable names start with a small latin letter and can contain small latin letters and numbers.
Names starting with a small letter 'c' are considered nominals.
#   - necessity.png - Necessity
@   - possibility.png - Possibility
#'  - necessity.png-1 - Reversed Necessity
@'  - possibility.png-1 - Reversed Possibility
[n] - Necessity with relation index, where n is a number
<n> - Possibility with relation index, where n is a number
[n]'- Reversed Necessity with relation index, where n is a number
<n>'- Reversed Possibility with relation index, where n is a number
&   - and.png - Conjunction
|   - or.png - Disjunction
~   - not.png - Negation
->  - Implication
<-  - Reversed Implication
<-> - Equivalence