Davide Grossi edited untitled.tex  about 8 years ago

Commit id: a471e6e762c8a43f76262ba2392189d370828a05

deletions | additions      

       

And what follows is the definition of the semantics, which is provided in an algebraic fashion.  \begin{definition}  Let $\phi \in \L^{\K^{\mu}}$. The satisfaction of $\phi$ by a pointed argumentation model $(\mathcal{M}, a)$ is inductively defined as follows:  \begin{eqnarray*} \begin{align*}  \Model, a \not\models \bot &&  \\ \Model, a \models p \ & \IFF&  a \in \Val(p), \mbox{ for } p \in {\bf P} \\ \Model, a \models \neg \phi & \IFF&  a \not\in \true{\phi}_\Model \\ \Model, a \models \phi_1 \wedge \phi_2 & \IFF&  a \in \true{\phi_1}_\Model \cap \true{\phi_2}_\Model \\ \Model, a \models \ldia \phi & \IFF&  a \in \{ b \mid \exists c: b R c \ \& \ c \in \true{\phi}_\Model \} \\ \Model, a \models \mu p. \phi(p) & \IFF&  a \in \bigcap \{ X \in 2^A \mid \true{\phi}_{\Model[p:=X]} \subseteq X \} \end{eqnarray*} \end{align*}  where $\true{\phi}_{\Model[p:=X]}$ denotes the truth-set of $\phi$ once $\Val(p)$ is set to be $X$. As usual, we say that: $\phi$ is valid in an argumentation model $\mathcal{M}$ iff it is satisfied in all pointed models of $\mathcal{M}$, i.e., $\mathcal{M} \models \phi$; $\phi$ is valid in a class $\mathfrak{M}$ of argumentation models iff it is valid in all its models, i.e., $\mathfrak{M} \models \phi$.   %All definitions are naturally generalizable to sets of formulae $\Phi$.  \end{definition}