Examples

Programming Systems

Gert Smolka

Publications

Teaching

Software

Formalizations

Satisfiable Formulas

  <r>p & [r](~p | q)

  [r](p -> q) -> [r]p -> [r]q

  <r>p & <r>~p

  ~(E p -> <r>p)

  E p -> A p

  {transitive: r}  ([r]p -> p) & [r]([r]p -> p) & ~p

  {transitive: r}  [r][r][r][r][r]0

Unsatisfiable Formulas

  <r>p & [r](~p & q)

  ~([r](p -> q) -> [r]p -> [r]q)

  <r>p & <r>~p & [r]=x

  ~(<r>p -> E p)

  A(~=x | p) & @x~p

  E(=x & p) & @x~p

  {transitive: r}  ~([r]p -> [r][r]p)

  {transitive: r}  ([r]p -> p) & [r]([r]p -> p) & ~p & [r][r][r][r][r]0

  {reflexive: r}  p & [r]~p

  {serial: *}  E[r]0