\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
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% Theorem-like environments %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newtheorem{defi}{Definition}
\newtheorem{theo}{Theorem}
\newtheorem{prop}{Proposition}
\newtheorem{lemm}{Lemma}
\newtheorem{coro}{Corollary}
\newtheorem{solu}{Solution}
\newenvironment{definition}[1]{\begin{defi} \rm \label{df-#1} }{\end{defi}}
\newenvironment{theorem}[1]{\begin{theo} \rm \label{thm-#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{solution}[1]{\begin{solu} \rm \label{sol-#1} }{\end{solu}}
\newenvironment{proof}{\begin{trivlist} \item[\hspace{\labelsep}\bf Proof:]}{\hfill $\Box$\end{trivlist}}
\newenvironment{itemise}{\begin{list}{$\bullet$}{\leftmargin 18pt
\labelwidth\leftmargini\advance\labelwidth-\labelsep
\topsep 4pt \itemsep 2pt \parsep 2pt}}{\end{list}}
\newcommand{\df}[1]{Definition~\ref{df-#1}}
\newcommand{\thm}[1]{Theorem~\ref{thm-#1}}
\newcommand{\pr}[1]{Proposition~\ref{pr-#1}}
\newcommand{\lem}[1]{Lemma~\ref{lem-#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\makebox[0pt][l]{\footnotemark}\\ \ \\}
R.J. van Glabbeek\\
\footnotesize
Computer Science Department, Stanford University\\
Stanford, CA 94305-9045, USA.\\
{\tt rvg@cs.stanford.edu}
\end{center}
\footnotetext{
This a mild revision of Stanford report
STAN-CS-TN-95-16, with added emphasis on
3-valued interpretations.
An extended abstract appeared in {F.\ Meyer
auf der Heide \& B.\ Monien}, editors:
{\sl Automata, Languages and Programming,
Proc.\ 23$^{th}\!$ International Colloquium,
ICALP '96}, Paderborn, Germany, LNCS 1099,
Springer, 1996, pp.\ 502--513.\\
This work was supported by ONR under
grant number N00014-92-J-1974. The revision
was written while the author was employed at
the National ICT Australia, and at INRIA,
Sophia Antipolis, France.}
\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{\dl}[1]{\mbox{\rm I\hspace{-0.75mm}#1}} % openface letter
\newcommand{\IN}{\dl{N}} % natural numbers
\newcommand{\IT}{\mbox{\sf T\hspace{-5.5pt}T}} % openface T (terms)
\newcommand{\plat}[1]{\raisebox{0pt}[0pt][0pt]{$#1$}} % no vertical space
\newcommand{\rec}[1]{\plat{ % pair
\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{\pf}{\noindent {\bf Proof:\ }} % beginning of proof
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\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. Additionally, this paper contributes a proof theoretic
characterisation of the well-founded semantics for logic programs.}
\section{Transition system specifications \& Introduction}
In this paper $V$ and $A$ are two sets of {\em variables} and {\em
actions}. Many concepts that will appear are parameterised 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{itemise}
\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{itemise}
A term $c()$ is often abbreviated as $c$. A {\em
$\Sigma$-substitution} $\sigma$ is a partial function from $V$ to
$\IT(\Sigma)$. If $\sigma$ is a substitution and $S$ any syntactic
object (built from terms), 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$. $S$ is
said to be {\em closed} if it contains no variables. The set of closed
terms is denoted ${\sf T}(\Sigma)$.
\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$. 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$.\pagebreak[3]
A TSS is {\em standard} if its rules have no premises of the form
$t\gonotto{a}t'$, and {\em positive} if all premises 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 formalisation of {\sc Plotkin}'s {\em Structural Operational
Semantics (SOS)} \cite{Pl81} that is sufficiently general to cover
most 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{itemize}\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{itemize}
\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 {\sf T}(\Sigma) \times A
\times {\sf 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
{\sf T}(\Sigma)$. Write $T \models H$, for $H$ a set of closed literals, if
$T \models \alpha$ for all $\alpha \in H$.
Write $T \models p$, for $p$ a closed proof, if $T \models \alpha$ for
all literals $\alpha$ that appear as node-labels in $p$.
\end{definition}
The main purpose of a TSS $(\Sigma,R)$ is to specify a transition
relation over $\Sigma$.
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$ can be regarded as an example of a TSS that does not
specify a well-defined transition relation (under any plausible
definition of `specify').\footnote{All my examples $P_i$ consider
TSSs $(\Sigma,R)$ in which $\Sigma$ consists of the single constant
$c$ only.} 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,}\label{quest1}
\end{equation}\vspace{-5ex}
\begin{equation}
\mbox{\em and which transition relations do they specify?}\label{quest2}
\pagebreak[3]\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'$.
I will compare the 11 solutions on consistency and extension,
and evaluate them on their taste in determining which specifications
are meaningful and which are not.
A transition relation can be seen as a function
$T: {\sf T}(\Sigma) \times A \times {\sf T}(\Sigma)\rightarrow
\{\mbox{\sl present}, \mbox{\sl absent}\}$, telling which potential
transitions are present in $T$ and which are absent.
A {\em 3-valued transition relation}
$T: {\sf T}(\Sigma) \times A \times {\sf T}(\Sigma)\rightarrow
\{\mbox{\sl present}, \mbox{\sl undetermined}, \mbox{\sl absent}\}$
extends this concept by leaving the value of certain transitions undetermined.
Although there turns out to be no satisfactory way to associate a (2-valued)
transition relation to every TSS, I present two satisfactory methods
to associate a 3-valued transition relation to every TSS.
One of these is the {\em well-founded semantics} of {\sc Van Gelder,
Ross \& Schlipf} \cite{GRS88}; the other may be new. I contribute
proof theoretic characterisations of these 3-valued solutions.
The most general completely acceptable answer to (\ref{quest1}) when
insisting on 2-valued transition relations, is, in my opinion: the TSSs
whose well-founded semantics is 2-valued.
\subsection*{Logic programming}
The problems analysed in \cite{Gr93} in associating transition
relations to TSSs with negative premises had been encountered long
before in logic programming, and most of the solutions reviewed in
the present paper stem from logic programming as well. However, the proof
theoretic approach to Solutions~\ref{sol-complete} and I, as well as
Solutions~\ref{sol-scomplete},~\ref{sol-sound},~\ref{sol-irrefutable} and
II and some comparative observations, are, as far as I know, new here.
The connection with logic programming may be best understood by
introducing {\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)$. A PSS is now defined in
terms of literals in a same way as a TSS\@. A {\em proposition}
is a closed positive literal, and a {\em proposition relation} or
{\em closed theory} a set of propositions. The problem of associating
a proposition relation to a PSS is of a similar nature as associating
a transition relation to a TSS, and in fact all concepts and results
mentioned in this paper apply equally well to both situations.
If I would not consider TSSs involving literals of the form $t
\gonotto{a}$, a TSS would be a special case of a PSS, namely the case
where all predicates are binary, and it would
make sense to present the paper in terms of PSSs. The main reason for
not doing so is to do justice to the r\^ole of literals $t\gonotto{a}$
in denying literals of the form $t \goto{a} t'$. However, every TSS
can be encoded as a PSS and vice versa, in such a way that all concepts
of this paper are preserved under the translations.
In order to encode a PSS 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}).
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.
A logic program is just a PSS obeying some finiteness conditions.
Hence everything I say about TSSs applies to logic programming too.
Consequently, this paper can in part be regarded as an overview
of a topic within logic programming, but avoiding the logic
programming jargon. However, 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}.
\section{Model theoretic solutions}\label{model}
\subsection{2-Valued solutions}
\begin{solution}{positive}({\em Positive}).
A first and rather conservative answer to (\ref{quest1}) and (\ref{quest2})
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\/}) \cite{BIM88,BolG91}.
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
relation $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
${\sf 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,
\plat{\{c\goto{a}c\}} and \plat{\{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)}.\pagebreak[3]
\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, in the sense
that neither one extends the other. 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.
$$\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 it fails to assign a
meaning to the perfectly reasonable TSS $P_3$. Moreover, it can be
criticised for yielding unsupported transition relations, 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 priori, 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}{ws}({\em Well-supported}).\footnote{\label{Rutten}
The original version of this paper, which appeared as Stanford report
STAN-CS-TN-95-16, contained an incorrect definition of well-supportedness
(but leading to the same notion of a well-supported model). As observed by
Jan Rutten, Proposition 3 in that version, stating that
well-supported transition relations are supported, was false.
With the new \df{ws} this proposition becomes trivial and is therefore
omitted. The mistake had no other bad consequences.
% Besides small additions to the proofs of \pr{stability}, \thm{3-valued}
% and \pr{supported} there are no further differences between the two versions.
}
A transition relation $T$ is {\em well-supported} by a TSS $P$ if:
\begin{center}
$T \models t\goto{a}t' ~~\Leftrightarrow$ \begin{tabular}{l}there is a
closed proof $p$, with $T \models p$, of a\\ transition rule
$\frac{N}{t\goto{a}t'}$ without positive premises.
\end{tabular}
\end{center}
\end{definition}
Note that ``$\Leftarrow$'' is trivial, and a well-supported
transition relation is surely supported.\pagebreak[3]
My concept of well-supportedness can easily be seen to coincide with
the one of {\sc Fages} \cite{Fa91}. It is closely related to the
earlier concept of {\em stability}, developed by {\sc Gelfond \&
Lifschitz} \cite{GL88} in logic programming, and
adapted for TSSs by {\sc Bol \& Groote} \cite{BolG91}.
\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~$ there is a
set $N$ of closed negative literals with $P \vdash \frac{N}{t\goto{a}t'}$
and $T \models N$.
\end{center}
\end{definition}
\begin{proposition}{stability}
$T$ is stable for $P$ iff it is a well-supported model of $P$.
\end{proposition}
\begin{proof} ``if'': ``$\Rightarrow$'' follows immediately from the
well-support of $T$, and ``$\Leftarrow$'' follows from the soundness
of $T$ by a trivial induction on the length of proofs.
``only if'':
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 premises
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 premises with $P
\vdash \frac{N}{t\goto{a}t'}$ and $T \models N$. Hence $T \models t\goto{a}t'$.
That $T$ is well-supported now follows by a trivial induction on
the length of proofs, taking into account that a proof of a closed
transition rule can easily be turned into a closed proof.
\end{proof}
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.1 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$.
It 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
premises with $P \vdash \frac{N}{t\goto{a}t'}$ and $T_2 \models N$.
By (\ref{contrapositive}) one has $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
\plat{c\goto{b}c}.~ \plat{\{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 \plat{\{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
incomparable 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 favour 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 Section~\ref{proof theoretic}.
\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
relation $\{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}
\hspace{1in}
\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}$$
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$, as in $P_8$. This would rule out $P_7$.
Solutions that cater to this taste will be proposed in
Section~\ref{proof theoretic}.
\subsection{3-Valued solutions}
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 ${\sf T}(\Sigma)\times A \times {\sf T}(\Sigma)$ into the
the transitions that hold and those that don't, but a partition of
${\sf T}(\Sigma)\times A \times {\sf T}(\Sigma)$ into three sets: {\em
true}, {\em false} and {\em unknown}. Such a 3-valued interpretation
can be given as a set of closed binary $\Sigma$-literals, not
containing literals that deny each other. Here a literal is {\em
binary} if it has the form $t \goto{a} t'$ or $t \gonotto{a} t'$.
\begin{definition}{3-valued}({\em 3-Valued transition relation}).
Let $\Sigma$ be a signature. A {\em 3-valued transition relation}
over $\Sigma$ is a set $T$ of closed binary $\Sigma$-literals, not
containing literals that deny each other.
A closed literal $\alpha$ {\em holds} in $T$, notation $T \models
\alpha$, if $\alpha$ is binary and $\alpha \in T$ or $\alpha =
(t\gonotto{a})$ and $(t \gonotto{a} t')\in T$ for all $t'\in {\sf T}(\Sigma)$.
Write $T \models H$, for $H$ a set of closed literals, if
$T \models \alpha$ for all $\alpha \in H$.
Write $CT$ for the positive literals in $T$, the transitions that
{\em certainly} hold, and $PT$ for $\{t\goto{a}t' \mid\linebreak[3]
(t \gonotto{a} t') \not\in T\}$, the transitions that {\em possibly} hold.
Using this convention, a 3-valued transition relation $T$ can
alternatively be presented as a pair $\rec{CT,PT}$ of transition
relations as in \df{transition}, satisfying $CT \subseteq PT$. A
3-valued transition relation $\rec{CT,PT}$ is said to be {\em
2-valued} if $CT=PT$.
\end{definition}
In {\sc Przymusinski} \cite{Prz90}, of the concept of a stable
transition relation (or well-supported model) is generalised to
3-valued interpretations.
\begin{definition}{3-stable}({\em 3-Valued stability}).
A 3-valued transition relation $T$ is {\em stable} for a TSS $P$ if:
\begin{center}
$T \models t\goto{a}t' ~~\Leftrightarrow~$ there is a
set $N$ of closed negative literals with $P \vdash \frac{N}{t\goto{a}t'}$
and $T \models N$,\\
and $~~T \models t\gonotto{a}t' ~~\Leftrightarrow$ \begin{tabular}{l}
for each set $N$ of closed negative literals satisfying
$P \vdash \frac{N}{t\goto{a}t'}$,\\ one has
$T \models \alpha$ for a literal $\alpha$ denying a literal in $N$.
\end{tabular}
\end{center}
\end{definition}
By Definitions \ref{df-transition} and \ref{df-3-valued},
for positive literals $\alpha$ one has $T \models \alpha
\Leftrightarrow CT \models \alpha$ whereas for negative literals
$\alpha$ one has $T \models \alpha \Leftrightarrow PT \models \alpha$.
Hence \df{3-stable} can be reformulated as follows:
\begin{proposition}{3-stable}
A 3-valued transition relation $\rec{CT,PT}$ is {\em stable} for a TSS $P$ iff:
\begin{center}
$CT \models t\goto{a}t' ~~\Leftrightarrow~$ there is a
set $N$ of closed negative literals with $P \vdash \frac{N}{t\goto{a}t'}$
and $PT \models N$,\\
and $~~PT \models t\goto{a}t' ~~\Leftrightarrow~$ there is a
set $N$ of closed negative literals with $P \vdash \frac{N}{t\goto{a}t'}$
and $CT \models N$.
\end{center}
\end{proposition}
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).
With this in mind, \pr{3-stable} explains \df{3-stable} as a valid
generalisation of \df{stable}.
The definition in \cite{Prz90} can be shown to amount to the same concept.
A stable transition relation as in \df{stable} can be regarded as
a stable 3-valued transition relation $\rec{CT,PT}$ with $CT=PT$.
On 3-valued transition relations the inclusion relation $\subseteq$ is
called the {\em information ordering}; $T \subseteq T'$ holds when in
$T'$ the truth or falsity of more transitions is known. This is the
case iff $CT \subseteq CT'$ and $PT \supseteq 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}.
Assuming that $A=\{a,b\}$, the TSS $P_1$ has three 3-valued stable
transition relations, namely \plat{\{c \goto{a} c,~ c \gonotto{b} c\}},
\plat{\{c \goto{b} c,~ c \gonotto{a} c\}} and $\emptyset$. 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
semantics\/}) 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 other solutions, as it
does not provides 2-valued transition relations. However, 2-valued
transition relations can be obtained by restricting attention to those
TSSs for which the least 3-valued stable transition relation
$\rec{CT,PT}$ satisfies $CT=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 propose another 3-valued
answer to (\ref{quest1}) and (\ref{quest2}), based on a generalisation
of the notion of a supported model.
\begin{definition}{3-agrees}({\em 3-Valued supported model}).
A 3-valued transition relation $T$ is a {\em supported model} of a TSS $P$ if:
\begin{center}
$T \models t\goto{a}t' ~~\Leftrightarrow~$ there is a
closed substitution instance $\frac{H}{t\goto{a}t'}$ of a rule of $P$
with $T \models H$,\\
and $~~T \models t\gonotto{a}t' ~~\Leftrightarrow$ \begin{tabular}{l}
for each closed substitution instance $\frac{H}{t\goto{a}t'}$ of a
rule of $P$,\\ one has
$T \models \alpha$ for a literal $\alpha$ denying a literal in $H$.
\end{tabular}
\end{center}
\end{definition}
A supported model as in \df{agrees} can be regarded as a 3-valued
supported model that happens to be 2-valued. In the next section I
will show that every TSS admits an information-least 3-valued
supported model.
\begin{trivlist}\item[]{\bf 3-Valued Solution II}
({\em Least 3-valued supported model}).
Any TSS is meaningful. Its meaning is its information-least 3-valued
supported model.\pagebreak[3]
\end{trivlist}
Solutions I and II agree on the treatment of $P_1$, $P_2$, $P_3$,
$P_7$ and $P_8$. Assuming that $A=\{a,b\}$, the transition relation
associated to $P_1$ and $P_7$ is $\emptyset$, meaning that both
potential transitions are undetermined. The meaning of $P_2$ is
\plat{c\gonotto{b}c}, i.e.\ the $a$-transition is undetermined.
The meaning of $P_3$ and $P_8$ is \plat{\{c \gonotto{b} c,~ c\goto{a}c\}};
here both potential transitions are determined. According to Solution
I the meaning of $P_5$ is $\{c \gonotto{a} c,~ c\gonotto{b}c\}$
whereas Solution 2 yields $\{c \gonotto{b} c\}$, leaving the
$a$-transition undetermined. Likewise, Solution II associates the
empty transition relation to $P_4$, leaving both transitions
undetermined, whereas Solution I yields \plat{\{c \gonotto{b} c\}}.
\section{Proof theoretic solutions}\label{proof theoretic}
In this section I will propose solutions based on a generalisation of
the concept of a proof. Note that in a proof two kinds of steps are
allowed, itemised with ``{\bf --}'' in \df{proof}. The first step 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 the second step. 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, by Definitions~\ref{df-agrees}
and~\ref{df-stable}, a (2-valued) model $T$ of a TSS $P$ is supported iff
\vspace{-1ex}\begin{center}
$T \models t\gonotto{a}t' ~~\Leftarrow$ \begin{tabular}{l}
for each closed substitution instance $\frac{H}{t\goto{a}t'}$ of a
rule of $P$,\\ one has
$T \models \alpha$ for a literal $\alpha$ denying a literal in $H$.
\end{tabular}
\end{center}
and well-supported (or stable) iff
\begin{center}
$T \models t\gonotto{a}t' ~~\Leftarrow$ \begin{tabular}{l}
for each set $N$ of closed negative literals satisfying
$P \vdash \frac{N}{t\goto{a}t'}$,\\ one has
$T \models \alpha$ for a literal $\alpha$ denying a literal in $N$.
\end{tabular}
\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=(\Sigma,R)$ 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{itemize}\vspace{-1ex}
\item $\beta$ is positive and $\frac{K}{\beta}$ is a substitution
instance of a rule from $R$,
\item or $\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 premises.\vspace{-1ex}
\end{itemize}
\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=(\Sigma,R)$ 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{itemize}\vspace{-1ex}
\item $\beta$ is positive and $\frac{K}{\beta}$ is a substitution
instance of a rule from $R$,
\item or $\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}
\pagebreak[3]
\end{itemize}
\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. The last step from \df{wsp}
allows one to infer $t\gonotto{a}t'$ whenever it is manifestly
impossible to infer $t\goto{a}t'$ (because every conceivable proof of
$t\goto{a}t'$ involves a premise that has already been refuted), or
$t\gonotto{a}$ whenever for any term $t'$ it is manifestly impossible
to infer $t\goto{a}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}$. From here onwards, statements hold with
or without the text enclosed in square brackets. Also, a proof as in
\df{proof} will be referred to as a {\em positive} proof.
\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 premise.
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
definitions of $s$- and $ws$-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
premises. 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}
({\em Consistency, soundness and completeness\/}).
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 {\sf 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 {\sf 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. Moreover,
it provides a proof theoretic characterisation of these solutions.
\begin{theorem}{3-valued}
For any TSS $P$, the set of closed binary literals $[w]s$-provable
from $P$ constitutes a 3-valued [well-]supported model of $P$. It is
even the least one w.r.t.\ the information ordering.
\end{theorem}
\begin{proof} By \pr{consistency} the set $T$ of closed binary literals
$[w]s$-provable from $P$ constitutes a 3-valued transition relation.
Using \lem{standard}, it is straightforward to check that $T$
satisfies the required equations. It follows from the soundness of
$\vdash_{[w]s}$ w.r.t.\ $\models_{3[w]s}$ (\pr{soundness}) that $T$ 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 of $P$. Thus $\alpha$ certainly
holds in the least such model w.r.t.\ the information ordering, which
is the one of \thm{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, when insisting on 2-valued
solutions 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.
The 3-valued solutions I and II are two satisfactory methods to
associate a 3-valued transition relation to {\em any} TSS.
I have given both model theoretic and proof theoretic
characterisations of these solutions. In the remainder of this section
I continue the search for 2-valued solutions. In this context, in line
with question~(\ref{quest1}), I will call a TSS {\em meaningless} if
it has no satisfactory 2-valued interpretation.
\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
characterisation 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 premises 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
premise $\beta$ in $H$, and $P\vdash_x \gamma$ for no transition
$\gamma$ denying a negative premise 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 $p$ of a
rule $\frac{N}{t\goto{a}t'}$ with $N$ a set of closed negative
literals. For any literal $\alpha$ in $p$ one has
\plat{P \vdash_x \alpha}. If $\alpha$ is positive, this immediately
gives $\alpha \in T$. If $\alpha$ is negative, then, by the
consistency of $\vdash_x$, \plat{P \vdash_x \beta} for no closed
literal $\beta$ denying $\alpha$. This implies \plat{T \models \alpha},
and hence $T \models p$.
\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 a 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}$ and suggested 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 next proposition shows that the proof theoretic
solutions behave better in this respect.\pagebreak[3]
\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 2-valued generalisations of the
proof theoretic solutions. The first idea is to define the transition
relation 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 immediately 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 {\sf 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 relation $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 constitutes 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 premise \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'}, one has \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}$, one has $\exists v' \in {\sf 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 immediately from \pr{supported} that the set of
$x$-irrefutable transitions of an $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 {\sf 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 a 2-valued meaning to {\em all} transition
system specifications}
In this section I will associate a 2-valued transition relation to
arbitrary TSSs. As illustrated 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 any more transitions. Hence the
transition relation 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 it 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 stabilises gives the associated transition relation.
However, in general this solution yields more transitions then I would
like to see. The transition relation 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 preferring 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 transition 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
upper bound 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[3]
\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$ one has $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$ one has \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 one has
$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 upper bound 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
\thm{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:({\sf T}(\Sigma) \times A \times {\sf 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 {\sf 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
upper bound 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