equal
deleted
inserted
replaced
5 \isamarkupsubsection{Propositional Dynamic Logic --- PDL% |
5 \isamarkupsubsection{Propositional Dynamic Logic --- PDL% |
6 } |
6 } |
7 % |
7 % |
8 \begin{isamarkuptext}% |
8 \begin{isamarkuptext}% |
9 \index{PDL|(} |
9 \index{PDL|(} |
10 The formulae of PDL are built up from atomic propositions via the customary |
10 The formulae of PDL\footnote{The customary definition of PDL |
11 propositional connectives of negation and conjunction and the two temporal |
11 \cite{HarelKT-DL} looks quite different from ours, but the two are easily |
|
12 shown to be equivalent.} are built up from atomic propositions via |
|
13 negation and conjunction and the two temporal |
12 connectives \isa{AX} and \isa{EF}. Since formulae are essentially |
14 connectives \isa{AX} and \isa{EF}. Since formulae are essentially |
13 syntax trees, they are naturally modelled as a datatype:% |
15 syntax trees, they are naturally modelled as a datatype:% |
14 \end{isamarkuptext}% |
16 \end{isamarkuptext}% |
15 \isacommand{datatype}\ formula\ {\isacharequal}\ Atom\ atom\isanewline |
17 \isacommand{datatype}\ formula\ {\isacharequal}\ Atom\ atom\isanewline |
16 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Neg\ formula\isanewline |
18 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Neg\ formula\isanewline |