Agent Dynamic Logic package

Examples of formulae

The following sequence of formulae is accepted by the parser as it is.
```[a*]_a0 p
~[a*]_a0 p
K_i p
W_i q
<a>_i p
[a]_i q
Comm_i a;b
A_i a;b
Comm_i a+b
A_i a+b
Comm_i a*
A_i a*
Comm_i ?(p)
A_i ?(p)
Comm_i a+b & A_i a+b
Comm_i a;b & A_i a;b
Comm_i a* & A_i a*
Comm_j ?(Comm_i a* & A_i a*)
Comm_i(a+b;d)*&A_i(a+b;d)*
[?([c c a;c u b + ?(p&~q & s|r->t)]_i3 K_i0 W_i1 (p->FALSE))]_i0 (p->q->r)
~[?([c c a;c u b + ?(p&~q & s|r->t)]_i3 ~K_i0 ~ W_i1 ~(p->FALSE))]_i0 ~(p->q->r)
[?([c c a;c u b + ?(p&~q & s|r->t)]_i3 ~K_i0 W_i1 ~(p->FALSE))]_i0 (p->q->r)
Comm_i(c(c(c(c(c(a);b);b);b);b);b)
A_i(c(c(c(c(c(a);b);b);b);b);b)
Comm_i(c(a)*)
Comm_i(c(c(c(c(a)*)*)*)*)
A_i(c(a)*)
A_i(c(c(c(c(a)*)*)*)*)
true
false
[a*]_a0 p->p&[a]_a0[a*]_a0 p
~([a*]_a0 p->p&[a]_a0[a*]_a0 p)
```
 There were 280858 visits of this page since Wed, 03 May 2006 20:57:56 BST. Last modified: Sat, 17 Mar 2007 18:58:33 GMT. Copyright ©2006 Dmitry Tishkovsky, School of Computer Science, The University of Manchester