\documentstyle[11pt]{article}		% Fontsize 11 point
\textwidth    		6.5 in		% paper = 8.5x11in
\textheight   		8.78in          %  + foot 30pt = 9.20in
\oddsidemargin		0   pt          % 1 inch margin comes for free
\evensidemargin 	0   pt          % 1 inch margin comes for free
\topmargin      	0   pt          % 3 margins of 1in each; bottom .8in
\headheight     	0   pt          % default 12pt = 0.42cm       
\headsep        	0   pt          % default 25pt = 0.88cm       
\unitlength		1   mm		% This is used in pictures

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%		On A4 paper the right margin is 6 mm smaller,		  %%%%
%%%%		whereas the bottom margin is 17.6 mm longer.		  %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newlength{\shiftside}			 \newlength{\shifttop}
\setlength{\shiftside}{-3mm}		 \setlength{\shifttop}{8.8mm}
\typeout{On what kind of paper are you going to print this?}
\typein[\paper]{Enter 0 for American paper or 1 for A4.}
\addtolength\oddsidemargin{\paper\shiftside}
\addtolength\evensidemargin{\paper\shiftside}
\addtolength\topmargin{\paper\shifttop}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%			Theorem-like environments			  %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newtheorem{defi}{Definition}
\newtheorem{theo}{Theorem}
\newtheorem{prop}{Proposition}
\newtheorem{lemm}{Lemma}
\newtheorem{coro}{Corollary}
\newtheorem{exam}{Example}
\newtheorem{solu}{Solution}

\newenvironment{definition}[1]{\begin{defi} \rm \label{df-#1} }{\end{defi}}
\newenvironment{theorem}[1]{\begin{theo} \rm \label{th-#1} }{\end{theo}}
\newenvironment{proposition}[1]{\begin{prop} \rm \label{pr-#1} }{\end{prop}}
\newenvironment{lemma}[1]{\begin{lemm} \rm \label{lem-#1} }{\end{lemm}}
\newenvironment{corollary}[1]{\begin{coro} \rm \label{cor-#1} }{\end{coro}}
\newenvironment{example}[1]{\begin{exam} \rm \label{ex-#1} }{\end{exam}}
\newenvironment{solution}[1]{\begin{solu} \rm \label{sol-#1} }{\end{solu}}
\newenvironment{proof}{\begin{trivlist} \item[\hspace{\labelsep}\bf Proof:]}{\hfill $\Box$\end{trivlist}}

\newcommand{\df}[1]{Definition~\ref{df-#1}}
\newcommand{\th}[1]{Theorem~\ref{th-#1}}
\newcommand{\pr}[1]{Proposition~\ref{pr-#1}}
\newcommand{\lem}[1]{Lemma~\ref{lem-#1}}
\newcommand{\cor}[1]{Corollary~\ref{cor-#1}}
\newcommand{\ex}[1]{Example~\ref{ex-#1}}
\newcommand{\sol}[1]{Solution~\ref{sol-#1}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\renewcommand{\title}[1]{ \vspace*{5pt}
			\setcounter{footnote}{0}
			\renewcommand{\thefootnote}{\fnsymbol{footnote}}
			\begin{center}
			{\LARGE \bf #1\\ \ \\}
			R.J. van Glabbeek\makebox[0pt][l]{\footnotemark}\\
			\footnotesize
			Computer Science Department, Stanford University\\
			Stanford, CA 94305, USA.\\
			{\tt rvg@cs.stanford.edu}
			\end{center}
			\footnotetext{This work was supported by ONR under
			grant number N00014-92-J-1974.}
			\renewcommand{\thefootnote}{\arabic{footnote}}
			\setcounter{footnote}{0}
			\vspace{5pt}			}
\renewcommand{\abstract}[1]{\begin{list}{}
			{\rightmargin\leftmargin
			\listparindent 1.5em
			\parsep 0pt plus 1pt}
			\small\item #1\end{list}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\dcup}{\stackrel{\cdot}{\cup}}		% disjoint union
\newcommand{\dl}[1]{\mbox{\rm I\hspace{-0.75mm}#1}}	% openface letter
\newcommand{\dc}[1]{\mbox{\rm {\raisebox{.4ex}{\makebox	% openface character
	[0pt][l]{\hspace{.2em}\scriptsize $\mid$}}}#1}}
\newcommand{\IT}{\mbox{\sf T\hspace{-5.5pt}T}}          % openface T (terms)
\newcommand{\plat}[1]{\raisebox{0pt}[0pt][0pt]{$#1$}}   % no vertical space
\newcommand{\Id}[1]{[\hspace{-1.4pt}[#1]\hspace{-1.2pt}]} % denotation
\newcommand{\In}[1]{\plat{			 	% notation
	\stackrel{\mbox{\tiny $/\hspace{-2.1pt}/$}}
	{\raisebox{-.3ex}[.3ex]{\tiny $\backslash
	\hspace{-2.1pt}\backslash$}}\!\!#1\!\!
	\stackrel{\mbox{\tiny $\backslash\hspace{-1.8pt}\backslash$}}
	{\raisebox{-.3ex}[.3ex]{\tiny $/\hspace{-1.8pt}/$}} }}
\newcommand{\rec}[1]{\plat{			 	% square brackets
	\stackrel{\mbox{\tiny $/$}}
	{\raisebox{-.3ex}[.3ex]{\tiny $\backslash$}}
	\!\!#1\!\!
	\stackrel{\mbox{\tiny $\backslash$}}
	{\raisebox{-.3ex}[.3ex]{\tiny $/$}} }}
\newcommand{\goto}[1]{\stackrel{#1}{\longrightarrow}}	% transition
\newcommand{\gonotto}[1]{\hspace{4pt}\not\hspace{-4pt}	% no transition
	\stackrel{#1\ }{\longrightarrow}}
\newcommand{\si}{\stackrel{\rightarrow}{\raisebox{0pt}[1pt][0pt]{$\scriptstyle \leftarrow$}}}
\newcommand{\bis}[1]{ \;				% bisimulation
	\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}
                  \,_{#1}\,}
\newcommand{\nobis}[1]{\mbox{$\,\not\hspace{-2.5pt}	% no bisimulation
	\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}
                  \,_{#1}\,$}}
\newcommand{\pf}{{\bf Proof:\ }}			% beginning of proof
\newcommand{\rest}{					% restriction operator
        \begin{picture}(2.16,3.2)
        \thinlines
        \put(1.12,-0.48){\line(0,1){3.52}}
	\put(0.8,1.6){\tiny $\backslash$}
        \end{picture} }

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%				Abbreviations			          %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\IN}{\dl{N}}			    % natural numbers
\newcommand{\IC}{\dc{C}}			    % configuration structures
\newcommand{\IE}{\dl{E}}			    % event structures
\newcommand{\IG}{\dc{G}}			    % graphs
\newcommand{\IP}{\dl{P}}			    % transition space
\newcommand{\IO}{\dc{O}}			    % observations
\newcommand{\pow}{{\cal P}}			    % powerset
\newcommand{\fC}{{\cal C}}			    % function into \IC
\newcommand{\fE}{{\cal E}}			    % function into \IE
\newcommand{\fG}{{\cal G}}			    % function into \IG
\newcommand{\fH}{{\cal H}}			    % hypothetical observations
\newcommand{\fO}{{\cal O}}			    % function into \IO
\newcommand{\eC}{{\rm C}}			    % conf. structure
\newcommand{\eD}{{\rm D}}			    % conf. structure
\newcommand{\eE}{{\rm E}}			    % event structure
\newcommand{\eF}{{\rm F}}			    % event structure
\newcommand{\eG}{{\rm G}}			    % process graph
\newcommand{\eH}{{\rm H}}			    % process graph
\newcommand{\eP}{{\rm P}}			    % process expression
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}
\bibliographystyle{plain}		% Actually the vG-style is used here

\title{The Meaning of Negative Premises\\
       in Transition System Specifications II}

\abstract{This paper reviews several methods to associate transition
relations to transition system specifications with negative premises
in Plotkin's structural operational style. Besides a formal comparison
on generality and relative consistency, the methods are also evaluated
on their taste in determining which specifications are meaningful and
which are not.}

\section{Transition system specifications}

In this paper $V$ and $A$ are two sets of {\em variables} and {\em
actions}. Many concepts that will appear are parameterized by the
choice of $V$ and $A$, but as in this paper this choice is fixed, a
corresponding index is suppressed.

\begin{definition}{signature} ({\em Signatures}).
A {\em function declaration} is a pair $(f,n)$ of a {\em function
symbol} $f \not\in V$ and an {\em arity} $n \in \IN$. A function
declaration $(c,0)$ is also called a {\em constant declaration}.
A {\em signature} is a set of function declarations. The set
$\IT(\Sigma)$ of {\em terms} over a signature $\Sigma$ is defined
recursively by:
\begin{itemize}
\item $V \subseteq \IT(\Sigma)$,
\item if $(f,n) \in \Sigma$ and $t_1,\ldots,t_n \in \IT(\Sigma)$ then
$f(t_1,\ldots,t_n) \in \IT(\Sigma)$.
\end{itemize}
A term $c()$ is often abbreviated as $c$.  $T(\Sigma)$ is the set of
{\em closed} terms over $\Sigma$, not containing any variables. A {\em
$\Sigma$-substitution} $\sigma$ is a partial function from $V$ to
$\IT(\Sigma)$. If $\sigma$ is a substitution and $S$ any syntactic
object, then $S[\sigma]$ denotes the object obtained from $S$ by
replacing, for $x$ in the domain of $\sigma$, every occurrence of $x$
in $S$ by $\sigma(x)$. In that case $S[\sigma]$ is called a {\em
substitution instance} of $S$.
\end{definition}

\begin{definition}{TSS} ({\em Transition system specifications}).
Let $\Sigma$ be a signature. A {\em positive $\Sigma$-literal} is an
expression $t \goto{a} t'$ and a {\em negative $\Sigma$-literal} an
expression $t \gonotto{a}$ or $t \gonotto{a} t'$ with $t,t'\in
\IT(\Sigma)$ and $a \in A$. For $t,t' \in \IT(\Sigma)$ the literals $t
\goto{a} t'$ and $t \gonotto{a}$, as well as $t \goto{a} t'$ and $t
\gonotto{a} t'$, are said to {\em deny} each other.
A {\em transition rule} over $\Sigma$ is an expression of the form
$\frac{H}{\alpha}$ with $H$ a set of $\Sigma$-literals (the {\em
premises} or {\em antecedents} of the the rule) and $\alpha$ a
$\Sigma$-literal (the {\em conclusion}). A rule $\frac{H}{\alpha}$
with $H=\emptyset$ is also written $\alpha$.  A literal or transition
rule is {\em closed} if it contains no variables. An {\em action rule}
is a transition rule with a positive conclusion. A {\em transition
system specification (TSS)} is a pair $(\Sigma,R)$ with $\Sigma$ a
signature and $R$ a set of action rules over $\Sigma$. A TSS is {\em
standard} if its rules have no antecedents of the form
$t\gonotto{a}t'$, and {\em positive} if all antecedents of its rules
are positive.
\end{definition}
The first systematic study of transition system specifications with
negative premises appears in {\sc Bloom, Istrail \& Meyer} \cite{BIM88}. 
The concept of a (positive) TSS presented above was introduced in {\sc
Groote \& Vaandrager} \cite{GrV92}; the negative premises $t
\gonotto{a}$ were added in {\sc Groote} \cite{Gr93}. The notion
generalises the {\em GSOS rule systems} of \cite{BIM88} and constitutes the
first formalization of {\sc Plotkin}'s {\em Structural Operational
Semantics (SOS)} \cite{Pl81} that is sufficiently general to cover
most, if not all, of its applications. The premises $t\gonotto{a}t'$
are added here, mainly for technical reasons.

The following definition tells when a transition is provable from a
TSS. It generalises the standard definition (see e.g.\ \cite{GrV92})
by (also) allowing the derivation of transition rules. The
derivation of a transition $t\goto{a}t'$ corresponds to the derivation
of the transition rule $\frac{H}{t\goto{a}t'}$ with $H=\emptyset$.
The case $H \neq \emptyset$ corresponds to the derivation of
$t\goto{a}t'$ under the assumptions $H$.

\begin{definition}{proof}({\em Proof\/}).
Let $P=(\Sigma,R)$ be a TSS. A {\em proof} of a transition
rule $\frac{H}{\alpha}$ from $P$ is a well-founded, upwardly
branching tree of which the nodes are labelled by $\Sigma$-literals,
such that:
\begin{itemize}\vspace{-1ex}
\item the root is labelled by $\alpha$, and\vspace{-1ex}
\item if $\beta$ is the label of a node $q$ and $K$ is the set of
labels of the nodes directly above $q$, then
\begin{enumerate}\vspace{-1ex}
\item either $K=\emptyset$ and $\beta \in H$,
\item or $\frac{K}{\beta}$ is a substitution instance of a rule from $R$.
\vspace{-1ex}\end{enumerate}
\end{itemize}
If a proof of $\frac{H}{\alpha}$ from $P$ exists, then
$\frac{H}{\alpha}$ is {\em provable} from $P$, notation $P \vdash
\frac{H}{\alpha}$.\\
A closed negative literal $\alpha$ is {\em refutable} if $P\vdash
\beta$ for a literal $\beta$ denying $\alpha$.
\end{definition}

\begin{definition}{transition}({\em Transition relation}).
Let $\Sigma$ be a signature.  A {\em transition relation} over
$\Sigma$ is a relation $T \subseteq T(\Sigma) \times A
\times T(\Sigma)$. Elements $(t,a,t')$ of a transition relation are
written as $t \goto{a} t'$. Thus a transition relation over $\Sigma$
can be regarded as a set of closed positive $\Sigma$-literals ({\em
transitions}).

A closed literal $\alpha$ {\em holds} in a transition relation $T$,
notation $T \models \alpha$, if $\alpha$ is positive and $\alpha \in
T$ or $\alpha = (t\gonotto{a}t')$ and $(t\goto{a}t')\not\in T$ or
$\alpha = (t\gonotto{a})$ and $(t\goto{a}t')\in T$ for no $t'\in
T(\Sigma)$. Write $T \models H$, for $H$ a set of closed literals, if
$T \models \alpha$ for all $\alpha \in H$.
\end{definition}
A positive TSS specifies a transition relation in a straightforward
way as the set of all provable transitions. But as pointed out in
{\sc Groote} \cite{Gr93}, it is much less trivial to associate a
transition relation to a TSS with negative premises. Several
solutions are proposed in \cite{Gr93} and {\sc Bol \& Groote}
\cite{BolG91}. Here I will present these solutions from a somewhat
different point of view, and also review a few others.
$$\begin{array}{@{}c@{}|cc|@{}}
\cline{2-3}
\makebox[0pt][r]{$P_1~~~\rule[-14pt]{0pt}{36pt}$}
&\displaystyle\frac{c\gonotto{a}}{c\goto{b}c}
&\displaystyle\frac{c\gonotto{b}}{c\goto{a}c}\\
\cline{2-3}
\end{array}$$
The TSS $P_1$\footnote{All my examples $P_i$ consider TSSs $(\Sigma,R)$ in
which $\Sigma$ consists of the single constant $c$ only.} can be
regarded as an example of a TSS that does not specify a well-defined
transition system.  So unless a systematic way can be found to
associate a meaning to TSSs like $P_1$, one has to accept that some
TSSs are meaningless. Hence there are two questions to answer:
\begin{equation}
\mbox{\em Which TSSs are meaningful, and which transition relations do
they specify?}\label{quest}
\end{equation}
In this paper I present 11 possible answers to these questions, each
consisting of a class of TSSs and a mapping from this class to
transition relations. Two such solutions are {\em consistent} if they
agree which transition relation to attach to a TSS in the intersection
of their domains. Solution $S'$ {\em extends} $S$ if the class of
meaningful TSSs according to $S'$ extends that of $S$ and the two are
consistent, i.e.\ seen as partial functions $S$ is included in $S'$.

\section{Model theoretic solutions}\label{model}

\begin{solution}{positive}({\em Positive}).
A first and rather conservative answer to (\ref{quest}) is to take the
class of positive TSSs as the meaningful ones, and associate with
each positive TSS the transition relation consisting of the
provable transitions.
\end{solution}
Before proposing more general solutions, I will first recall two
criteria from {\sc Bloom, Istrail \& Meyer} \cite{BIM88} and
{\sc Bol \& Groote} \cite{BolG91} that can be imposed on solutions.

\begin{definition}{agrees}({\em Supported model\/}).
A transition relation $T$ {\em agrees} with a TSS
$P$ if:
\begin{center}
$T \models t\goto{a}t' ~~\Leftrightarrow~~ \mbox{there is a closed
substitution instance } \frac{H}{t\goto{a}t'} \mbox{ of a rule of } P
\mbox{ with } T \models H.$
\end{center}
$T$ is a {\em model} of $P$ if ``$\Leftarrow$'' holds;
$T$ is {\em supported} by $P$ if ``$\Rightarrow$'' holds.
\end{definition}
The first and most indisputable criterion imposed on a transition
system $T$ specified by a TSS $P$ is that it is a model of $P$. This
is called being {\em sound} for $P$ in \cite{BIM88}.  This criterion
says that the rules of $P$, interpreted as implications in first-order
or conditional logic, should evaluate to true statements about $T$.
The second criterion, of being supported, says that $T$ does not
contain any transitions for which it has no plausible justification to
contain them. In \cite{BIM88} being supported is called {\em
witnessing}. Note that the universal transition relation on
$T(\Sigma)$ is a model of any TSS. It is however rarely the intended
one, and the criterion of being supported is a good tool to rule it
out. Next I check that \sol{positive} satisfies both criteria.

\begin{proposition}{least}
Let $P$ be a positive TSS and $T$ the set of transitions provable
from $P$. Then $T$ is a supported model of $P$. Moreover $T$ is the
least model of $P$.
\end{proposition}

\begin{proof}
That $T$ is a supported model of $P$ is an immediate consequence of
the definition of provability. Furthermore, let $T'$ be any model of
$P$, then by induction on the length of proofs it follows
that $T \subseteq T'$.
\end{proof}

Starting from \pr{least} there are at least three ways to generalise
\sol{positive} to TSSs with negative premises. One can generalise
either the concept of a proof, or the least model property, or
the least supported model property of positive TSSs. Starting with
the last two possibilities, observe that in general no least model
and no least supported model exists. A counterexample is given by
the TSS $P_1$ (given earlier), which has two minimal models,
$\{c\goto{a}c\}$ and $\{c\goto{b}c\}$, both of which are supported.

\begin{solution}{least}({\em Least}).
A TSS is meaningful iff it has a least model {\scriptsize (this being its
specified transition relation)}.
\end{solution}

\begin{solution}{least supported}({\em Least supported\/}).
A TSS is meaningful iff it has a least supported model.
\end{solution}
These two solutions turn out to have incomparable domains. The TSS
$P_2$ below has $\{c\goto{a}c\}$ as its least model, but has no
supported models.
On the other hand $P_3$ has two minimal models, namely
\plat{\{c\goto{b}c\}} and $\{c \goto{a}c\}$ of which only the latter one is
supported. This is its least supported model.
$$\begin{array}{@{}c@{}|c|@{}}
\cline{2-2}
\makebox[0pt][r]{$P_2~~~\rule[-14pt]{0pt}{36pt}$}
&\displaystyle\frac{c\gonotto{a}}{c\goto{a}c}\\
\cline{2-2}
\end{array}
\hspace{1in}
\begin{array}{@{}c@{}|c|@{}}
\cline{2-2}
\makebox[0pt][r]{$P_3~~~\rule[-14pt]{0pt}{36pt}$}
&\displaystyle\frac{c\gonotto{b}}{c\goto{a}c}\\
\cline{2-2}
\end{array}$$
Obviously \sol{positive} is extended by
both solutions above. However, Solutions \ref{sol-least} and
\ref{sol-least supported} turn out to be inconsistent with each other.
$P_4$ has both a least model and a least supported model, but
they are not the same.\vspace{-2ex}
$$\begin{array}{@{}c@{}|ccc|@{}}
\cline{2-4}
\makebox[0pt][r]{$P_4~~~\rule[-14pt]{0pt}{36pt}$}
&\displaystyle\frac{c\gonotto{a}}{c\goto{a}c}
&\displaystyle\frac{c\goto{b}c}{c\goto{a}c}
&\displaystyle\frac{c\goto{b}c}{c\goto{b}c}\\
\cline{2-4}
\end{array}
\hspace{1in}
\begin{array}{@{}c@{}|c|@{}}
\cline{2-2}
\makebox[0pt][r]{$P_5~~~\rule[-14pt]{0pt}{36pt}$}
&\displaystyle\frac{c\goto{a}c}{c\goto{a}c}\\
\cline{2-2}
\end{array}$$
\sol{least} is not very productive, because if fails to assign a
meaning to the perfectly reasonable TSS $P_3$. Moreover, it can be
criticized for yielding unsupported transition systems, as in the case
of $P_2$. However, in $P_4$ the least model $\{c\goto{a}c\}$ appears to be
a better choice than the least supported model \plat{\{c\goto{a}c, ~
c\goto{b}c\}}, as the `support' for transition \plat{c\goto{b}c} is not
overwhelming. Thus, to my taste, \sol{least supported} is somewhat
unnatural.

In {\sc Bloom, Istrail \& Meyer} \cite{BIM88} the following solution
is applied.

\begin{solution}{unique supported}({\em Unique supported\/}).
A TSS is meaningful iff it has a unique supported model.
\end{solution}
The positive TSS $P_5$ above has two supported models, $\emptyset$ and
$\{c\goto{a}c\}$, and hence shows that \sol{unique supported} does not
extend \sol{positive}.

Although for the kind of TSSs considered in \cite{BIM88} (the {\em
GSOS rule systems}) this solution coincides with all acceptable
solutions mentioned in this paper, in general it suffers from the same
drawback as \sol{least supported}.  The least supported model of $P_4$
is even the unique supported model of this TSS. My conclusion is that
the criterion of being supported is too weak to be of any use in this
context.

This conclusion was also reached by {\sc Fages} \cite{Fa91} in the
setting of logic programming, who proposes to strengthen this
criterion.  Being supported can be rephrased as saying that a
transition may only be present if there is a nonempty proof of its
presence, starting from transitions that are also present. However,
these premises in the proof may include the transition under
derivation, thereby allowing for loops, as in the case of $P_4$. Now
the idea behind a {\em well-supported model} is that the {\em absence}
of a transition may be assumed a priory, as long as this assumption is
consistent, but the {\em presence} of a transition needs to be proven
without assuming the presence of (other) transitions. Thus a
transition may only be present if it admits a valid proof,
starting from negative literals only.

\begin{definition}{stable}({\em Stable transition relation}).
A transition relation $T$ is {\em stable} for a TSS
$P$ if:
\begin{center}
$T \models t\goto{a}t' ~~\Leftrightarrow$ \begin{tabular}{l}there is a
closed transition rule $\frac{N}{t\goto{a}t'}$ without positive
antecedents\\ with $P \vdash \frac{N}{t\goto{a}t'}$ and $T \models N$.
\end{tabular}
\end{center}
$T$ is {\em well-supported} by $P$ if ``$\Rightarrow$'' holds.
\end{definition}

\begin{proposition}{stable model}
If $T$ is stable for $P$, then it is a model of $P$. Moreover, any
model of $P$ satisfies ``$\Leftarrow$''.  Hence a stable transition
relation is the same as a well-supported model.
\end{proposition}

\begin{proof}
Suppose there is a closed substitution instance $\frac{H}{t\goto{a}t'}$
of a rule of $P$ with $T \models H$. Assuming that $T$ is stable,
for any $t_i\goto{a_i}t_i' \in H$ there must be a closed transition
rule $\frac{N_i}{t_i\goto{a_i}t_i'}$ without positive antecedents
with $P \vdash \frac{N_i}{t_i\goto{a_i}t_i'}$ and $T \models N_i$.
Let $N$ be the union of all those $N_i$'s and the negative literals in
$H$. Then, by combination of proof-fragments, $\frac{N}{t\goto{a}t'}$
is a closed transition rule without positive antecedents with $P
\vdash \frac{N}{t\goto{a}t'}$ and $T \models N$. Hence $T \models t\goto{a}t'$.

The second statement follows by a trivial induction on the lenght of
proofs, and the third one is an immediate corollary.
\end{proof}

\begin{proposition}{well-supported}
If a transition relation is well-supported by $P$, then
it is supported by $P$.
\end{proposition}

\begin{proof}
Let $T$ be well-supported by $P$, and let $T \models t\goto{a}t'$.
Then there is a closed transition rule $\frac{N}{t\goto{a}t'}$
without positive antecedents with $P \vdash \frac{N}{t\goto{a}t'}$ and
$T \models N$. As the transition $t\goto{a}t'$ cannot be in $N$, there must be
a non-empty proof of $\frac{N}{t\goto{a}t'}$. Let
$\frac{K}{t\goto{a}t'}$ be the closed substitution instance of a rule
of $P$ applied in the last step of this proof. After omitting this
step from the proof, one is left with proofs for the literals in $K$.
It follows that $T \models K$, which had to be established.
\end{proof}
My concept of well-supportedness can easily be seen to coincide with
the one of {\sc Fages} \cite{Fa91}.  The (earlier) concept of
stability for TSSs stems from {\sc Gelfond \& Lifschitz} \cite{GL88}
in the context of logic programming. It has been adapted for TSSs by
{\sc Bol \& Groote} \cite{BolG91}.  In \cite{BolG91} stability was
defined in terms of an operator $Strip$ on TSSs without variables. If
$P$ is such a TSS and $T$ a transition relation, $Strip(P,T)$ is
obtained from $P$ by removing from $P$ all rules with negative
premises that do not hold in $T$, and removing from the remaining
rules the negative premises that do hold (Definition 4.3 in
\cite{BolG91}). This yields a positive TSS, whose associated transition
relation is denoted $\longrightarrow_{Strip(P,T)}$. Now $T$ is said to
be stable for $P$ if $T=\longrightarrow_{Strip(P,T)}$. This definition
is extended to TSSs $P$ with variables by identifying such a TSS with
the TSS of all closed substitution instances of rules in $P$.

\begin{proposition}{BolG91}
The concept of stability of \df{stable} coincides with that from
\cite{BolG91}.
\end{proposition}

\begin{proof}
Let $P'$ be a TSS and $P$ be the TSS consisting of all closed
substitution instances of rules in $P$. Note that $T$ is stable for
$P$ in the sense of \df{stable} iff it is for $P'$.

The construction of $Strip$ entails that $Strip(P,T) \vdash
t\goto{a}t'$ iff $P\vdash \frac{N}{t\goto{a}t'}$
for a set of closed negative literals $N$ with $T \models N$.
It follows immediately that both definitions are equivalent.
\end{proof}

The following two solutions are adaptations of Solutions
\ref{sol-least supported} and \ref{sol-unique supported}, were the
requirement of being supported has been replaced by that of being
well-supported. The second is taken from \cite{BolG91}.

\begin{solution}{stable}({\em Stable}).
A TSS is meaningful iff it has a least stable transition relation.
\end{solution}\addtocounter{solu}{-1}

\begin{solution}{unique stable}({\em Stable}).
A TSS is meaningful iff it has a unique stable transition relation.
\end{solution}
The particular numbering of these two solutions is justified by the following.

\begin{proposition}{stable}
Let $T_1$ be a model of a TSS $P$ and $T_2$ be well-supported by
$P$. If $T_1 \subseteq T_2$ then $T_1 = T_2$.
If follows (from the special case that $T_1$ and $T_2$ are both
stable) that a TSS has a least stable transition relation iff it
has a unique stable transition relation.
\end{proposition}

\begin{proof}
As $T_1 \subseteq T_2$ one has
$$T_1 \models t\goto{a}t' ~~\Rightarrow~~ T_2 \models t\goto{a}t'$$
from which it follows that
\begin{equation}\label{contrapositive}
T_2 \models t\gonotto{a}t' ~~\Rightarrow~~ T_1 \models t\gonotto{a}t'
~~~~~~~~~\mbox{and}~~~~~~~~~
T_2 \models t\gonotto{a} ~~\Rightarrow~~ T_1 \models t\gonotto{a}.
\end{equation}
Now suppose $T_2 \models t\goto{a}t'$. Then there is a
closed transition rule $\frac{N}{t\goto{a}t'}$ without positive
antecedents with $P \vdash \frac{N}{t\goto{a}t'}$ and $T_2 \models N$.
By (\ref{contrapositive}) we have $T_1 \models N$ and hence $T_1
\models t\goto{a}t'$.
\end{proof}
\sol{stable} improves Solutions \ref{sol-least supported} and
\ref{sol-unique supported} by rejecting the TSS $P_4$ as
meaningless. It also improves \sol{least} by rejecting the TSS
$P_2$ (whose least model was not supported). Surprisingly however,
\sol{stable} not only differs from the earlier solutions by being more
fastidious; it also provides meaning to perfectly acceptable TSSs that
were left meaningless by Solutions \ref{sol-least},
\ref{sol-least supported} and \ref{sol-unique supported}.

$$\begin{array}{@{}c@{}|cc|@{}}
\cline{2-3}
\makebox[0pt][r]{$P_6~~~\rule[-14pt]{0pt}{36pt}$}
&\displaystyle\frac{c\gonotto{a}}{c\goto{b}c}
&\displaystyle\frac{c\goto{a}c}{c\goto{a}c}\\
\cline{2-3}
\end{array}$$
An example is the TSS $P_6$. There is clearly no satisfying way
to obtain $c\goto{a}c$.  Hence $c\gonotto{a}$ and consequently
$c\goto{b}c$.  $\{c\goto{b}c\}$ is indeed the unique stable transition
relation of this TSS. However, $P_6$ has two minimal models, both of
which are supported, namely $\{c\goto{b}c\}$ and $\{c\goto{a}c\}$.

\begin{proposition}{consistent}
\sol{stable} ({\em stable}) is consistent with \sol{least} ({\em
least}) and \ref{sol-least supported} ({\em least supported\/}).
\end{proposition}

\begin{proof}
If a TSS has both a (least) well-supported model and a least
[supported] model, the two must be equal by \pr{stable}.
\end{proof}
As the set of transitions provable from a positive TSS is by definition
well-supported, \sol{stable} ({\em stable}) extends \sol{positive}
({\em positive}).
Hence the relations between the solutions seen so far are as indicated
in Figure \ref{semantic solutions} below. An arrow indicates
an extension. The relation $\smile$ indicates consistency and
incomparible domains (neither one extends the other).
There are no more extension and consistency relations than indicated
in the figure (taking into account that {\em positive$\smile$unique
supported} follows from the information displayed). All
counterexamples appear earlier in this section.
\begin{figure}[htb]
\begin{center}
\begin{picture}(80,30)(-40,0)
\put(0,30){\makebox[0pt][c]{positive (\ref{sol-positive})}}
\put(-8,29){\vector(-1,-1){25}}
\put(8,29){\vector(1,-1){26}}
\put(0,29){\vector(0,-1){11}}
\put(0,15){\makebox[0pt][c]{unique stable (\ref{sol-unique stable})}}
\put(-.2,14){\line(0,-1){11}}
\put(.2,14){\line(0,-1){11}}
\put(0,0){\makebox[0pt][c]{least stable (\ref{sol-stable})}}
\put(40,15){\makebox[0pt][c]{unique supported (\ref{sol-unique supported})}}
\put(40,14){\vector(0,-1){11}}
\put(40,00){\makebox[0pt][c]{least supported (\ref{sol-least supported})}}
\put(-40,0){\makebox[0pt][c]{least model (\ref{sol-least})}}
\put(-20,-2){\makebox[0pt][c]{\LARGE $\smile$}}
\put(18,13){\makebox[0pt][c]{\LARGE $\smile$}}
\put(18,-2){\makebox[0pt][c]{\LARGE $\smile$}}
\end{picture}
\end{center}
\caption[semantic solutions]{Relations between Solutions
\ref{sol-positive}--\ref{sol-stable}\label{semantic solutions}}
\end{figure}

It is interesting to see how the various solutions deal with {\em circular}
rules, such as \raisebox{2pt}[0pt][0pt]{$\frac{c\goto{a}c}{c\goto{a}c}$}, and
rules like \plat{\frac{c\gonotto{a}}{c\goto{a}c}}. The support-based
solutions (\ref{sol-least supported} and \ref{sol-unique supported})
may use a circular rule to obtain a transition that would be
unsupported otherwise (Example $P_4$). This is my main argument to
reject these solutions. In addition they may (or may not) reject TSSs
as meaningless because of the presence of such a rule (Example $P_6$).
On the other hand, Solutions \ref{sol-least} and \ref{sol-stable}
politely ignore these rules.  To my taste, there are two acceptable
attitudes towards circular rules: to ignore them completely (as done
by Solutions \ref{sol-positive}, \ref{sol-least} and
\ref{sol-stable}), or to reject any TSS with such a rule for being
ambiguous, unless there is independent evidence for a transition
$c\goto{a}c$. A strong argument in favor of the first approach is the
existence of useful rules of which only certain substitution instances
are circular (cf.\ \cite{BolG91}). A solution that caters to the
second option will be proposed in the next section.

\sol{least} can treat a rule \plat{\frac{c\gonotto{a}}{c\goto{a}c}} as
equivalent to $c\goto{a}c$ (namely if there are no other closed terms
than $c$, cf.\ $P_2$), which gives rise to unsupported transition relations.
Solutions \ref{sol-least supported}, \ref{sol-unique supported} and
\ref{sol-stable} do not go so far, but use such a rule to
choose between two otherwise equally attractive transition relations.
This is illustrated by the TSS $P_7$, which determines the transition
system $\{c\goto{a}c\}$ according to each of the solutions
\ref{sol-least}, \ref{sol-least supported}, \ref{sol-unique supported}
and \ref{sol-stable}.
$$\begin{array}{@{}c@{}|ccc|@{}}
\cline{2-4}
\makebox[0pt][r]{$P_7~~~\rule[-14pt]{0pt}{36pt}$}
&\displaystyle\frac{c\gonotto{a}}{c\goto{b}c}
&\displaystyle\frac{c\gonotto{b}}{c\goto{a}c}
&\displaystyle\frac{c\gonotto{a}}{c\goto{a}c}\\
\cline{2-4}
\end{array}$$
Note that ignoring rules like
\raisebox{2pt}[0pt][0pt]{$\frac{c\gonotto{a}}{c\goto{a}c}$}
is unacceptable, as this would yield unsound transition relations
(non-models). But it could be argued that any TSS with such a rule
should be rejected as meaningless, unless there is independent
evidence for a transition $c\goto{a}t$. This would rule out $P_7$.
Solutions that cater to this taste will be proposed in the next section.

\subsection*{3-Valued transition relations}

3-valued interpretations of logical programs are considered, among
others, in {\sc Van Gelder, Ross \& Schlipf} \cite{GRS88} and {\sc
Przymusinski} \cite{Prz90}. The same can be done for TSSs.  The
meaning of a TSS is then not given by a transition relation, i.e.\ a
partition of $T(\Sigma)\times A \times T(\Sigma)$ into the the
transitions that hold and those that don't, but a partition of
$T(\Sigma)\times A \times T(\Sigma)$ into three sets: {\em true}, {\em
false} and {\em unknown}. Such a 3-valued interpretation is in logic
programming often given as a pair $\rec{T;F}$ of disjoint transition
relations, representing the transitions that certainly hold, and those
that certainly don't. Here I find it easier to represent the same
information as a pair $T=\rec{CT,PT}$, called a {\em 3-valued
transition relation}, with $CT$ the set of transitions that {\em
certainly} hold, and $PT \supseteq CT$ the ones that {\em possibly}
hold. Thus $PT$ combines the values true and unknown, and is the
complement of $F$.  On 3-valued transition relations the {\em
information ordering} $\subseteq$ is defined by $\rec{CT,PT} \subseteq
\rec{CT',PT'}$ iff $CT \subseteq CT'$ and $PT \supseteq PT'$, i.e.\ in
$\rec{CT',PT'}$ the thruth or falsety of more transitions is known.
In the $\rec{T;F}$-representation $PT \supseteq PT'$ translates to $F
\subseteq F'$. A 3-valued transition relation $\rec{CT,PT}$ is said to
be {\em 2-valued} if $CT=PT$.
Note that for a negative literal $\alpha$, $CT \models
\alpha$ means that $\alpha$ {\em possibly} holds (no denying literal
certainly holds), whereas $PT \models \alpha$ means that $\alpha$ {\em
certainly} holds (no denying literal possibly holds). This explains
the following generalisation, based on the work of {\sc Przymusinski}
\cite{Prz90}, of the concept of a stable transition relation (or
well-supported model) to 3-valued interpretations.

\begin{definition}{3-stable}({\em 3-Valued stabilily}).
A 3-valued transition relation $\rec{CT,PT}$ is {\em stable} for a TSS $P$ if:
\begin{center}
$CT \models t\goto{a}t' ~~\Leftrightarrow$ \begin{tabular}{l}there is a
closed transition rule $\frac{N}{t\goto{a}t'}$ without positive
antecedents\\ with $P \vdash \frac{N}{t\goto{a}t'}$ and $PT \models N$,
\end{tabular}
\end{center}
\begin{center}
and $~~PT \models t\goto{a}t' ~~\Leftrightarrow$ \begin{tabular}{l}there is a
closed transition rule $\frac{N}{t\goto{a}t'}$ without positive
antecedents\\ with $P \vdash \frac{N}{t\goto{a}t'}$ and $CT \models N$.
\end{tabular}
\end{center}
\end{definition}
The definition in \cite{Prz90} is a bit more complicated, but can be
shown to amount to the same concept. Note that a stable transition
relation as in \df{stable} can be regarded as a stable 3-valued
transition relation $T=\rec{CT,PT}$ with $CT=PT$. 
{\sc Przymusinski} \cite{Prz90} showed that every logic program admits
a 3-valued stable transition relation, and the same can be said for
TSSs. There is even a least one w.r.t.\ the information
ordering. He also showed that the least 3-valued stable model
coincides with the {\em well-founded semantics} of an arbitrary TSS
(logical program) proposed earlier by {\sc Van Gelder, Ross \&
Schlipf} \cite{GRS88}. See Section \ref{reduction} for a variant
of the approach of \cite{GRS88}. The TSS $P_1$ has three 3-valued stable
transition relations, namely $\rec{\{c \goto{a} c\},\{c \goto{a} c\}}$,
$\rec{\{c \goto{b} c\}, \{c \goto{b} c\}}$ and $\rec{\emptyset, \{c \goto{a}
c, ~ c \goto{b} c\}}$. The first two are 2-valued. For reasons of
symmetry the latter, which is also the least, is most suited as the
intended meaning of this TSS\@. This is its well-founded semantics.
Hence the following solution.

\begin{trivlist}\item[]{\bf 3-Valued Solution I} ({\em Well-founded\/})
Any TSS is meaningful. Its meaning is its information-least 3-valued
stable transition relation.
\end{trivlist}
The existence of this relation will be demonstrated in the next section.
The example $P_1$ shows that there need not be a least 3-valued stable
transition relation w.r.t.\ the {\em truth ordering}, defined by
requiring $CT \subseteq CT'$ and $PT \subseteq PT'$.
3-Valued Solution I is not numbered with the others, as it does not
provides (2-valued) transition relations. However, a 2-valued
relation can be obtained by restricting attention to those
TSSs for which the least 3-valued stable transition relation
$\rec{CT,PT}$ satisfies $T=PT$. Alternatively, just the component $CT$
(or just $PT$) of the least 3-valued stable transition relation $\rec{CT,PT}$
could be taken to be the meaning of a TSS. These possibilities will be
explored in the next section. Finally I mention another 3-valued
answer to (\ref{quest}), based on a generalisation of the notion of a
supported model which is left as an exercise to the reader.

\begin{trivlist}\item[]{\bf 3-Valued Solution II} 
Any TSS is meaningful. Its meaning is its information-least 3-valued
supported model.
\end{trivlist}

\section{Proof theoretic solutions}

In this section I will propose solutions based on a generalization of
the concept of a proof. Note that in a proof two kinds of steps are
allowed, numbered 1 and 2 in \df{proof}. Step 1 just allows hypotheses
to enter, in case one wants to prove a transition rule. This step
can not be used when merely proving transitions. The essence of
the notion is step 2. This step reflects the postulate that
the desired transition relation must be a model of the given TSS\@. As a
consequence those and only those transitions are provable that appear
in any model. When generalising the notion of a proof to derive
negative literals it makes sense to import more postulates about the
desired transition relation. Note that a transition relation $T$ is
supported iff
\begin{center}
$T \not\models t\goto{a}t' ~~\Leftarrow~~ \mbox{for each closed
substitution instance } \frac{H}{t\goto{a}t'} \mbox{ of a rule of } P
\mbox{ one has } T \not\models H.$
\end{center}
and well-supported iff
\begin{center}
$T \not\models t\goto{a}t' ~~\Leftarrow~~$for each
set of negative closed literals $N$ with $P \vdash
\frac{N}{t\goto{a}t'}$, one has $T \not\models N$.
\end{center}
Therefore I propose the following two concepts of provability.

\begin{definition}{supported proof}({\em Supported proof\/}).
A {\em supported proof} of a closed literal $\alpha$ from a TSS
$P$ is like a closed (positive) proof (see \df{proof}), but
admitting steps of the form
\begin{itemize}\vspace{-1ex}
\item [3.] $\beta$ is negative and for each closed substitution
instance of a rule of $P$ whose conclusion denies $\beta$, a literal
in $K$ denies one of its antecedents.\vspace{-1ex}
\end{itemize}
$\alpha$ is {\em $s$-provable}, notation $P\vdash_s {\alpha}$, if a
supported  proof of ${\alpha}$ from $P$ exists.\\
A literal is {\em $s$-refutable} if a denying literal is $s$-provable.
\end{definition}

\begin{definition}{wsp}({\em Well-supported proof\/}).\label{df-refutable}
A {\em well-supported proof} of a closed literal $\alpha$ from a TSS
$P$ is like a closed (positive) proof (see \df{proof}), but admitting
steps of the form
\begin{itemize}\vspace{-1ex}
\item [3.] $\beta$ is negative and for every set $N$ of negative
closed literals such that $P \vdash \frac{N}{\gamma}$ for $\gamma$ a closed
literal denying $\beta$, a literal in $K$ denies one in $N$.\vspace{-1ex}
\end{itemize}
$\alpha$ is {\em $ws$-provable}, notation $P\vdash_{ws} \alpha$, if a
well-supported  proof of $\alpha$ from $P$ exists.\\
A literal is {\em $ws$-refutable} if a denying literal is $ws$-provable.
\end{definition}
Note that these proof-steps establish the validity of $\beta$ when $K$
is the set of literals established earlier. In case $K$ and $N$ are
sets of closed literals and a literal in $K$ denies one in $N$, one
has $T\not\models N$ for any transition relation $T$ with $T \models
K$. Thus step 3 from \df{wsp} allows to infer $t\gonotto{a}t'$ whenever
it is manifestly impossible to infer $t\goto{a}t'$, or $t\gonotto{a}$ whenever
it is manifestly impossible to infer $t\goto{a}t'$ for some term $t'$.
This practice is sometimes referred to as {\em negation as failure}
\cite{Cl78}. \df{supported proof} allows such an inference only if the
impossibility to derive $t\goto{a}t'$ can be detected by examining all
possible proofs that consist of one step only. This corresponds with
the notion of {\em negation as finite failure} of {\sc Clark} \cite{Cl78}.
The extension of these notions (especially $\vdash_{ws}$) from closed
to open literals $\alpha$, or to transition rules $\frac{H}{\alpha}$,
is somewhat problematic, and not needed in this paper.
The following may shed more light on $\vdash_s$ and $\vdash_{ws}$.

\begin{proposition}{refutable}
Let $P$ be a TSS\@. Then $P \vdash_s t\gonotto{a}[t']$ iff every
closed substitution instance \plat{\frac{H}{t\goto{a}t'}}
of\linebreak[2] a rule of $P$ has an $s$-refutable antecedent.
Moreover $P \vdash_{ws} t\!\gonotto{a}\![t']$ iff every set $N$ of closed
negative literals with $P \vdash \frac{N}{t\goto{a}t'}$ contains an
$ws$-refutable literal.\\[1ex]
\pf Fairly trivial.\hfill $\Box$
\end{proposition}

\begin{proposition}{ws-s} For $P$ a TSS and $\alpha$ a closed literal
one has $~~P\vdash {\alpha} ~~\Rightarrow~~ P\vdash_s {\alpha}
~~\Rightarrow~~ P\vdash_{ws} {\alpha}$.
\end{proposition}

\begin{proof}
The first statement is trivial. The second will be established with
induction on the structure of a $\vdash_s$-proof of ${\alpha}$.  Let
$\frac{K}{\alpha}$ be the last step in such a proof.  As $P\vdash_{s}
K$ by means of strict subproofs, it follows by induction that
$P\vdash_{ws} K$. Here I write $P \vdash_x K$ for $K$ a set of
literals if $P \vdash_x \beta$ for all $\beta \in K$.  If $\alpha$ is
positive, $P\vdash_{ws} {\alpha}$ follows immediately from the
definition of provability. Thus suppose $\alpha$ is negative. Let
$\{\alpha_i\}_{i\in I}$ be the set of negative literals in $K$, and
let \plat{\frac{K_i}{\alpha_i}} for $i\in I$ be the collection of last
proof-steps in $\vdash_{ws}$-proofs of the $\alpha_i$. Let $L=
\bigcup_{i\in I} K_i \cup (K-\{\alpha_i\}_{i\in I})$. Then clearly
$P\vdash_{ws} L$, so it suffices to show that for every set $N$ of negative
closed literals such that $P \vdash \frac{N}{\gamma}$ for $\gamma$ a
literal denying $\alpha$, a literal in $L$ denies one in $N$.

Consider a $\vdash$-proof $p$ of $\frac{N}{\gamma}$ with $N$ a set of
negative literals and $\gamma$ denies $\alpha$. By the definition of
$\vdash_{s}$, $p$ contains a literal $\delta$ that denies a literal
$\beta$ in $K$. This literal is the label of a node right above the
root.  In case $\delta$ occurs in $N$, $\beta$ is positive and
therefore occurs in $L$. In case $\delta \not\in N$, $\beta$ must be
negative and hence be $\alpha_i$ for certain $i \in I$. Because
\plat{\frac{K_i}{\alpha_i}} is a valid step in a $\vdash_{ws}$-proof
and $P \vdash \frac{N}{\delta}$ with $\delta$ denying $\alpha_i$, a
literal in $N$ must deny one in $K_i \subseteq L$.
\end{proof}

\begin{proposition}{finite failure}
Let a {\em quasi-proof} be defined as in \df{proof}, but without the
requirement of well-foundedness.
If in a TSS $P$ any quasi-proof is well-founded,
then $P \vdash_s \alpha \Leftrightarrow P \vdash_{ws} \alpha$.
\end{proposition}

\begin{proof}
Suppose $P \vdash_{ws} \alpha$. Let $\frac{K}{\alpha}$ be the last
step in a $\vdash_{ws}$-proof of $\alpha$. Applying induction on such
proofs, I may assume $P \vdash_s K$. In case $\alpha$ is positive the
desired result $P\vdash_s \alpha$ follows immediately, so suppose it
is not.  Let $\beta$ be a literal that denies $\alpha$ and let
\plat{\frac{H}{\beta}} be a closed substitution instance of a rule of $P$.
This instance constitutes a (positive) one-step proof $p$ of
\plat{\frac{H}{\beta}} from $P$.  I have to show that $H$ contains an
$s$-refutable literal.  Suppose by contradiction that is does not.
Then, by \pr{refutable}, for every positive literal $\gamma \in H$
there must a closed substitution instance
\plat{\frac{H_\gamma}{\gamma}} of a rule of $P$, without $s$-refutable
antecedents. Adding these rules to $p$ yields a larger proof $p'$ of a
rule \plat{\frac{H'}{\beta}} with $H'=\bigcup_{\{\gamma\in H \mid
\gamma ~\rm positive\}} H_\gamma \cup \{\gamma \in H \mid \gamma ~{\rm
negative}\}$. Iterating this procedure by applying the same reasoning
to $H'$ etc.\ yields a quasi-proof of a statement $\frac{N}{\beta}$
with $N$ a set of $s$-irrefutable closed negative literals. By
assumption this quasi-proof must be a proof. By the $ws$-provability
of $\alpha$ it follows that $N$ must contain a literal that is denied
by a literal from $K$, and hence $s$-refutable.  This yields a
contradiction.
\end{proof}

\begin{definition}{consistency}
For a 3-valued $T=\rec{CT,PT}$ define $T \models
\alpha$ as $\left\{\raisebox{0pt}[0pt]{\begin{tabular}{@{}l@{}}
$CT \models \alpha$ if $\alpha$ is positive\\
$PT \models \alpha$ if $\alpha$ is negative\end{tabular}}\right.$.\\
For $P$ a TSS and $\alpha$ a closed literal, write $P\models_s \alpha$
[resp.\ $P\models_{3s} \alpha$] if $T\models \alpha$ for any
[3-valued] supported model $T$ of $P$ and
$P\models_{ws} \alpha$ [resp.\ $P\models_{3ws} \alpha$] if $T\models
\alpha$ for any [3-valued] well-supported model $T$ of $P$.  A notion
$\vdash_x$ is called 
\begin{itemize}
\item {\em consistent} if there is no TSS deriving two
literals that deny each other.
\item {\em sound} w.r.t.\ $\models_x$ if for any TSS $P$ and closed literal
$\alpha$, $P\vdash_x \alpha \Rightarrow P\models_x \alpha$.
\item {\em complete} w.r.t.\ $\models_x$ if for any TSS $P$ and closed literal
$\alpha$, $P\vdash_x \alpha \Leftarrow P\models_x \alpha$.
\end{itemize}
\end{definition}

\begin{proposition}{consistency}
$\vdash_{ws}$ is consistent.
\end{proposition}

\begin{proof}
Let's say that two proofs $p$ and $q$ deny each other if their roots
are labelled with literals that deny each other. By induction on their
structure I establish that no two proofs from the same TSS $P$ deny
each other. So let $p$ and $q$ be two $\vdash_{ws}$-proofs from $P$
and assume that no two proper subproofs deny each other. By
contradiction suppose the roots of $p$ and $q$ are labelled with $t
\goto{a} t'$ and $t \gonotto{a}$ (or $t \gonotto{a}t'$) respectively.
Note that the bottom part of $p$ is a positive proof of a rule
$\frac{N}{t\goto{a}t'}$, where $N$ contains only negative literals.
Let $K$ be the set of literals labelling nodes directly above the root
of $q$. Then from the last step of $q$ it follows that $N$ (and thus
$p$) contains a negative literal that denies one in $K$, thus yielding
proper subproofs of $p$ and $q$ that deny each other.
\end{proof}
As $P\vdash \alpha ~\Rightarrow~ P\vdash_s \alpha ~\Rightarrow~
P\vdash_{ws} \alpha$, if follows that also $\vdash_s$ and $\vdash$ are
consistent.

\begin{proposition}{soundness}
$\vdash_{ws}$ is sound w.r.t.\ $\models_{ws}$ and $\models_{3ws}$.
Likewise $\vdash_{s}$ is sound w.r.t.\ $\models_{s}$ and $\models_{3s}$.
\end{proposition}
\pf
Let $P$ be a TSS and $T$ a [3-valued] well-supported model of $P$. With a
straightforward induction on the structure of proofs if follows that
$P\vdash_{ws} \alpha \Rightarrow T\models \alpha$.
The other part goes likewise.

\begin{lemma}{standard}
If $P$ is a TSS and $t\gonotto{a}$ a closed
literal, then $P \vdash_x t\gonotto{a}$ iff $P \vdash_x t\gonotto{a}
t'$ for any term $t' \in T(\Sigma)$.
\end{lemma}

\begin{proof}
This follows immediately from the observation that a closed literal $\gamma$
denies $t\gonotto{a}$ iff it denies $t \gonotto{a} t'$ for some $t'
\in T(\Sigma)$.
\end{proof}
The following theorem implies that any TSS has a least 3-valued
[well-]supported model w.r.t.\ the information ordering. This
justifies 3-valued Solutions I and II mentioned earlier.

\begin{theorem}{3-valued}
Let $P$ be TSS with $CT$ the set of $[w]s$-provable transitions and $PT$ the
set of $[w]s$-irrefutable transitions (the ones for which no denying
literal is $[w]s$-provable). Then $\rec{CT,PT}$ is a 3-valued
[well-]supported model of $P$. It is even the least one w.r.t.\ the
information ordering.
\end{theorem}

\begin{proof}
Note that for $\alpha$ positive $P \vdash_{[w]s} \alpha
\Leftrightarrow CT \models \alpha$, and for $\alpha$ negative, using
\lem{standard}, $P \vdash_{[w]s} \alpha \Leftrightarrow PT \models
\alpha$. Using this, it is straightforward to check that $CT$ and $PT$
satisfy the required equations. It follows from the soundness of
$\vdash_{[w]s}$ w.r.t.\ $\models_{3[w]s}$ (\pr{soundness}) that
$\rec{CT,PT}$ is included in any other 3-valued [well-]supported model
of $P$.
\end{proof}

\begin{corollary}{completeness}
$\vdash_{ws}$ is complete w.r.t.\ $\models_{3ws}$.
Likewise $\vdash_{s}$ is complete w.r.t.\ $\models_{3s}$.
\end{corollary}

\begin{proof}
If $P\models_{3[w]s} \alpha$ then by definition $\alpha$ certainly
holds in all [well]-supported models $\rec{CT,PT}$ (if $\alpha$ is
positive then $\alpha \in CT$ and if $\alpha$ is $t\gonotto{a}t'$ then
$t\goto{a}t' \not\in PT$).  Thus $\alpha$ certainly holds in the
least such model w.r.t.\ the information ordering, which is the one of
\th{3-valued}.  This implies $P \vdash_{[w]s} \alpha$.
\end{proof}
However, $\vdash_s$ and $\vdash_{ws}$ are not complete w.r.t.\
$\models_{[w]s}$. A trivial counterexample concerns TSSs like $P_2$
that have no [well-]supported models. $P_2 \models_{[w]s} \alpha$ for
any $\alpha$, which by \pr{consistency} is not the case for
$\vdash_{[w]s}$.  A more interesting counterexample concerns the TSS
$P_7$, which has only one [well-]supported model, namely \plat{\{c
\goto{a} c\}}.  In spite of this, \plat{P_7 \not\vdash_{[w]s}
c\goto{a}c} and \plat{P_7 \not\vdash_{[w]s} c\gonotto{b}}.

As argued in the previous section, there is a point in excluding $P_7$
from the meaningful TSSs, since there is insufficient evidence for the
transition $c \goto{a} c$. Here the incompleteness of $\vdash_{[w]s}$
w.r.t.\ $\models_{[w]s}$ comes as a blessing rather than a shortcoming.

\subsection{Solutions based on completeness}

I will now introduce the concept of a {\em complete} TSS: one in which
any transition is either provable or refutable.  Just as in the theory
of logic there is a distinction between the completeness of a logic
(e.g.\ first-order) and the completeness of a particular theory (e.g.\
arithmetic), here the completeness of a TSS is something different
from the completeness of a proof-method $\vdash_x$. Let $x$ be $s$ or $ws$.

\begin{definition}{complete}({\em Completeness of a TSS\/}).
A TSS $P$ is {\em $x$-complete} if for any transition $t\goto{a}t'$
either $P\vdash_{x} t\goto{a}t'$ or $P\vdash_{x} t\gonotto{a}t'$.
By `complete' I will mean `${ws}$-complete'.
\end{definition}
Note that a TSS is $[w]s$-complete iff its least (and only) 3-valued
[well-]supported model is 2-valued.

\begin{solution}{scomplete}({\em Complete with support}).
A TSS is meaningful iff it is ${s}$-complete. The associated
transition relation consists of the ${s}$-provable transitions.
\end{solution}

\begin{solution}{complete}({\em Complete}).
A TSS is meaningful iff it is (${ws}$-)complete. The associated
transition relation consists of the ${ws}$-provable transitions.
\end{solution}
In {\sc Bol \& Groote} \cite{BolG91} a method called {\em reduction}
for associating a transition relation with a TSS was proposed,
inspired by the {\em well-founded models} of {\sc Van Gelder, Ross \&
Schlipf} \cite{GRS88} in logic programming. In Section~\ref{reduction}
I show that this solution coincides with \sol{complete}.
\sol{complete} can therefore be regarded as a proof theoretical
characterization of the ideas from \cite{GRS88,BolG91}.
\sol{scomplete} may be new.

The TSS $P_6$ is complete, but not complete with support.
$P_3$ is even complete with support.
The following proposition says that a standard TSS (i.e.\ without
premises $t \gonotto{a}t'$) is complete if every closed
negative standard literal can be proved or refuted.

\begin{proposition}{complete}
A standard TSS $P$ is complete iff for any closed literal $t\gonotto{a}$
either $P\vdash_{ws} t\goto{a}t'$ for some closed term $t'$ or
$P\vdash_{ws} t\gonotto{a}$.
\end{proposition}

\begin{proof}
``only if'': Immediately by \lem{standard}.

``if'': Suppose $P\not\vdash_{ws}t\goto{a}t'$. In that case any set
$N=\{t_i \gonotto{a_i} \mid i\in I\}$ such that $P\vdash
\frac{N}{t\goto{a}t'}$ must contain a literal $t_{N} \gonotto{a_{N}}$
with $P\not\vdash_{ws} t_{N}\gonotto{a_{N}}$. By assumption, for
such a literal there is a $t_{N}'$ with
$P\vdash_{ws}t_{N}\goto{a_{N}}t_{N}'$.
It follows from \df{wsp}, taking $K$ to be the set of all transitions
$t_{N}\goto{a_{N}}t_{N}'$ (one for each possible choice of $N$),
that $P\vdash_{ws} t\gonotto{a}t'$.
\end{proof}
As literals $t\gonotto{a}t'$ do not appear in the antecedents of rules
in a standard TSS, their occurrence in a well-supported proof-tree
can be limited to the root. Thus \pr{complete} says that the concept
of a complete TSS can be introduced without considering such literals
at all.  The reason that these were introduced nevertheless, is that
\pr{complete} does not apply to completeness with support.  A
counterexample is given by the TSS Q.
$$\begin{array}{@{}c@{}|cc|@{}}
\cline{2-3}
\makebox[0pt][r]{$Q~~~\rule[-14pt]{0pt}{36pt}$}
&\displaystyle t\goto{a}t_1
&\displaystyle\frac{t\goto{a}t_2}{t\goto{a}t_2}\\
\cline{2-3}
\end{array}
\hspace{1in}
\begin{array}{@{}c@{}|cc|@{}}
\cline{2-3}
\makebox[0pt][r]{$R~~~\rule[-14pt]{0pt}{36pt}$}
&\displaystyle t\goto{a}t_1
&\displaystyle\frac{t\goto{a}t_2}{t\goto{b}t_2}\\
\cline{2-3}
\end{array}$$
$Q \not\vdash_s t\goto{a}t_2$ and $Q \not\vdash_s t\gonotto{a}t_2$, thus
this TSS is incomplete with support. However, for any closed literal
$u\gonotto{a}$, either $Q\vdash_{s} u\goto{a}u'$ for some term $u'$
or $Q\vdash_{s} u\gonotto{a}$. Moreover, even for the derivation of
standard literals, nonstandard literals may be essential in supported proofs.
The validity of \plat{R \vdash_s t\gonotto{b}} for instance, can only be
established by a proof tree containing $t\gonotto{a}t_2$.

\begin{proposition}{model}
The set of ${[w]s}$-provable transitions of a
${[w]s}$-complete TSS $P$ is a model of $P$.
\end{proposition}

\begin{proof}
Let $P$ be an $x$-complete TSS and $T$ the set of
$x$-provable transitions.  Suppose $\frac{H}{t\goto{a}t'}$ is a
closed substitution instance of a rule in $P$, and $T \models H$.  By
\df{transition} (of $T\models H$) $P\vdash_x \beta$ for each positive
antecedent $\beta$ in $H$, and $P\vdash_x \gamma$ for no transition
$\gamma$ denying a negative antecedent in $H$. Thus, by completeness
and \lem{standard}, $P\vdash_x \beta$ for any $\beta$ in $H$. Hence
$P\vdash_x t\goto{a}t'$.
\end{proof}

\begin{proposition}{supported}
The set of ${[w]s}$-provable transitions of any TSS is well-supported.
\end{proposition}

\begin{proof}
Let $P$ be a TSS and $T$ the set of $x$-provable transitions.
Suppose $T \models t\goto{a} t'$, i.e.\ $P \vdash_x t\goto{a}t'$ with
$t$ and $t'$ closed terms.  Take a [well-]supported proof of
this transition from $P$, and delete all branches above a node
labelled with a negative literal. This yields a positive proof of a
rule $\frac{N}{t\goto{a}t'}$ with $N$ a set of closed negative
literals. For any literal $\delta$ in $N$ one has
\plat{P \vdash_x \delta}. By the consistency of $\vdash_x$
\plat{P \vdash_x \beta} for no closed literal $\beta$ deying $\delta$.
This implies \plat{T \models \delta}.
\end{proof}

\begin{proposition}{complete-unique}
\sol{scomplete} [\ref{sol-complete}] is strictly extended by
\sol{unique supported} [\ref{sol-unique stable}].
\end{proposition}

\begin{proof}
Suppose $P$ is ${[w]s}$-complete. By Propositions \ref{pr-model}
and \ref{pr-supported} the ${[w]s}$-provable transitions
constitute a [well-]supported model of $P$, and by \pr{soundness}
this is the only such model. Strictness follows from the TSS $P_7$,
which has an unique [well-]supported model, but is left
meaningless by Solutions \ref{sol-scomplete} and \ref{sol-complete}.
\end{proof}

\subsection{Advantages of the proof theoretic solutions}

Now I will turn to the advantages of the proof theoretic solutions
over the model theoretic ones. At the end of Section \ref{model} I
discussed the r\^ole of rules like $\frac{c\gonotto{a}}{c\goto{a}c}$
and $\frac{c\goto{a}c}{c\goto{a}c}$. My suggestion was that any
TSS containing the former rule should be rejected as meaningless,
unless there is independent evidence for a transition $c\goto{a}t$.
As shown by counterexample $P_7$ all model theoretic solutions fail
this test. The following proposition shows that the proof theoretic
solutions behave better in this respect.

\begin{proposition}{p2}
Let $P,P'$ be TSSs that only differ in a rule
\plat{\frac{c\gonotto{a}}{c\goto{a}c}} that is in $P$ but not in $P'$.
Then $P$ is ${[w]s}$-complete only if $P'$ is
${[w]s}$-complete and proves the same literals as $P$,
including $c\goto{a}t$ for some term $t$.
\end{proposition}

\begin{proof}
Suppose $P$ is complete. It cannot be that $P\vdash_{[w]s}c\gonotto{a}$,
since in that case one could derive $P\vdash_{[w]s} c\goto{a}c$, contradicting
\pr{consistency} (consistency). Thus the label $c\gonotto{a}$ does not
appear in any proof of a literal from $P$. It follows that any literal
provable from $P$ is already provable from $P'$. By \lem{standard},
since $P\not\vdash_{[w]s} c\gonotto{a}$, $P\vdash_{[w]s} c\goto{a}t$ for
some term $t$.
\end{proof}\vspace{-1ex}
I also recommended two acceptable attitudes towards rule like
$\frac{c\goto{a}c}{c\goto{a}c}$. Below I show that \sol{complete}
ignores such rules completely (which is one option), whereas
\sol{scomplete} rejects a TSS with such a rule, unless there is
independent evidence for a transition $c \goto{a} c$ (the other option).

\begin{proposition}{p6ss}
Let $P,P'$ be TSSs that only differ in a rule 
$\frac{c\goto{a}c}{c\goto{a}c}$ that is in $P$ but not in $P'$.
Then $P$ is ${ws}$-complete iff $P'$ is ${ws}$-complete.
If $P$ is ${ws}$-complete it proves the same literals as $P'$.
\end{proposition}

\begin{proof}
Any application of \plat{\frac{c\goto{a}c}{c\goto{a}c}}
can be eliminated from a positive or well-supported proof.
\end{proof}

\begin{proposition}{p6s}
Let $P,P'$ be TSSs that only differ in a rule 
$\frac{c\goto{a}c}{c\goto{a}c}$ that is in $P$ but not in $P'$.
Then $P$ is ${s}$-complete only if $P'$ is ${s}$-complete and
proves the same literals as $P$, including $c\goto{a}c$.\vspace{-1ex}
\end{proposition}

\begin{proof}
Suppose $P$ is complete. It is easy to eliminate applications of the
rule $\frac{c\goto{a}c}{c\goto{a}c}$ from any supported proof, so any literal
provable from $P$ is also provable from $P'$. Hence $P'$ is complete.
Due to the rule $\frac{c\goto{a}c}{c\goto{a}c}$ it is impossible to
prove $c\gonotto{a}c$ from $P$. Thus $P\vdash_{s} c\goto{a}c$.
\end{proof}

\subsection{Solutions based on soundness}

The remainder of this section is devoted to generalizations of the
proof theoretic solutions. The first idea is to define the transition
system associated to a TSS $P$ just as in Solutions \ref{sol-scomplete}
and \ref{sol-complete}, that is as the set of $[w]s$-provable
transitions, but without requiring that $P$ is ${[w]s}$-complete.
This amounts to taking as the meaning of $P$ the component $CT$ of
its least [well-]supported model $\rec{CT,PT}$.
In general this may yield unsound transition relations (non-models),
which is not acceptable. This happens in the case of $P_1$, $P_2$,
$P_4$ and $P_7$. Thus the following restriction is needed.

\begin{solution}{sound}({\em Sound with support}).
A TSS is meaningful if the set of $s$-provable transitions
(this being the associated transition relation) constitutes a model.
\end{solution}

\begin{trivlist}
\item[]{\bf \sol{sound}b}
A TSS is meaningful if the set of ${ws}$-provable transitions
constitutes a model.
\end{trivlist}
Note that by \pr{supported} the transition relation determined by such
a TSS is even stable.

\begin{proposition}{sound=complete}
\sol{sound}b coincides with \sol{complete}.
\end{proposition}

\begin{proof}
It follows immediatelty from \pr{model} that a complete TSS is also
meaningful in the sense of \sol{sound}b. Now let $P$ be a TSS that is
meaningful in the sense of \sol{sound}b and $T$ the set 
of ${ws}$-provable transitions.  Suppose $P \not\vdash_{ws}
t\goto{a}t'$ for certain $t,t'\in T(\Sigma)$. Then $T \not\models
t\!\goto{a}\!t'.$  By the soundness of $T$ every set $N$ of closed
negative literals such that $P \vdash \frac{N}{t\goto{a}t'}$ must
contain a literal $\delta$ with \plat{T \not\models \delta}. The
latter means \plat{P\vdash_{ws} \epsilon} for a transition $\epsilon$
denying $\delta$. Collecting all such $\epsilon$'s (one for every
choice of $N$) in a set $K$ yields a well-supported proof of
$t\gonotto{a}t'$.
\end{proof}

\begin{proposition}{sound}
\sol{sound} is extended by Solutions
\ref{sol-least supported} (least supported) and \ref{sol-sound}b
(= \ref{sol-complete}, complete), and extends Solutions \ref{sol-positive}
(positive) and \ref{sol-scomplete} (complete with support).
\end{proposition}

\begin{proof}
By \pr{supported} a TSS that is sound with support determines a transition
relation that is a supported model. By \pr{soundness} (the soundness
of $\vdash_s$ w.r.t.\ $\models_s$), this transition relation is
included in any supported model. Therefore it constitutes the least.

By definition, the transition relation $T_1$ determined by a TSS $P$
that is sound with support is a model of $P$. The set $T_2$ of
transitions that are ${ws}$-provable from $P$ is well-supported, by
\pr{supported}. By \pr{ws-s} $T_1 \subseteq T_2$ and \pr{stable}
yields $T_1 = T_2$. If follows that $T_2$ is model too.

If a TSS $P$ is positive, then $P\vdash_s t\goto{a}t'$ iff $P \vdash
t\goto{a}t'$. By \pr{least} the ($s$-)provable transitions
form a model.

The last statement follows immediately from \pr{model}.
\end{proof}

\subsection{Solutions based on irrefutability}\label{irrefutability}

A second (and last) idea is to define the transition system $T$
associated to a TSS $P$ as the set of {\em $x$-irrefutable}
transitions, i.e.\ $T= \{t\goto{a}t' \mid P \not\vdash_x t \gonotto{a}
t' \}$, in which $x$ is $s$ or $ws$. This amounts to taking as the
meaning of $P$ the component $PT$ of its least [well-]supported model
$\rec{CT,PT}$.  This is consistent with Solutions \ref{sol-scomplete}
and \ref{sol-complete}, as for $x$-complete TSSs one has $P
\vdash_x t\goto{a} t' \Leftrightarrow P \not\vdash_x t\gonotto{a} t'$. 

\begin{proposition}{irrefutable}
The set of $x$-irrefutable transitions of any TSS consititutes a model.
\end{proposition}

\begin{proof}
Let $P$ be a TSS and \plat{\frac{H}{t\goto{a}t'}} be a closed
substitution instance of a rule of $P$. Let $T$ be the set of
$x$-irrefutable transitions and suppose $T \not\models
t\goto{a}t'$, i.e.\ $P \vdash_x t\gonotto{a}t'$. I have to prove that
$T \not\models H$. In case $x=s$ it follows from \pr{refutable}
that $H$ contains an $x$-refutable literal. I establish the
same in case $x=ws$.

Suppose that \plat{P \not\vdash_{ws} u \gonotto{b}u'} for each
positive antecedent \plat{\alpha = (u \goto{b} u')} in $H$. Then for
each such $\alpha$ there is a set $N_\alpha$ of $ws$-irrefutable
negative closed literals with $P \vdash \frac{N_\alpha}{\alpha}$. Let
$N$ be obtained from $H$ by replacing $\alpha$ by $N_\alpha$ for each
positive $\alpha$ in $H$. Then $N$ contains negative literals only.
Since $P \vdash_{ws} t\gonotto{a}t'$ and $P \vdash
\frac{N}{t\goto{a}t'}$, $N$ must contain a $ws$-refutable literal.
This literal must be in $H$, which had to be established.

In case the $x$-refutable literal in $H$ is positive, say
\plat{u\goto{b}u'}, we have \plat{P \vdash_x u\gonotto{a}u'}, which
implies \plat{T \not\models u\goto{b}u'}. In case it is negative, say
$v\gonotto{c}$, we have $\exists v' \in T(\Sigma): P \vdash_x
v\goto{c}v'$, which by the consistency of $\vdash_x$ implies $\exists
v': P \not\vdash_x v \gonotto{c}v'$, which implies $\exists v': T
\models v\goto{c} v'$ and thus $T\not\models v\gonotto{c}$.
In case of a literal $v\gonotto{c}v'$ just leave out the existential
quantifications.
\end{proof}
For the moment I restrict attention to solutions yielding
well-supported transition relations.

\begin{trivlist}
\item[]{\bf \sol{irrefutable}a}
A TSS is meaningful if the set of $s$-irrefutable transitions
(this being the associated transition relation) is well-supported.
\end{trivlist}

\begin{trivlist}
\item[]{\bf \sol{irrefutable}b}
A TSS is meaningful if the set of $ws$-irrefutable transitions
is well-supported.
\end{trivlist}
Note that by \pr{irrefutable} the transition relation determined by such
a TSS is even stable.

\begin{proposition}{irr}
\sol{irrefutable}a coincides with \sol{scomplete} and
\ref{sol-irrefutable}b with \ref{sol-complete}.
\end{proposition}

\begin{proof}
It follows immediatelty from \pr{supported} that the set of
$x$-irrefutable transitions of a $x$-complete TSS is well-supported.
Now let $P$ be a TSS whose set $T$ of $x$-irrefutable
transitions is well-supported.  Suppose $P \not\vdash_x
t\gonotto{a}t'$ for certain $t,t'\in T(\Sigma)$. Then $T \models
t\goto{a}t'.$ By the stability of $T$ there is a set $N$ of
closed negative literals such that \plat{P \vdash \frac{N}{t\goto{a}t'}}
and $T \models N$. The latter means $T \not\models v\goto{c}v'$ for
any literal $v\gonotto{c}v'$ in $N$, which means $P \vdash_x
v\gonotto{c}v'$. By \df{transition} and \lem{standard} the same holds
for literals $v\gonotto{c}$ in $N$. Therefore $P \vdash_x t\goto{a}t'$.
\end{proof}

\subsection{Attaching meaning to {\em all} transition system specifications}

In this section I will associate a transition relation to arbitrary TSSs.
As illustruted by $P_1$ and $P_2$, such a transition relation can not always
be a supported model. I will insist on soundness (being a model), and
thus have to give up support. Hence among the model theoretic
solutions only \sol{least} (least model) can provide inspiration.

Let me first decide what to do with $P_1$. Since the associated
transition relation should be a model, it must contain either
$c\goto{a}c$ or $c\goto{b}c$. For reasons of symmetry I cannot choose
between these transitions, so the only way out is to include both.
There is no reason to include even more transitions.  Hence the
transition system associated to $P_1$ should be \plat{\{c\goto{a}c,~
c\goto{b}c\}}.

The simplest model theoretic solution I thought of that gives this
result is to define $T_1$ as the union of all minimal models of a TSS\@.
In many cases this will be the desired transition relation, but in can
happen that $T_1$ is not a model. In that case $T_2$ is defined as the
union of all minimal models containing $T_1$, and iterating this
procedure until it stabilizes gives the associated transition relation.

However, in general this solution yields more transition then I would
like to see. The transition system associated to $P_3$ for instance
would be \plat{\{c\goto{a}c,~ c\goto{b}c\}}, whereas $\{c\goto{a}c\}$
appears to be sufficient. The same would hold after addition of a
second premise $c\gonotto{a}$ to the only rule in $P_3$.  In case
there are other closed terms besides $c$ the associated transition
relation will be even larger.  Therefore I will not pursue this idea
further, and turn to the proof theoretic solutions instead.  The
reason for prefering transition $c\goto{a}c$ over \plat{c\goto{b}c} in
$P_3$ is not that $c\goto{a}c$ is provable---after addition of the
premise $c\gonotto{a}$ it is not---but that \plat{c\goto{b}c} is
refutable. Therefore I consider:

\begin{solution}{irrefutable}({\em Irrefutable}).
Any TSS is meaningful. The associated transition relation consists of
the $ws$-irrefutable transitions.
\end{solution}
In the case of $P_1$ this yields the desired result $\{c\goto{a}c,~
c\goto{b}c\}$ and likewise $P_2$, $P_3$ and $P_4$ yield $\{c\goto{a}c\}$.
The transition relation of $P_7$ is the same as the one of $P_1$.
This indicates that \sol{irrefutable} is inconsistent with Solutions
\ref{sol-least}--\ref{sol-stable}. I don't consider this to be a
problem, as the model theoretic allocation of a transition relation to
$P_7$ was not very convincing.

A variant of \sol{irrefutable} is to associate to a TSS the set of its
$s$-irrefutable transitions. This solution is inconsistent with
\sol{positive} (positive) as the transition relation of $P_5$ would
consist of $c\goto{a}c$. Note that this transition relation is
supported. In order to rule out this anomaly one would have to
restrict the meaningful TSSs to the ones for which the associated
transition relation is well-supported, which yields
\sol{irrefutable}a, that has been shown to coincide with \sol{scomplete}.

Another variant is to stick to the $ws$-irrefutable transitions, but
require those to form a supported model. Note that adding rules
$\frac{x\goto{a}y}{x\goto{a}y}$ for $a \in A$ to an arbitrary TSS
does not change the associated transition relation according to
\sol{irrefutable}, but makes this relation supported.  Thus requiring
the associated transion relation to be supported is not much of a
restriction. Moreover, as rules like the one above should not make the
difference between meaningful and meaningless TSSs, this requirement
is not recommended.

\section{Reduction}\label{reduction}

In this section I show that the method of {\em reduction} of {\sc Bol
\& Groote} \cite{BolG91} coincides with \sol{complete}.

In \cite{BolG91} the operations $True$, $Pos$ and
$Red^\kappa$ for $\kappa$ an ordinal are defined on TSSs without variables.
The operator $True$ deletes all rules with negative premises and thus
yields a positive TSS. The operator $Pos$ deletes all negative
premises from rules, and hence also yields a positive TSS.
Finally the operator $Red^\kappa$ deletes all rules that
\begin{itemize}\vspace{-1ex}
\item contain a positive premise that for some $\lambda<\kappa$ is not
provable from $Pos(Red^\lambda(P))$\vspace{-1ex} or
\item contain a negative premise that for some $\lambda<\kappa$ is
refutable from $True(Red^\lambda(P))$\vspace{-1ex}
\end{itemize}
and in the remaining rules deletes all premises that are
\begin{itemize}\vspace{-1ex}
\item positive and for some $\lambda<\kappa$ 
provable from $True(Red^\lambda(P))$\vspace{-1ex} or
\item negative and for some $\lambda<\kappa$ not
refutable from $Pos(Red^\lambda(P))$.\vspace{-1ex}
\end{itemize}
The idea is that the positive TSSs $True(Red^\kappa(P))$ only prove
transitions that surely hold, whereas the positive TSSs
$Pos(Red^\kappa(P))$ prove all transitions that possibly hold.
Thus ``not provable (or refutable, see \df{proof}) from
$Pos(Red^\lambda(P))$'' means ``not provable (resp.\ refutable) at all''.
Now a TSS without variables is said to be {\em positive after
reduction} if for certain ordinal $\kappa$, $Red^\kappa(P)$ is a
positive TSS. In that case $True(Red^\kappa(P)) = Red^\kappa(P)
= Pos(Red^\kappa(P))$ and $Red^{\kappa+1}$ is a TSS in which no rule
has premises. The transition relation associated to such a TSS
consists of the transitions provable from $Red^\kappa(P)$, which are
the rules of $Red^{\kappa+1}(P)$. The case of TSSs with variables
reduces to the case without variables by taking the set of all closed
substitution instances of the rules in such a TSS.

\begin{lemma}{reduction}Let $P$ be a TSS without variables.\\
1. For any closed positive literal $\alpha$: $P\vdash_{ws} \alpha
~\Rightarrow~ \exists \kappa: True(Red^\kappa(P)) \vdash \alpha$, and\\
2. for any closed negative literal $\alpha$: $P\vdash_{ws} \alpha
~\Rightarrow~ \exists \kappa: Pos(Red^\kappa(P))$ does not refute $\alpha$.
\end{lemma}

\begin{proof}
With induction on the structure of proofs. Suppose $P \vdash_{ws}
\alpha$ by means of a proof $p$ and the statements are established of
$\beta$'s obtainable by subproofs. Let $H$ be the set of
labels directly above the root of $p$. For any literal $\beta \in
H$, one has $P\vdash_{ws}\beta$ by means of a subproof of $p$.
Thus, for $\beta$ positive $\exists \lambda: True(Red^\lambda(P))
\vdash \beta$ and for $\beta$ negative $\exists \lambda:
Pos(Red^\lambda(P))$ does not refute $\beta$. Let $\kappa$ be a strict
upperbound of all those $\lambda$'s.

Now there are two cases. If $\alpha$ is positive, there is a rule
$\frac{H}{\alpha}$ in $P$. By construction, all premises of this rule
are deleted in the reduction process, and $\frac{\emptyset}{\alpha}$
is a rule in $Red^\kappa(P)$. Hence $True(Red^\kappa(P)) \vdash
\alpha$.

Now suppose $\alpha$ is negative and $Pos(Red^\kappa(P))$ refutes
$\alpha$. This means that $Pos(Red^\kappa(P)) \vdash \gamma$ for
$\gamma$ a literal denying $\alpha$, which implies that
$Red^\kappa(P) \vdash \frac{N}{\gamma}$ for $N$ a set of negative
closed literals. Since $p$ is a well-supported proof, a literal
$\beta \in H$ denies a literal $\delta$ in $N$. $\beta$ must be
positive, so $\exists \lambda < \kappa: True(Red^\lambda(P)) \vdash
\beta$, and $\delta$ is refutable from $True(Red^\lambda(P))$. It
follows that at least one of the rules needed in the proof of
\plat{\frac{N}{\gamma}} has been deleted in $Red^\kappa(P)$,
contradicting \plat{Red^\kappa(P) \vdash \frac{N}{\gamma}}. Hence
$Pos(Red^\kappa(P))$ does not refute $\alpha$.
\end{proof}

\begin{proposition}{reduction}
Let $P$ be a TSS without variables and $\alpha$ a closed literal. Then
$$Red^\kappa(P) \vdash_{ws} \alpha ~~\Rightarrow~~ P \vdash_{ws} \alpha.$$
\end{proposition}
\pagebreak
\pf By transfinite induction on $\kappa$. Suppose the statement has
been established for all ordinals $\lambda < \kappa$. By definition
$True(P) \vdash t\goto{a}t' \Rightarrow P \vdash_{ws}
t\goto{a}t'$ and if $\beta$ is negative and for all $\gamma$ denying
$\beta$ we have $Pos(P) \not\vdash \gamma$ then $P \vdash_{ws} \beta$.
Substituting $Red^\lambda(P)$ for $P$ yields
\begin{itemize}\vspace{-1ex}
\item[(i)] If $\beta$ is positive and for some $\lambda<\kappa$ 
provable from $True(Red^\lambda(P))$\vspace{-1ex} then $P \vdash_{ws} \beta$,
and \item[(ii)] if $\beta$ is negative and for some $\lambda<\kappa$ not
refutable from $Pos(Red^\lambda(P))$\vspace{-1ex} then $P \vdash_{ws} \beta$.
\end{itemize}
Apply a (nested) induction on the structure of a well-supported
proof $p$ of $\alpha$ from $Red^\kappa(P)$. Let $K$ be the set of
labels directly above the root of $p$. By induction $P \vdash_{ws}
\beta$ for any $\beta \in K$. In case $\alpha$ is positive,
$\frac{K}{\alpha}$ must be a rule in $Red^\kappa(P)$. Hence for a
certain set $H$ of premises $\frac{K\cup H}{\alpha}$ must be a rule
in $P$. The premises in $H$ are deleted in the definition of
$Red^\kappa$, and thus, by (i) and (ii), are $ws$-provable from $P$.
It follows that $P \vdash_{ws} \alpha$.

Now let $\alpha$ be negative. Suppose $P \vdash \frac{N}{\gamma}$ with
$\gamma$ a literal denying $\alpha$ and $N$ a set of closed negative
literals. I have to show that $P \vdash_{ws} \beta$ for a literal
$\beta$ denying a literal $\delta$ in $N$. There are two cases.
\begin{itemize}\vspace{-1ex}
\item Suppose $N$ contains a literal $\delta$ that for some $\lambda < \kappa$
is refutable from $True(Red^\lambda(P))$. This means that
$True(Red^\lambda(P))\vdash \beta$ with $\beta$ denying
$\delta$. Obviously $Red^\lambda(P)\vdash \beta$, hence
$Red^\lambda(P)\vdash_{ws} \beta$ and by induction $P\vdash_{ws}
\beta$.\vspace{-1ex}
\item Suppose $N$ contains no such literal. By induction on the
structure of proofs I establish that $P \vdash \frac{N}{\epsilon}
\Rightarrow Red^\lambda(P) \vdash \frac{N}{\epsilon}$ for any
transition $\epsilon$ and $\lambda \leq \kappa$. Namely, suppose
$q$ is a proof of $\frac{N}{\epsilon}$ from
$P$. Then for any $\zeta \neq \epsilon$ appearing in $q$ we have \plat{P
\vdash \frac{N}{\zeta}} by means of a smaller proof, and hence
\plat{Red^\lambda(P) \vdash \frac{N}{\zeta}} for any $\lambda \leq
\kappa$, which implies $Pos(Red^\lambda(P)) \vdash \zeta$.  It follows
that $q$ employs no rule that is deleted in the construction of
$Red^\mu(P)$ for $\mu \leq \kappa$.
Thus, by cutting the branches in $q$ that sprout from deleted
premises in $Red^\mu(P)$, a proof $q'$ from $Red^\mu(P)$ is
obtained of a rule $\frac{N'}{\epsilon}$ with $N' \subseteq N$. 
Therefore $Red^\mu(P) \vdash \frac{N}{\epsilon}$, as
claimed.  In particular \plat{Red^\kappa(P) \vdash \frac{N}{\gamma}}.  By
the definition of a well-supported proof ($p$), a literal $\beta$ in $K$
denies one in $N$. As remarked already, $P \vdash_{ws} \beta$.\hfill $\Box$
\end{itemize}

\begin{theorem}{reduction}
A TSS is positive after reduction iff it is complete. In that case the
associated transition relation is the set of ${ws}$-provable
transitions.
\end{theorem}

\begin{proof}
Without limitation of generality I can restrict attention to TSSs
$P$ without variables.

Suppose $P$ is positive after reduction. In that case there is an
ordinal $\kappa$ such that the rules of $Red^\kappa(P)$ have no
premises. Thus for any transition $t\gonotto{a}t'$ either
$Red^\kappa(P)\vdash_{ws} t\goto{a}t'$ or $Red^\kappa(P)\vdash_{ws}
t\gonotto{a}t'$.  By \pr{reduction} the same holds for $P$, which
therefore must be complete. As $\vdash_{ws}$ is sound we have 
$Red^\kappa(P) \vdash t\goto{a}t' \Leftrightarrow P \vdash_{ws} t\goto{a}t'$.

Now suppose $P$ is complete. For each closed literal $\alpha$ with
$P\vdash_{ws} \alpha$, there is an ordinal $\kappa$ given by
\lem{reduction}. Let $\mu$ be a strict upperbound of those $\kappa$'s.
I will show that $Red^\mu(P)$ is positive. Let $\frac{H}{\alpha}$ be a
rule in $P$ and $\beta \in H$ a negative premises. In case
$P\not\vdash_{ws} \beta$, by completeness or \pr{complete} I have $P
\vdash_{ws} \gamma$ for a (positive) literal $\gamma$ denying $\beta$,
i.e.\ $\beta$ is $ws$-refutable from $P$. By \lem{reduction}.1 $\beta$
is refutable from $True(Red^\kappa(P))$ for some $\kappa < \mu$.
Hence $\frac{H}{\beta}$ does not occur in $Red^\mu(P)$.  In case $P
\vdash_{ws} \beta$, \lem{reduction}.2 implies that $\beta$ will be
deleted from $H$ in $Red^\mu(P)$.
\end{proof}
It is possible to simplify the definition of $Red^\kappa$ by deleting
only (rules with) {\em negative} premises. I.e.\ $Red^\kappa$ deletes
all rules that contain a negative premise that for some
$\lambda<\kappa$ is refutable from $True(Red^\lambda(P))$, and in the
remaining rules deletes all negative premises that for some
$\lambda<\kappa$ are not refutable from $Pos(Red^\lambda(P))$.
For this version of $Red$ \lem{reduction}, \pr{reduction} and
\th{reduction} remain true, with only slightly adapted proofs.
Thus this simplified method of reduction gives the same meaning to
TSSs as the original one.

\section{Solutions based on stratification}

Here I review two methods to assign meaning to transition system
specifications based on the technique of {\em (local) stratification}, as
proposed in the setting of logic programming by {\sc Przymusinski}
\cite{Prz88}. This technique was tailored for TSSs by {\sc Groote}
\cite{Gr93}.

\begin{definition}{stratification}({\em stratification}).
A function $S:(T(\Sigma) \times A \times T(\Sigma)) \rightarrow \lambda$,
where $\lambda$ is an ordinal, is called a {\em stratification} of a
TSS $P=(\Sigma,R)$ if for every rule $\frac{H}{\alpha}\in R$ and every
substitution $\sigma:V \rightarrow T(\Sigma)$ it holds that
\begin{center}
\begin{tabular}{l}
for all positive literals $\beta \in H: S(\sigma(\beta)) \leq
S(\sigma(\alpha))$ and\\
for all transitions $\beta$ denying a negative literal in $H:
S(\sigma(\beta)) < S(\sigma(\alpha))$.
\end{tabular}
\end{center}
A stratification is {\em strict} if also for all positive literals
$\beta \in H: S(\sigma(\beta)) < S(\sigma(\alpha))$.\\
A TSS with a (strict) stratification is said to be {\em (strictly) stratified}.
\end{definition}
In a stratified TSS no transition depends negatively on itself. A
transition relation is associated to such a TSS one {\em
stratum} $S_\kappa = \{\alpha \mid S(\alpha)=\kappa\}$ at a time. A
transition in $S_0$ is present iff it is provable in the sense of
\df{proof}, and as soon as one knows the about validity of all
transitions $\alpha$ with $S(\alpha) < \kappa$ for an ordinal
$\kappa$, one knows the validity of all negative premises that could
occur in a proof of a transition in stratum $\kappa$, which determines
the validity of those transitions. 

\begin{definition}{strat-trans}
Let $P$ be a TSS with a stratification $S$ with range $\lambda$. The
transition relations $T_{\kappa}$ with $\kappa < \lambda$ are
defined by transfinite recursion through
$${\textstyle T_{\kappa} = \{\alpha \mid S(\alpha)=\kappa \wedge P
\vdash \frac{H}{\alpha}} \mbox{ for a set of closed literals
$H$ with } \plat{\displaystyle \bigcup_{\mu<\kappa} T_{\mu} \models H \}.}$$
The transition relation $T_{P,S}$ {\em associated with P} (and {\em based on
$S$}) is $\bigcup_{\mu<\lambda} T_{\mu}$.
\end{definition}
Note that each transition in such a set $H$ or denying a literal in
$H$ is in a lower stratum than $\alpha$. Hence $\bigcup_{\mu<\kappa}
T_\mu \models H$ iff $T_{P,S} \models H$.
In {\sc Bol \& Groote} \cite{BolG91} $T_\kappa$ is defined by
$T_{\kappa} = \{\alpha \mid P_\kappa \vdash \alpha\}$ where 
$P_\kappa$ is the set of all rules $\frac{H^{\kappa}}{\alpha}$
obtained from closed substitution instances $\frac{H}{\alpha}$ of
rules from $P$ with $S(\alpha)=\kappa$ and $\bigcup_{\mu<\kappa} T_\mu
\models H-H^\kappa$. Here $H^\kappa = \{\beta \in H \mid \beta \mbox{
positive } \wedge S(\beta)=\kappa\}$.

\begin{proposition}{strat-BolG}
\df{strat-trans} agrees with the definition in \cite{BolG91}.
\end{proposition}

\begin{proof}
Suppose $\alpha \in T_\kappa$ according to \df{strat-trans}. Let $p$
be a closed proof of $\frac{H}{\alpha}$ where $H$ is a set of literals
with $\bigcup_{\mu<\kappa} T_\mu \models H$. Let $p'$ be obtained from
$p$ by deleting all branches above nodes labelled with a transition
$\beta$ with $S(\beta) < \kappa$. Then $p'$ is a proof from $P$ of a
rule \plat{\frac{H'}{\alpha}} with $\bigcup_{\mu<\kappa} T_\mu \models H'$.
All rules used in $p'$ are also rules in $P_\kappa$, except that there
the premises from $H'$ are deleted. It follows that $P_\kappa \vdash
\alpha$. The other direction is straightforward.
\end{proof}
The definition in \cite{BolG91} can in turn be seen to coincide with
the original one in {\sc Groote} \cite{Gr93}.

\begin{proposition}{strat-complete}
If $P$ is a TSS with stratification $S$ and $\alpha$ a closed
literal, then $P \vdash_{ws}\! \alpha$ iff $T_{P,S} \models \alpha$.
\end{proposition}

\begin{proof}
Define $S(\alpha)$ for $\alpha$ negative to be the least strict
upperbound of $\{S(\beta)\mid \beta$ denies $\alpha\}$. Under this
definition the two conditions in \df{stratification} can be combined
into \begin{center}
for all literals $\beta \in H: S(\sigma(\beta)) \leq S(\sigma(\alpha)).$
\end{center}
For $\alpha,\beta$ closed write $\alpha < \beta$ if either
$S(\alpha) < S(\beta)$ or $S(\alpha)=S(\beta)$ with $\alpha$ negative
and $\beta$ positive.

``if'': With induction on $<$.  Suppose $T_{P,S} \models
\alpha$ and the statement has been obtained for literals $\beta$ with
$\beta < \alpha$. If $\alpha$ is positive then $\alpha \in
T_{S(\alpha)}$ and there is a set $H$ of closed literals with $P
\vdash \frac{H}{\alpha}$ and $\bigcup_{\mu<S(\alpha)} T_\mu \models
H$, which implies $T_{P,S} \models H$. As $\beta < \alpha$ for each
$\beta \in H$, $P \vdash_{ws} H$ and thus $P \vdash_{ws} \alpha$. In
case $\alpha$ is negative, then for each transition $\gamma$ that
denies $\alpha$ one has $T_{P,S}\not\models \gamma$, i.e.\ $\gamma
\not\in T_{S(\gamma)}$. Hence, each set $H$ of closed literals with
\plat{P \vdash \frac{H}{\gamma}} contains a literal $\delta$ with
$\bigcup_{\mu<S(\gamma)} T_\mu \not\models \delta$. This implies the
existence of a literal $\beta$ denying $\delta$ such that
$\bigcup_{\mu<S(\gamma)} T_\mu \models \beta$. This holds in
particular for sets $H$ only containing negative literals, and in such
a case $\beta < \delta < \gamma < \alpha$ and $T_{P,S} \models \beta$,
so $P \vdash_{ws} \beta$. This for every choice of $\gamma$ and a
negative $H$. \df{wsp} yields $P\vdash_{ws} \alpha$.

``only if'': Suppose $P \vdash_{ws} \alpha$ with $\alpha$ negative.
Then for any transition $\beta$ denying $\alpha$ \pr{consistency} gives
$P \not\vdash_{ws} \beta$, and by ``if'' $T_{P,S} \not\models \beta$.
By \df{transition} this implies $T_{P,S} \models \alpha$.
Similarly suppose $P \vdash_{ws} t\goto{a}t'$. Then $P
\not\vdash_{ws} t\gonotto{a}t'$, so by ``if'' $T_{P,S} \not\models
t\gonotto{a} t'$. By definition this implies $T_{P,S} \models t\goto{a}t'$.
This proof benefits highly from the consideration of literals of the
form $t\gonotto{a} t'$.
\end{proof}

\begin{proposition}{strat-unique}
Let $P$ be a TSS with two stratifications $S$ and $S'$. Then $T_{P,S}
= T_{P,S'}$.
\end{proposition}

\begin{proof}
This is Lemma 2.5.4 in \cite{Gr93}. Here it is an immediate corollary
of \pr{strat-complete}.
\end{proof}
The last proposition says that for a stratified TSS the choice of the
stratification in the construction of the transition relation is
immaterial. This enables the following solution to (\ref{quest}).

\begin{solution}{stratified}({\em Stratified\/}) \cite{Prz88,Gr93}.
A TSS is meaningful iff it is stratified. The associated
transition relation is given in \df{strat-trans}.
\end{solution}

\begin{proposition}{strat-pos-complete}
\sol{stratified} strictly extends \sol{positive} and is strictly
extended by \sol{complete}.
\end{proposition}

\begin{proof}
If $P$ is positive take $S(\alpha)=0$ for all $\alpha$. This is a
stratification and $T_{P,S} = T_0 = \{\alpha \mid P\vdash \alpha \}$.
The second statement is an immediate consequence of
\pr{strat-complete}, using that for any transition $t\goto{a}t'$
either $T \models t\goto{a}t'$ or $T \models t\gonotto{a}t'$.

Strictness follows from $P_3$ and $P_6$, which are stratified but not
positive, and $P_8$ below, which is complete but not stratified.
\end{proof}\vspace{-3ex}
$$\begin{array}{@{}c@{}|cc|@{}}
\cline{2-3}
\makebox[0pt][r]{$P_8~~~\rule[-14pt]{0pt}{36pt}$}
&\displaystyle c\goto{a}c
&\displaystyle\frac{c\gonotto{a}}{c\goto{a}c}\\
\cline{2-3}
\end{array}$$

\begin{solution}{strict}({\em Strictly stratified\/}) \cite{Gr93}.
A TSS is meaningful iff it is strictly stratified. The associated
transition relation is as in \df{strat-trans}, but with `$P \vdash
\frac{H}{\alpha}$' replaced by `$\frac{H}{\alpha}$ is a closed
substitution instance of a rule of $P$'.
\end{solution}

\begin{proposition}{strict-complete}
\sol{strict} is strictly extended by Solutions \ref{sol-stratified}
and \ref{sol-scomplete} (complete with support).
\end{proposition}

\begin{proof}
Note that $T_{P,S}$ in \df{strat-trans} would not change if $P \vdash
\frac{H}{\alpha}$ were replaced by `$\frac{H}{\alpha}$ is provable by
means of a proof in which for all transitions $\beta$ labelling a
non-leaf we have $S(\beta)=S(\alpha) =\kappa$'. This follows from the first
four sentences in the proof of \pr{strat-BolG}. In the special case
that $S$ is stratified, this modified definition agrees with the one
proposed in \sol{strict}, which establishes the consistency of
Solutions \ref{sol-stratified} and \ref{sol-strict}.

Just like in \pr{strat-complete} one can prove that if $P$ is a TSS
with a strict stratification $S$ and $\alpha$ is a closed literal,
then $P \vdash_s \alpha \Leftrightarrow T_{P,S} \models \alpha$.
This implies that \sol{scomplete} extends \sol{strict}.

Strictness follows from $P_5$ and $P_6$, which are stratified but not
strictly so, and $P_8$, which is complete with support but not
strictly stratified.
\end{proof}

\section{Compositionality}\label{compositionality}

In concurrency theory it is common practice to group together
representations of concurrent systems in equivalence classes. This is
done when these representations are thought to represent the same
system, or at least systems whose essential properties are the same.
As system representations often closed terms over some signature are
concidered.  The equivalence relation employed is then formulated in
terms of the transition relation between closed terms obtained from a
given TSS over that signature.  In order to allow modular reasoning it
is important to use an equivalence relation that is a {\em congruence}.
This means that the meaning (the associated equivalence class) of a
closed term $f(t_1,...,t_n)$ is completely determined by the meaning
of the subterms $t_1,...,t_n$. The most popular equivalence relation
is {\em bisimulation equivalence}. In {\sc Bol \& Groote}
\cite{BolG91} it was established that for complete TSSs whose rules
satisfy a syntactic criterion (the {\em well-founded ntyft/ntyxt
format}, developed earlier in \cite{GrV92,Gr93}), bisimulation
equivalence is guaranteed to be a congruence, and so are many other
equivalence relations. Moreover, a counterexample was given againts
the extension of this result to TSSs that are meaningful according to
\sol{stable} (stable).  Of course the example concerned an incomplete
TSS in well-founded ntyft/ntyxt format with a unique stable transition
relation for which bisimulation is not a congruence.  This TSS also
has a unique supported model, and thus shows that the congruence
theorem does not generalise to \sol{unique supported} either.  Here I
show that also \sol{irrefutable}---or any other proof theoretic
solution for that matter---does not lend itself to such a
generalisation, indicating that \sol{complete} (complete) is the most
general one for which this nice result holds. My counterexample
concerns the following TSS $S$ over a signature with constants $c$,
$d$ and $e$ and a unary function $f$.
$$\begin{array}{@{}c@{}|ccc|@{}}
\cline{2-4}
\makebox[0pt][r]{$S~~~\rule[-14pt]{0pt}{36pt}$}
&\displaystyle c\goto{a}f(c)
&\displaystyle\frac{x\goto{a}y\gonotto{a}}{f(x)\goto{a}c}
&\displaystyle d\goto{a}e\\
\cline{2-4}
\end{array}$$
This TSS is surely in the well-founded ntyft/ntyxt format. It has
a unique 3-valued stable transition relation, namely 
$$\rec{\{c\goto{a}f(c),~ d\goto{a}e,~ f(d)\goto{a}c \},~
\{c\goto{a}f(c),~ d\goto{a}e,~ f(d)\goto{a}c,~ f(c) \goto{a} c\}}.$$
Thus the transitions $c\goto{a}f(c)$, $d\goto{a}e$ and $f(d)\goto{a}c$
are $ws$-provable, and with the exception of $f(c)\goto{a}c$, all
other transitions are $ws$-refutable. Note, by the way, that for this
TSS there is no difference between $s$-provability and
$ws$-provability, or between $s$- and $ws$-refutability. This can be
verified directly, or through \pr{finite failure}. As the 3-valued
relation above is not 2-valued, the TSS is incomplete (has no meaning
according to \sol{complete}). It also has no meaning under
\sol{stable} (stable). The 3-valued transition relation constitutes
the most acceptable interpretation of $S$. If we insist on 2-valued
relations, the proof theorectic approach offers only one choice, namely
whether or not to include the transition $f(c)\goto{a}c$. Each of
these possibilities yields a transition relation for which
bisimulation is not a congruence, and if fact no equivalence relation
used in concurrency theory is a congruence.  The only properties of
such equivalence relations needed here, is that systems for which the
reachable parts of the transition relation are isomorphic are
equivalent, and a system without outgoing transitions (a {\em
deadlock}) cannot be equivalent to a system with an outgoing $a$-transition.
\sol{irrefutable} (irrefutable) includes the transition
$f(c)\goto{a}c$. Now $c$ and $f(c)$ are equivalent (the reachable part
of the transition relation from each of them is an $a$-loop), but
$f(c)$ and $f(f(c))$ are inequivalent ($f(f(c))$ deadlocks).
Taking only the provable transitions (instead of the irrefutable ones)
would exclude the transition $f(c)\goto{a}c$. In that case $c$ and $d$ are
equivalent, but $f(c)$ and $f(d)$ are not.

\section{Conclusion}

I presented 11 answers to the question which transition system
specifications are meaningful and which transition relations they
specify. The relations between these 11 solutions are indicated in
Figure~\ref{solutions}. 
\begin{figure}[htb]
\begin{center}
\begin{picture}(80,60)(-40,0)
\put(-20,60){\makebox[0pt][c]{positive (\ref{sol-positive})}}
\put(-26,59){\vector(-1,-2){13}}
\put(-15,59){\vector(1,-2){13}}
\put(15,29){\vector(1,-2){13}}
\put(-40,30){\makebox[0pt][c]{stratified (\ref{sol-stratified})}}
\put(-40,29){\vector(0,-1){11}}
\put(-40,15){\makebox[0pt][c]{complete (\ref{sol-complete})}}
\put(-40,14){\vector(0,-1){11}}
\put(-40,0){\makebox[0pt][c]{stable (\ref{sol-stable})}}
\put(22,60){\makebox[0pt][c]{strictly stratified (\ref{sol-strict})}}
\put(16,59){\vector(-2,-1){52}}
\put(28,59){\vector(1,-1){11}}
\put(40,45){\makebox[0pt][c]{complete with support (\ref{sol-scomplete})}}
\put(26,44){\vector(-2,-1){22}}
\put(40,44){\vector(0,-1){26}}
\put(40,15){\makebox[0pt][c]{unique supported (\ref{sol-unique supported})}}
\put(40,14){\vector(0,-1){11}}
\put(40,00){\makebox[0pt][c]{least supported (\ref{sol-least supported})}}
\put(0,30){\makebox[0pt][c]{sound with support (\ref{sol-sound})}}
\put(-6,29){\vector(-2,-1){23}}
\put(0,15){\makebox[0pt][c]{least model (\ref{sol-least})}}
\put(-18,59){\vector(1,-3){13.7}}
\put(18,15){\makebox[0pt][c]{\LARGE $\#$}}
\put(18,7.5){\makebox[0pt][c]{\LARGE $\#$}}
\put(12,3){\line(1,1){4}}
\put(19.5,10.5){\line(1,1){4}}
\put(0,7.5){\makebox[0pt][c]{\LARGE $\#$}}
\put(0,3){\line(0,1){2.5}}
\put(0,12){\line(0,1){2.5}}
\put(-22,0){\makebox[0pt][c]{\LARGE $\#$}}
\put(-30,1){\line(1,0){4}}
\put(-18,1){\line(1,0){4}}
\put(-29,14){\vector(2,-1){22}}
\put(0,0){\makebox[0pt][c]{irrefutable (\ref{sol-irrefutable})}}
\end{picture}
\end{center}
\caption[solutions]{Relations between Solutions
\ref{sol-positive}--\ref{sol-strict}\label{solutions}}
\end{figure}
There \begin{picture}(15,2)
\put(0,0){$S_1$} \put(5,1){\vector(1,0){5}} \put(11,0){$S_2$}
\end{picture}
indicates that solution $S_2$ extends $S_1$, as defined in Section 1,
and $S_1 \# S_2$ indicates that $S_1$ and $S_2$ are inconsistent.
By the definition of extension and consistency,
\begin{picture}(26,2)
\put(0,0){$S_1$} \put(5,1){\vector(1,0){5}} \put(11,0){$S_2$}
\put(16,1){\vector(1,0){5}} \put(22,0){$S_3$}
\end{picture}
implies \begin{picture}(15,2)
\put(0,0){$S_1$} \put(5,1){\vector(1,0){5}} \put(11,0){$S_3$}
\end{picture}
({\em transitivity}) and
\begin{picture}(24,2)
\put(0,0){$S_1$} \put(5,0){\#} \put(9,0){$S_2$}
\put(14,1){\vector(1,0){5}} \put(20,0){$S_3$}
\end{picture}
implies $S_1 \# S_3$ ({\em conflict heredity}).
All extensions are strict and there are no more extensions or
inconsistencies than indicated in the figure (or derivable by
transitivity and conflict heredity). 
The arrows in Figure~\ref{solutions} have been established in
Propositions \ref{pr-least}, \ref{pr-strat-pos-complete},
\ref{pr-strict-complete}, \ref{pr-complete-unique} and \ref{pr-sound}
and in the third sentence of Section~\ref{irrefutability}, whereas
the remaining consistency results follow from \pr{consistent}.
Strictness, the absence of further extensions and the inconsistencies
follow from the information collected in Table 1, which
indicates which of the TSSs $P_1$--$P_8$ given in this paper are
meaningful according to each of the solutions. 
A `$-$' indicates that the TSS is meaningless, a `$+$' that it has the
same meaning as given by \sol{irrefutable}, and a `$*$' that is has a
meaning different from the one given by \sol{irrefutable}.
\begin{center}
\begin{tabular}{|r|l|c|c|c|c|c|c|c|c|}
\hline
\multicolumn{2}{|l|}{Solution}&$P_1$&$P_2$&$P_3$&$P_4$&$P_5$&$P_6$&$P_7$&$P_8$\\
\hline
1 & positive		&$-$&$-$&$-$&$-$&$+$&$-$&$-$&$-$\\
2 & least		&$-$&$+$&$-$&$+$&$+$&$-$&$*$&$+$\\
3 & least supported 	&$-$&$-$&$+$&$*$&$+$&$-$&$*$&$+$\\
4 & unique supported	&$-$&$-$&$+$&$*$&$-$&$-$&$*$&$+$\\
5 & stable		&$-$&$-$&$+$&$-$&$+$&$+$&$*$&$+$\\
6 &complete with support&$-$&$-$&$+$&$-$&$-$&$-$&$-$&$+$\\
7 & complete		&$-$&$-$&$+$&$-$&$+$&$+$&$-$&$+$\\
8 & sound with support	&$-$&$-$&$+$&$-$&$+$&$-$&$-$&$+$\\
9 & irrefutable		&$+$&$+$&$+$&$+$&$+$&$+$&$+$&$+$\\
10& stratified		&$-$&$-$&$+$&$-$&$+$&$+$&$-$&$-$\\
11& strictly stratified &$-$&$-$&$+$&$-$&$-$&$-$&$-$&$-$\\
\hline
\end{tabular}\\[2ex]
Table 1: Counterexamples\vspace{-1ex}
\end{center}

\subsection*{Logic programming}\vspace{-2pt}

Everything said in this paper about transition system specifications
applies equally well to {\em proposition system specifications (PSSs)}.
These are obtained by replacing the set $A$ of actions by a set of
{\em predicate declarations} $(p,n)$ with $p\not\in V$ a {\em
predicate symbol} (different from any function symbol) and $n \in
\IN$. A literal is then an expression $p(t_1, \ldots, t_n)$ or $\neg 
p(t_1, \ldots, t_n)$ with $t_i \in \IT(\Sigma)$. From here on all
concepts are defined as before. Note that a logic program is a PSS
obeying some finiteness conditions. Hence everything said applies to
logic programming too.

Note that a PSS can be seen as a special kind of TSS. First of all
an $n$-ary predicate $p$ can be expressed in terms of an $n$-ary
function $f_p$ and the unary predicate $holds$, namely by defining
$holds(f_p(t_1,...,t_n))$ as $p(t_1,...,t_n)$. Next, if $p$ is a unary
predicate then $p(t)$ can be encoded as the transition \plat{t
\goto{p} 0}, with $0$ a constant introduced specially for this purpose
(cf.\ {\sc Verhoef} \cite{Ver94}).

Likewise a TSS can be encoded as a PSS by considering $\goto{a}$ to be
a binary predicate for any $a \in A$, or, as in {\sc Bol \& Groote}
\cite{BolG91}, $\goto{}$ as a single ternary predicate with $a \in A$
interpreted as a term. A negative literal $t\gonotto{a}t'$ denotes
$\neg(t\goto{a}t')$ and $t\gonotto{a}$ can be seen as an abbreviation
of the (infinite) conjunction of $t\gonotto{a}t'$ for $t'\in
\IT(\Sigma)$. These translations preserve all concepts of this paper.
In order to avoid the infinite conjunction, Bol \& Groote introduce
the unary version of $\goto{a}$ (or actually the binary version of
$\goto{}$) as a separate predicate, linked to the binary (ternary)
version by the rule $\displaystyle\frac{x\goto{a}y}{x\goto{a}}$,
implicitly present in every TSS.  As shown in anomaly A.3 in
\cite{BolG91} this translation does not preserve \sol{least} (least
model). However, it does preserve the other concepts.

In this paper I do not touch issues that are relevant in logic
programming, but not manifestly so for transition system
specifications. For these, and many more references, see {\sc Apt \&
Bol} \cite{AB94}.\vspace{-3pt}

\subsection*{Evaluation of the solutions}\vspace{-2pt}

\sol{positive} is the classical interpretation of TSSs without negative
premises, and Solutions~\ref{sol-least} (least model)
and~\ref{sol-least supported} (least supported model) are two
straightforward generalisations. \sol{unique supported} (unique
supported model) stems from {\sc Bloom, Istrail \& Meyer}
\cite{BIM88}, where it was used to ascertain that TSSs in their
so-called GSOS format are meaningful (such TSSs have unique supported
models). My counterexample $P_4$ shows that \sol{unique supported}
yields contraintuitive results and is therefore not suited to base
such a conclusion on. Fortunately, TSSs in the GSOS format are even
strictly stratified, which is one of the most restrictive criteria for
meaningful TSSs considered. \sol{least supported} can be rejected on
the same grounds as \sol{unique supported} and \sol{least} is not very
useful because it leaves most TSSs with negative premises meaningless
(cf.\ $P_3$).

\sol{stratified} (stratified) stems from {\sc Przymusinski}
\cite{Prz88} and is the perhaps the best known solution in logic
programming. A variant that also satisfies the criterion of
\sol{unique supported} is \sol{strict} (strictly stratified), proposed
by {\sc Groote} \cite{Gr93}.

\sol{stable} (unique stable transition relation) stems from {\sc
Gelfond \& Lifschitz} \cite{GL88} and is generally considered to be
the most general acceptable solution available. Counterexample $P_7$
however suggests that this solution may yield debatable results,
although to a lesser extent than Solutions~\ref{sol-least supported}
and~\ref{sol-unique supported}.

\sol{complete} (well-founded, positive after reduction, complete) is
essentially due to {\sc Van Gelder, Ross \& Schlipf} \cite{GRS88}. It
is the most general solution without undesirable properties. In {\sc
Bol \& Groote} \cite{BolG91}, where this solution has been adapted to
TSSs, an example in the area of concurrency is given (the modelling of
a priority operator in basic process algebra with abstraction) that
can be handled with \sol{complete}, but not with \sol{stratified}.
This example can neither be handled by \sol{sound}, showing that the
full generality of \sol{complete} can be useful in applications.

My presentation of \sol{complete} differs so much from the original
one \cite{GRS88,BolG91} that I gave it a new name. It is based on a
concept of provability incorporating the notion of {\em negation as
failure} of {\sc Clark} \cite{Cl78}. \th{reduction} establishes the
correspondence between my version and the one from
\cite{GRS88,BolG91}, whereas \th{3-valued} establishes the
correspondence with the work of {\sc Przymusinski} \cite{Prz90}.  I
think that my proof-theoretic characterization of \sol{complete}, and
to some extent also the one of \sol{stable}, can be useful in
applications, among others because it allows induction on proofs. The
following proposition on {\em transition equivalence} of TSSs for
instance follows immediately from the definitions given here, whereas
it would be nontrivial when starting from the original definitions. As
a matter of fact, I need this proposition in another paper, and the
search for it inspired me to write this one.

\begin{proposition}{equivalence}
Let $P$ and $P'$ be TSSs over the same signature, such that $P \vdash
\frac{N}{\alpha} \Leftrightarrow P' \vdash \frac{N}{\alpha}$ for any
closed action rule $\frac{N}{\alpha}$ with only negative antecedents. Then
\begin{itemize}\vspace{-1ex}
\item A transition relation $T$ is stable for $P$ iff it is stable for
$P'$. Hence $P$ is meaningful according to \sol{stable} iff $P'$ is,
and in that case they determine the same transition relation.\vspace{-1ex}
\item $P \vdash_{ws} \beta \Leftrightarrow P' \vdash_{ws} \beta$ for any
closed literal $\beta$. Hence $P$ is meaningful according to
\sol{complete} iff $P'$ is, and in that case they determine the same
transition relation.\vspace{-1ex}
\item  According to \sol{irrefutable} $P$ and $P'$ are meaningful and
determine the same transition relation.
\end{itemize}
\end{proposition}
Solutions~\ref{sol-scomplete} (complete with
support),~\ref{sol-sound} (sound with support),
and~\ref{sol-irrefutable} (irrefutable) may be new. The first two are
based on a notion of provability that is somewhat simpler to apply, and
only incorporates the notion of {\em negation as finite failure}
\cite{Cl78}. Moreover, \sol{scomplete} only yields unique supported
models, like \sol{strict} (and~\ref{sol-unique supported}).
\sol{irrefutable} appears to be the best way to associate a transition
relation to arbitrary TSSs. However, it has the disadvantage that it
sometimes yields unstable transition relations, and even unsupported
models. A good example from concurrency theory of an incomplete TSS is
Basic Process Algebra with a priority operator, unguarded recursion
and renaming, as defined in {\sc Groote} \cite{Gr93}. This TSS has no
supported models. \sol{irrefutable} does give a meaning to this TSS,
but it appears rather arbitrary and not very useful. In particularly,
recursively defined processes do no longer satisfy their defining
equation, which makes algebraic reasoning virtually impossible.  Also
the absence of a congruence theorem as demonstrated in Section
\ref{compositionality} is a bad property of this Solution. Hence
\sol{complete} (complete) remains the most general completely
acceptable answer to (\ref{quest}). In case 3-valued solutions are
allowed, this solution generalises to all transition system
specifications in the shape of the well-founded semantics.

\subsection*{Specifying transition relations}

This paper dealt with the problem of associating a transition relation
to a given TSS\@. A related problem is to find a good TSS to specify a
given transition relation. Here ``good'' could be something like
``finite'' or ``in ntyft/ntyxt format''. Without such a restriction
the transition relation itself can be used as TSS, regarding every
transition as a rule without premises. The problem can be further
parametrised by specifying the desired transition relation up to a given
notion of equivalence only. In this light the solutions of
Figure~\ref{solutions} can be compared also on their expressiveness,
i.e.\ {\em are there transition relations that can be specified by a
good TSS that is meaningful according to solution S, but not by one
that fits in solution $S'$?\/} This issue is left for future research.

\subsection*{Acknowledgments}
This paper benefited greatly from the insightful comments of Roland Bol.
Also thanks to the audience of the PAM seminar for useful feedback.

%\bibliography{/uf/rvg/lib/abbreviations,/uf/rvg/lib/dbase,/uf/rvg/lib/new}
\begin{thebibliography}{10}

\bibitem{AB94}
{\sc K.R. Apt \& R.~Bol} (1994):
\newblock {\em Logic programming and negation: A survey.}
\newblock {\sl Journal of Logic Programming \rm 19--20}, pp. 9--71.

\bibitem{BIM88}
{\sc B.~Bloom, S.~Istrail \& A.R. Meyer} (1988):
\newblock {\em Bisimulation can't be traced: Preliminary report.}
\newblock In {\sl Conference Record of the $15^{th}$ ACM Symposium on Principles of Programming Languages, {\rm San Diego, California}}, pp. 229--239.
\newblock Full version available as Technical Report 90-1150, Department of Computer Science, Cornell University, Ithaca, New York, August 1990. Accepted to appear in {\sl Journal of the ACM}.

\bibitem{BolG91}
{\sc R.N. Bol \& J.F. Groote} (1991):
\newblock {\em The meaning of negative premises in transition system specifications (extended abstract).}
\newblock In J.~Leach~Albert, B.~Monien \& M.~Rodr\'{\i}guez, editors: {\sl Proceedings $18^{th}$ ICALP, {\rm Madrid}}, {\sl \rm LNCS} 510, Springer-Verlag, pp. 481--494.
\newblock Full version appeared as Report CS-R9054, CWI, Amsterdam, 1990.

\bibitem{Cl78}
{\sc K.L. Clark} (1978):
\newblock {\em Negation as failure.}
\newblock In H.~Gallaire \& J.~Minker, editors: {\sl Logic and Databases}, Plenum Press, New York, pp. 293--322.

\bibitem{Fa91}
{\sc F.~Fages} (1991):
\newblock {\em A new fixpoint semantics for general logic programs compared with the well-founded and the stable model semantics.}
\newblock {\sl New Generation Computing \rm 9(4)}.

\bibitem{GRS88}
{\sc {A. van} Gelder, K.~Ross \& J.S. Schlipf} (1988):
\newblock {\em Unfounded sets and well--founded semantics for general logic programs.}
\newblock In {\sl Proceedings of the $7^{th}$ ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems}, pp. 221--230.
\newblock Alternatively see {\it The well-founded semantics for general logic programs}, JACM 38(3), pp. 620--650, 1991.

\bibitem{GL88}
{\sc M.~Gelfond \& V.~Lifschitz} (1988):
\newblock {\em The stable model semantics for logic programming.}
\newblock In R.~Kowalski \& K.~Bowen, editors: {\sl Proceedings $5^{th}$ International Conference on Logic Programming}, MIT Press, Cambridge, Massachusetts, pp. 1070--1080.

\bibitem{Gr93}
{\sc J.F. Groote} (1993):
\newblock {\em Transition system specifications with negative premises.}
\newblock {\sl Theoretical Computer Science} 118(2), pp. 263--299.

\bibitem{GrV92}
{\sc J.F. Groote \& F.W. Vaandrager} (1992):
\newblock {\em Structured operational semantics and bisimulation as a congruence.}
\newblock {\sl Information and Computation} 100(2), pp. 202--260.

\bibitem{Pl81}
{\sc G.D. Plotkin} (1981):
\newblock {\em A structural approach to operational semantics.}
\newblock Report DAIMI FN-19, Computer Science Department, Aarhus University.

\bibitem{Prz88}
{\sc T.C. Przymusinski} (1988):
\newblock {\em On the declarative semantics of deductive databases and logic programs.}
\newblock In Jack Minker, editor: {\sl Foundations of Deductive Databases and Logic Programming}, Morgan Kaufmann Publishers, Inc., Los Altos, California, pp. 193--216.

\bibitem{Prz90}
{\sc T.C. Przymusinski} (1990):
\newblock {\em The well-founded semantics coincides with the three-valued stable semantics.}
\newblock {\sl Fundamenta Informaticae} XIII(4), pp. 445--463.

\bibitem{Ver94}
{\sc C.~Verhoef} (1994):
\newblock {\em A congruence theorem for structured operational semantics with predicates and negative premises.}
\newblock In B.~Jonsson \& J.~Parrow, editors: {\sl Proceedings CONCUR 94, {\rm Uppsala, Sweden}}, {\sl \rm LNCS} 836, Springer-Verlag, pp. 433--448.

\end{thebibliography}
\end{document}
