\documentclass[11pt,a4paper]{article}
\usepackage{proofs}
\usepackage{html}
\usepackage{harvard}


% if .bbl is newly generated, URLs need to be brought
% into the form 
% \harvardurl{http://www.mpi-sb.mpg.de/\~{}hg/pca.html\#LICS94}

% hyperlinking
\newcommand{\cmd}[1]{\hyperref{\sat{#1}}{\sat{#1} (Section~}{)}{cmd-#1}}
\newcommand{\cmdp}[2]{\hyperref{\sat{#1(#2)}}{\sat{#1(#2)} (Section~}{)}{cmd-#1}}
\newcommand{\cmdptr}[3]{\hyperref{#3}{#3 (Section~}{)}{cmd-#1-#2}}
\newcommand{\link}[2]{\htmladdnormallink{#2}{#1}}
\newcommand{\hyref}[2]{\hyperref{#2}{#2 (Section~}{)}{#1}}
\newcommand{\example}[2]{\html{\link{../../examples/#1}{#2}}\latex{#2\footnote{File \sat{#1} in the examples directory of the \Sat\ distribution}}}

% Saturate text
\newcommand{\msat}[1]{\mbox{\sat{#1}}}
\newcommand{\sat}[1]{{\tt #1}}
\newcommand{\Saturate}{{\sf Saturate}}
\newcommand{\Sat}{\Saturate}


% math notation
\newcommand{\inferencepattern}[3]{\strut #1 \quad #2 \over \strut #3}
\newcommand{\inference}[2]{\strut\displaystyle {#1} \over \strut\displaystyle {#2}}
\newcommand{\equ}{\mathrel{\mbox{{\tt ==}}}}
\newcommand{\imp}{\mathrel{\mbox{\tt ->}}}
\newcommand{\implies}{\supset}

% latex2html bugs
\newcommand{\underscore}{\_}
\newcommand{\percent}{\%}
\newcommand{\dollar}{\$}

\sloppy

\newcommand{\ignore}[1]{}
\begin{document}
%\documenttitle{no title}
%\documenttoplevel{section}
%\sectionlevel{0}{f}{title}
%\htmlLabel{1}
\title{The Saturate System}
\author{Harald Ganzinger\\
Robert Nieuwenhuis\\
Pilar Nivela}
\maketitle

\begin{abstract}
The \Saturate\ system is an experimental theorem prover for first-order
logic, primarily based on saturation.
\Saturate\ uses techniques of ordered chaining for
arbitrary transitive relations, including orderings, equivalence relations
and congruences, and integrates CNF transformation lazily into saturation.
\end{abstract}
\newpage

%\sectionlevel{0}{f}{contents}
%\htmlLabel{2}
\tableofcontents
\newpage

\section{Installation}
%\htmlLabel{3}
Saturate runs under Quintus 3.2 (SunOS4.1, 5.3 and higher),
under SICStus 2.1 (patch levels \#9 or higher; SunOS 4.1 only)\footnote{This 
used to be the case up to version~2.4, but has not been verified for version 2.5.}
and SICStus 3.x (3.0: patch levels \#3 or higher; SunOS4.1, 5.3 and higher).

It also runs under SICStus 3.x (Linux and Windows).

\subsection{Copying the System}
%\htmlLabel{4}
You may obtain the system by ftp from ftp.mpi-sb.mpg.de
as compressed tar file \sat{pub/SATURATE/saturate.tar.gz} or,
in a web browser, by clicking  
\link{//www.mpi-sb.mpg.de/SATURATE/saturate.tar.gz}{this link}.

Then
untar \sat{saturate.tar} in some directory 
\sat{<saturate\underscore{}install\underscore{}dir>}
 which generates
a subdirectory \sat{saturate} containing the system
(in subdirectories called 
\sat{papers}, \sat{sources}, \sat{doc}, and \sat{examples}).
The documentation can be found in the subdirectory \sat{doc}
(manual in hypertext format (subdirectory \sat{Saturate}, file \sat{Saturate.html}) or as a
gzipped Postscript file \sat{Saturate.ps.gz}).

\subsection{Installing the System}
%\htmlLabel{5}
Take the following steps
\begin{itemize}
\item
\sat{cd <saturate\underscore{}install\underscore{}dir>/saturate/sources}
\item
Replace in the file \sat{sat.pl} the lines
\begin{verbatim}
        assert(saturate_directory( '/HG/local/provers/saturate' ) .
        davis_putnam( yes ).
\end{verbatim}
   by 
\begin{verbatim}
        saturate_directory( '<saturate_install_dir>/saturate' ) .
        davis_putnam( <yes/no> ).
\end{verbatim}
You may also want to adjust the configuration of the web browser to be used
for displaying the help files. With netscape (Unix) or explorer (Windows)
it should just work fine as is. Even if those settings are not correct
that's not a problem,
the Saturate system will function in any case. 

The flag for \sat{davis\underscore{}putnam} indicates as to whether the optional incremental
Davis-Putnam-like satisfiability checker should be included in the system.
The flag has no effect for Quintus- and SICStus 2.1-Prolog.
The module only works under SICStus 3.x.

For SICStus 3.x users
it is possible that on your computer system ``yes'' will produce errors due
to incompatibilities on the C-compiler and C-libraries level.
In that case change the default to ``no'' and run the generation
again. Saturate will function
without that module, too, but will perform much worse in medium to large
examples of near-propositional nature and in certain
knowledge representation applications.
If you want that module, you may obtain it via
\link{ftp://www.mpi-sb.mpg.de/pub/tools/CLPPB/clppb.html}{ftp}.
You will then have to re-compile them on your system,
{\bf using the same C-compiler that was used for installing SICStus 3.0}.
Then move the resulting
modules into directory \sat{<saturate\underscore{}install\underscore{}dir>/saturate/sources/CLPPB}
and say \sat{davis\underscore{}putnam( yes ).} before generating Saturate again.


\item
{\bf For SICStus Prolog users only: } You need to have patch level \#3
or higher for SICStus 3.0 and patch level \#8 or higher for SICStus 2.1
(patch level \#9 recommended). For later versions
of SICStus 3.x any patch level should be fine.
\begin{itemize}
\item
On SPARC architectures include
\begin{verbatim}
        :- prolog_flag(compiling,_,fastcode).
\end{verbatim}
      into your \sat{.sicstusrc} file (or execute that query on top level)
      before installing the system if you want native code generation
     (the preferred mode). 

\item
Include
\begin{verbatim}
        setenv SP_COMPRESS_SAVE 1
\end{verbatim}
     into your \sat{.cshrc} file to save space when saving Saturate.
\end{itemize}
\item
cd to the \sat{sources} subdirectory.

\item
Call Quintus Prolog or SICStus Prolog.

\item
Execute
\begin{verbatim}
        | ?- compile(sat), genSystem.
\end{verbatim}
(don't forget the dot at the end).
Then, on demand, enter the name of a file 
           to save the Saturate system on.
           Use that name on shell level to call Saturate lateron, or when restoring that state.

\item
Exit the Prolog system or start using Saturate right away.
\item
Don't remove the source files after system generation. Some of them will be
needed and linked dynamically at runtime.
\item
If you would like to check as to whether the system operates correctly,
execute

\begin{verbatim}
        | ?- cd('<saturate_install_dir>/saturate/examples'), 
             hgstuff:testsuite.
\end{verbatim}
As of November 2001 this runs for about 180 sec
under SICStus 3.x on a 600Mhz Pentium IIII.
The resulting behaviour should look like the one
that is documented in the log-file 
\sat{<saturate\underscore{}install\underscore{}dir>/saturate/testsuite.log*}.
\end{itemize}

\section{Overview}
%\htmlLabel{6}
The \Saturate\ system is an experimental automated theorem prover for 
first-order logic primarily based on saturation up to redundancy.
The theoretical basis of \Sat\ are 
rewrite techniques for transitive relations as described
in \cite{BachmairGanzinger-94-lics} and~\cite{BachmairGanzinger-95-mpii2-009}.
%\htmladdnormallink{LICS94 paper}{../papers/abstracts.html#BG-LICS94}.
Clausal normal form transformation is integrated into \Sat\ 
in an attempt to keep the logical structure, in particular
quantifiers and equivalences, visible.
The system is written in Prolog and runs under Quintus and SICStus.

\Sat\ is a cooperation project between UPC~Barcelona and MPI~Informatik
within the ESPRIT
Basic Research Working Groups CCL and
\htmladdnormallink{CCL~II}{http://ps-www.dfki.uni-sb.de/ccl/}.

The main focus of the system is on
\begin{itemize}
        \item 
the efficient treatment of \hyref{sec-trans}{transitive relations} by term 
\hyref{sec-chain}{rewrite techniques}, and on
        \item
the global restriction of the search space in saturation-based theorem proving by 
applying techniques for detecting \hyref{sec-redundancy}{redundancy} of clauses and inferences.
\end{itemize}
Moreover, \Sat\ 
\begin{itemize}
        \item
integrates
a set of inference rules
that are derived from the \hyref{sec-sk}{sequent calculus} into saturation so as to 
not prematurely eliminate quaintifiers and other
logical structure;
        \item
provides
methods for translating \hyref{sec-modal-logic}{modal logics} into first-order logic
based on various semantic embeddings into Kripke structures, and
        \item
supports \hyref{sec-ac}{AC-operators} by providing AC-unification, AC-matching,
AC-extensions of equalities,
and AC-compatible orderings as a basis for a future
integration of specific algebraic methods for theories such as abelian groups,
rings and fields.
\end{itemize}

There are three basic kinds of problems for which Saturate can be used:
\begin{itemize}
        \item 
for \hyref{sec-tp}{refutational theorem proving}
        \item
for the finite \hyref{sec-sat}{saturation of a consistent theory}, and
        \item
for finding \hyref{sec-locality}{complexity bounds} for decidable theories.
\end{itemize}

\html{This manual is also available as a \link{../Saturate.ps.gz}{Postscript file}.}

\subsection{Applications}
%\htmlLabel{7}

\subsubsection{Refutational Theorem Proving}
%\htmlLabel{8}
\label{sec-tp}
In refutational theorem proving we prove $F$ by deriving a contradiction
from $\neg F$. 
For simple cases, calling \cmd{prove}
will do the job.
The formula
$\neg F$ will be saturated up to redundancy by
a refutationally complete \hyref{sec-inferences}{inference system}
until a contradiction is found.
Alternatively, if $\neg F$ can be finitely saturated 
without producing a contradiction, $F$ is not provable.
Applying simplification and techniques for detecting redundancy,
\Sat\ attempts to gain better control of its forward computation
mode.
The forward inferences (resolution, chaining, superposition)
are restricted by ordering constraints and selection functions
such that only maximal or selected atoms or terms need
to be resolved or chained.

\ignore{\Sat\ does not transform $\neg F$ as a whole into an equivalent (with respect to satisfiablity)
matrix of standard clauses. Only those subformulas of the goal
that might become subject to forward computation inferences eventually
are expanded. This strategy allows to keep the logical structure
visible as much as possible. In particular, equivalences will
not be expanded unless the maximal atom or term needs to be exposed
for participation in resolution or chaining inferences.
In other words, \Sat\ computes with general clauses in
which literals are general (signed) first-order formulas.}

When one uses \Sat\ for refutational theorem proving,
only a modest amount of simplification should
be applied. If \Sat\  is at all able to find a proof,
if will often also find a proof in its automatic mode which
in particular includes an automatic setting of the ordering and selection
function. Sometimes a more clever setting of meta-logical directives
is required. A more detailed discussion of this issue is
provided \hyref{sec-flags-tp}{below}.

\subsubsection{Saturation of a Theory}
%\htmlLabel{9}
\label{sec-sat}
When we are interested in the finite saturation of a theory,
we don't expect to find a contradiction and hence want to
limit forward computation as much as possible.
In that case certain meta-logical directives, including the reduction ordering,
have to be set \hyref{sec-flags-sat}{manually}.

\subsubsection{Establishing Complexity Bounds}
%\htmlLabel{10}
\label{sec-locality}
This is a new application of saturation up to redundancy
by ordered resolution. For a finitely presented saturated theory,
depending on the ordering that was used for saturation,
we may obtain a complexity result for the entailment problem for
that theory. We call a theory local if it can be saturated up to redundancy
for an ordering with a specific complexity bound.
The setting of directives for establishing locality is discussed
\hyref{sec-flags-locality}{below}. Specific orderings must be used
and the full power with respect to redundancy proofs has to be requested.

\subsection{Inference System}
%\htmlLabel{11}
\label{sec-inferences}
\Sat\ applies two kinds of inferences, chaining inferences
based on known transitivity properties for binary relations
(including the transitivity of logical implication and equivalence),
and certain rules derived from sequent calculus for eliminating
logical symbols and quantifiers.

\subsubsection{Chaining Inferences}
%\htmlLabel{12}
\label{sec-chain}
Transitivity of a relation $R$, say, is dealt with by \emph{chaining} inferences of the form
$$
\inference{C,\  R(s,t) \quad\quad D,\ R(u,v)}
        {(C,\ D,\ R(s,v))\rho}
$$
with $\rho$ the mgu of $t$ and $u$.
Its dual, \emph{negative chaining}, is an inference of the form
$$
       \inferencepattern{C ,\  R(t,s)}{D ,\  \neg R(u,v)}{( C ,\  D ,\  \neg R(s,v) )\rho}
$$
or
$$
       \inferencepattern{C ,\  R(s,t)}{D ,\  \neg R(v,u)}{( C ,\  D ,\  \neg R(v,s) )\rho}
$$
with $\rho$ the mgu of $t$ and $u$.

As can be seen, paramodulation is
a special case of chaining.
In fact, equality is a binary relation
for which we have transitivity, reflexivity, symmetry and monotonicity
for all function and predicate symbols. Monotonicity or
anti-monotonicity axioms can be dealt with by chaining into subterms.
At present, subterm chaining is only implemented for partial congruences
including equality.
Resolution, too, is a special case of negative chaining
$$
       \inferencepattern{C ,\  A\equ\top}{D ,\  \neg (B\equ\top)}
                                {C\sigma ,\  D\sigma ,\  \neg (\top\equ\top)}
$$
between two equivalences $A\equ\top$ and $B\equ\top$ 
with subsequent deletion of the trivial equation $\top\equ\top$,
where
$\rho$ is the mgu of $A$ and $B$.

\Sat\ attempts to automatically
recognize relevant \hyref{sec-trans}{properties of binary relations},
including transitivity, in order to find an appropriate tailoring
of the chaining inference system.

The chaining inference system in \Sat\ 
is parameterized by essentially two meta-logical parameters:
\hyref{sec-orderings}{orderings} and \hyref{sec-selection}{selection function}.
Ordering and selection function induce
essential \hyref{sec-restrictions}{restrictions}
that one may place on inferences without
compromising refutational completeness.

\paragraph{Reduction Orderings.}
%\htmlLabel{13}
\label{sec-orderings}
When we speak of an ordering we mean a total (or completable)
reduction ordering. A reduction ordering is a well-founded ordering on ground terms
that is compatible with contexts and is total or can be extended to
a total such ordering.
Reduction orderings are the basis for terminating computations
by term rewriting. \Sat\ provides several \cmdptr{add}{orddecl}{classes of reduction
orderings}, including the lexicographic path ordering
and its AC-variant.
Orderings specify an orientation of binary atoms, in particular equalities,
indicating the preferred direction when replacing equals by equals.
A ordering $\succ$ also expresses preferences and directions
of search when attempting to construct models
for disjunctions: $A\vee B$ is to be viewed as $\neg B \to A$, if $A\succ B$,
and this links ordered resolution to negation as failure in logic programming.

\paragraph{Selection Functions.}
%\htmlLabel{14}
\label{sec-selection}
With the concept of selection functions one exploits the don't-care
nondeterminism that comes with negative literals in clauses:
To refute $A_1,\ldots,A_k\to$ requires to refute each of the $A_i$,
but the order in which this is done is irrelevant.
To eliminate redundancy that might arise from this nondeterminism,
selection functions that select negative literals can be defined
with the command~\cmd{sass}.

\paragraph{Restrictions for Inferences.}
%\htmlLabel{15}
\label{sec-restrictions}
Given an ordering and a selection function,
the chaining inferences are restricted
in that an inference is performed only between maximal or selected
atoms in a clause, and only if the middle term through which
is being chained is maximal (with respect to the given reduction
ordering $\succ$) in both atoms:
\begin{enumerate}
        \item 
$s\sigma \not\succeq t\sigma$,
        \item
$v\sigma \not\succeq u\sigma$,
        \item
the participating $R$-atoms must either be maximal or
selected within the repsective premises; and
        \item
the positive (that is, first) premise of an inference
contains no selected literals.
\end{enumerate}
Hence, selection not only indicates which subgoal to solve
in a clause. It also serves to block clauses from
becoming a positive premise in an inference.

Unrestricted chaining amounts to hyperresolution
with the transitivity axiom and creates a large search space.
This is illustrated by the two examples \example{hres15}{\sat{HRES15}}
and \example{oc15}{\sat{OC15}} which both consist of
the facts $i > i+1$, for $i=1,\ldots,14$, together with the transitivity axiom
for $>$. In the case of \sat{HRES15}, the ordering restrictions are turned
off. To saturate \sat{HRES15} takes about 100~times longer than
running the example in the unsual ordered chaining mode \sat{OC15}.

\subsubsection{Sequent Calculus}
%\htmlLabel{16}
\label{sec-sk}
Sequent calculus is usually viewed as being applied in a backward manner
to construct proofs for sequents $S$ by eliminating the logical symbols in $S$
one after the other.
For this mode of application cuts are not required,
although their use might lead to much smaller proofs.

Saturation-based theorem proving can be viewed as a mechanism for
establishing
$$
S_1,\ldots,S_k \vdash {\to}
$$
that is, for deriving the empty sequent $\to$ from an inconsistent
set $S_1,\ldots,S_k$ of sequents, by the \emph{forward application}
of the rules of the sequent calculus.
In that context, the cut rule becomes the main working horse,
and its combination with the substitution rule,
which is an inverse form of certain quantifier rules,
is called resolution.
That view of resolution allows one to integrate 
clausal normalform transformation into resolution and chaining
in a lazy manner.

The (multi-conclusion) rules that we apply in a forward manner
are the inverse forms
$$
\inference{\Gamma \to F\wedge G,\Delta }{\Gamma \to F,\Delta \quad \Gamma \to G,\Delta }
$$
of invertible rules such as
$$
\inferencepattern{\Gamma \to F,\Delta }{\Gamma \to G,\Delta }{\Gamma \to F\wedge G,\Delta }
$$
for the logical connectives.
(The expanded formula $F\wedge G$ of the inference is called its \emph{main formula}
below.)
The quantifier rules that we use are
$$
\inference{\Gamma \to \forall x. F(x),\ \Delta }{\Gamma \to F(X),\ \Delta }
$$
where $X$ is a fresh free variable, and
$$
\inference{\Gamma \to \exists x. F(x,\vec Y),\ \Delta }{\Gamma \to F(f(\vec Y),\vec Y),\ \Delta }
$$
where $f$ is a new (Skolem) function symbol and $\vec Y$ are the free variables
in $F$. (The ``left`` versions of the rules are analoguous.)

Note that these rules are simplifications in that the premise can be deleted
once its conclusions have been derived.
In fact, the conclusions imply their premise and are smaller in an appropriate extension
of the atom ordering to general first-order formulas.
However, we apply rules only if the main formula is either maximal in the sequent
or negative and selected. In other words, the rules obey the same restrictions with
respect to ordering and selection functions as the chaining inferences.

Sequents in \Sat\ may contain equalities $F\equ G$ between formulas
$F$ and $G$, semantically denoting equivalence of $F$ and $G$,
which are dealt with specifically.
Only if a maximal one of the two sides $F$ and $G$ is non-atomic,
the equality is expanded according to
$$
\inference{\Gamma \to F\equ G,\Delta }{\Gamma,F\to G,\Delta \quad \Gamma,G \to F,\Delta }
$$
In case $F\succ G$ and $F$ is atomic, i.e., of the form $p(s_1,\ldots,s_k)$,
with a predicate symbol $p$ and terms $s_i$,
the equivalence is \emph{not} eliminated from the sequent.
Non-eliminated equivalences are subject to ordering-restricted forms of chaining
inferences such as
$$
\inferencepattern{\Gamma \to A\equ F,\Delta }{\Lambda \to B\equ G,\Pi }{(\Gamma,\Lambda \to F\equ G,\Delta,\Pi)\sigma }
$$
with $\sigma$ the mgu of the atoms $A$ and $B$, provided
$F\sigma\not\succeq A\sigma$, $G\sigma\not\succeq A\sigma$,
no premise contains a selected literal, and both equivalences are maximal
in their respective premises.

Orientable equivalences $A\equ F$ in which the maximal side $A$ is atomic
are also used for simplification in that everywhere occurences of $A\sigma$ will be replaced
by $F\sigma$.
This handling of equivalences is especially useful for definition hierarchies
if the definitions are to be applied in a goal to replace derived predicates
and if one does not want to automatically
infer
lemmas for the new predicates.
An example how proofs in \Sat\ look like when
simplification with equivalences are intertwined with chaining
is a simple \example{set}{set theory} with
an \example{set.ord}{ordering} under which definitions are expanded out.

\subsubsection{Modal Logics}
%\htmlLabel{17}
\label{sec-modal-logic}
\Sat\ includes a \link{../translate.html}{translator} for modal logic into first-order logic
by semantic embedding.
The translator will be implicitly invoked when calling \cmd{prove} for a modal logic
formula.

\subsubsection{Specific Treatment of Binary Relations}
%\htmlLabel{18}
\label{sec-trans}
\Sat\ attempts to automatically
recognize certain properties of binary relations 
and then specializes the chaining-based inference rules accordingly.
Also, the simplification module will know about these properties.
The system recognizes and treats in a specific manner
\begin{description}
        \item[transitivity]
or, more generally, certain collections of composition laws of the form
$$
 p(X,Y), q(Y,Z) \to r(X,Z), 
$$
for binary relations $p$, $q$, and $r$;

        \item[totality laws]
of the form 
$$
\to p(X,Y),\ p(Y,X),\ X=Y \ ;
$$

        \item[reflexivity and irreflexivity laws]
of the form
$$
\to p(X,X)
$$
or
$$
p(X,X) \to \ ;
$$

        \item[monotonicity laws]
of the form 
$$
p(X,Y) \to p(f(\ldots X \ldots),f(\ldots Y \ldots)) \ ;
$$

        \item[anti-monotonicity laws]
of the form
$$
p(X,Y) \to p(f(\ldots Y \ldots),f(\ldots X \ldots)) \ ;
$$

        \item[symmetry laws]
of the form 
$$
        \to p(X,Y) ,\  p(Y,X) \ ;
$$

        \item[density laws]
of the form
$$
        p(X,Y) \to p(X,d(X,Y)) \wedge p(d(X,Y),Y)
$$
(written as two clauses); and

        \item[laws about the absense of endpoints]
of the form
$$
\to p(X,f(X))
$$
or
$$
\to  p(g(X),X).
$$
\end{description}
Interesting types of binary relations with such properties include
equivalences, equality (congruences) and orderings.

\subsection{Redundancy}
%\htmlLabel{19}
\label{sec-redundancy}
Proving the redundancy of clauses and inferences
is indispensible for pruning the search space non-locally.
With the techniques that are implemented in \Sat\ we
can effectively compute saturated sets of clauses 
in more cases than with most other saturation-based provers.
Finite, saturated sets of clauses not containing the empty clause are provably
consistent, and more efficient refutational theorem proving strategies 
become available for proving consequences of such theories.
Sometimes they provide the basis for a decision 
procedure for the respective theory.
 
Redundany is closely tied to the term ordering that one uses.
In short, a clause is redundant in a particular state of 
the saturation process if it is logically entailed by smaller clauses
that exist in that state.
For inferences a similar criterion applies: if the conclusion is entailed by
clauses smaller than the negative premise it is redundant
(see~\cite{BachmairGanzinger-94-jlc}.
Ordering constraints as they arise
from inferences can be kept with the conclusion
and inherited to its descendants as described in~\cite{NieuwenhuisRubio-92-esop} and~\cite{NieuwenhuisRubio-92-cade}.
This technique not only provides for a more precise checking
of the constraints, it also increases the power
in checking for redundancy of inferences.

\subsection{Associative-Commutative Operators}
%\htmlLabel{20}
\label{sec-ac}
\Sat\ provides two ways of dealing with AC-operators.
One is 
by the standard methods of ordered rewriting.
This is in many cases not good enough. On problems in which AC-symbols play a
central role and interact non-trivially with some transitive relation,
ordered rewriting as provided in \Sat\ may perform
poorly, although AC-specific redundancy proof techniques (e.g., convergence
tests for critical pairs by case analysis and constrained rewriting) are provided.
A non-trivial case in which ordered rewriting together with these techniques
works well is an exampe due to \example{overbeek3}{Overbeek}.
In that example, saturation not only finds the required commutativity property
of multiplication but moreover terminates with a ground convergent
system for the commutative ring in question.

Alternatively, and this is the standard setting, \Sat\ will apply 
AC-superposition and AC-chaining based on AC-unification,
extended clauses and AC-orderings
as explained in~\cite{BachmairGanzinger-95-ctrs}.
AC-unification can be very expensive.
Most of the time, additional algebraic structure e.g., cancellativity, group or ring structure,
is present and, hence, should be exploited.
This is one of the directions into which future research concentrates on.

\section{Getting started}
%\htmlLabel{21}
The system is implemented in Prolog and expects commands in the syntactic form
of Prolog goals. 
The list of all the Saturate commands
is given \hyperref{here}{in Section~}{}{sec-commands}.
For proving $\Phi$ in automatic mode
enter $\msat{prove}(\Phi)$.
The syntax of formulas is explained \hyperref{here}{in Section~}{}{sec-syntax}.

In semi-automatic mode, or for saturating a consistent theory,
the typical \hyref{sec-interaction}{interaction cycle} with Saturate consists of reading a set of 
(general) clauses,
issuing commands to define the reduction ordering, 
inference system, redundancy checks, system messages and
profiling flags, and, finally, starting the saturation process.
If saturation terminates or is interrupted (by typing control-C),
proofs of generated clauses can be inspected.
Saturated systems of clauses can be filed out for later uses as modules
of more complex theories.

\section{Formula Syntax}
%\htmlLabel{22}
\label{sec-syntax}
First-order formulas
are built in from
\begin{itemize}
        \item Prolog variables, denoting free or bound variables,
        \item logical symbols \sat{=},
\sat{\~{}}, \sat{and}, \sat{or}, \sat{<=>}, \sat{=>},
\sat{all}, and \sat{exists}, denoting equality, negation, conjunction, disjunction,
equivalence, implication, universal and existential quantification, respectively, and
        \item Prolog terms for denoting terms and atoms.
\end{itemize}
General or standard first-order \emph{clauses} are written as
sequents $\Gamma \imp \Delta$ of multisets $\Gamma$ (the \emph{antecedent})
and $\Delta$ (the \emph{succedent})
of general literals.
The elements in $\Gamma$ and $\Delta$ are separated by ``,''.
A \emph{general literal}
is either a first-order formulas $F$ or, somewhat unusually, 
an \emph{equality $F\equ G$ between two 
formulas $F$ and $G$}.
As usual, comma on the right side of $\imp$ denotes disjunction, and comma left denotes
conjunction. Equality on the level of formulas denotes logical equivalence.
This is an example of a sequent consisting of a single (and positive)
equality:
\begin{verbatim}
   -> eq(X,Y) == all(Z,member(Z,X) <=> member(Z,Y))
\end{verbatim}
Free variables in a clause, such as $X$ and $Y$ above,
are implicitly universally quantified.
Here is an example of a (Horn) sequent
\begin{verbatim}
   exists(X,f(X)), exists(X,g(X)) ->
         all(X,(f(X) => h(X)) and all(X,g(X)=>j(X)))
                             == 
         all(X,all(Y,f(X) and g(Y) => h(X) and j(Y)))
\end{verbatim}
with a 2-element antecedent and an $\equ$-equality
as succedent.
We have an equivalence \sat{==} on the level of sequents 
(in addition to the equivalence \sat{<=>} on the level of formulas)
as an explicit
indication for our computing with certain such equivalences
by rewriting.
A detailed definition of the syntax is given \hyref{sec-cf-syntax}{below}.

%\sectionlevel{1}{f}{^}
%\htmlLabel{23}

%\sectionlevel{2}{f}{^}
%\htmlLabel{24}

\paragraph{Context-free Syntax for Clauses.}
%\htmlLabel{25}
\label{sec-cf-syntax}
Nonterminals in the subsequent grammar are the symbols that begin with
an upper-case letter. 

\begin{verbatim}
Clause  : ProperClause
        | goal ProperClause
        
ProperClause : Antecedent -> Succedent.  -- sequent notation
             | Succedent <- Antecedent.  -- reverse sequents
             | Succedent.                -- positive disjunction
             | axiom( [ AntecedentL, SuccedentL, Constraint ] ).
                                         -- clauses with initial constraints
             | Literals.                 -- Otter-like notation
                
Antecedent : Multiset
Succedent  : []                          -- empty succedent
           | Multiset
Multiset   : Formula ``,'' Multiset | Formula

AntecedentL, SuccedentL: List(Formula)

Literals : Literal OrSymbol Literals
         | Literal

Literal  : Formula                       -- positive literal
         | - Formula                     -- negative literal

OrSymbol : ``;'' | ``|''
        

Formula  : Form
         | Form == Form                  -- equivalence
Form     : all(Variable,Form) 
         | exists(Variable,Form)
         | Form Op Form   
         | ~ Form   
         | Atom
Op       : and | or | => | <=> 

Atom     : Eq 
         | NonEqAtom

Eq       : Term=Term                       -- term equation
         | NonEqAtom                 
NonEqAtom: p(Term,...,Term)    where p is a predicate symbol


Constraint: list( Conjuncts )              -- interpreted as a dnf
Conjunct  : [ List(Ineq) , List(Eq) ]
Ineq      : Term > Term | Term >= Term 

Term      : Prolog term
Variable  : Prolog variable
List(X)   : Prolog list with elements of type X
\end{verbatim}
In addition, the usual Prolog operator precedences apply, plus the following precedences
\begin{verbatim}
        :- op(920,yfx,[and]).
        :- op(930,yfx,[or]).
        :- op(950,xfx,[<=>]).
        :- op(950,xfy,[=>]).
        :- op(900,fy,[~,dia,box]).
        :- op(910,yfx,[::]).
        :- op(910,xfx,[^^]).
\end{verbatim}
(The symbols \sat{dia}, \sat{box}, \sat{::}, and \sat{\^{}}\sat{\^{}}
are used for denoting \hyref{sec-modal-logic}{modal logic operators}
in connection with \cmd{translate}.)

Clauses
may have ordering and equality constraints attached.
(In constraints only term equations are admitted.)
In that case a clause represents all the ground instances
which satisfy the constraint. The constraints are
interpreted over
the selected reduction ordering.
The ordering is selected by 
an optional \cmdptr{add}{orddecl}{ordering declaration}.
The constraints mainly serve to reduce the search space
for the saturation process and to delay immediate constraint
solving upon inference computation. If initial input clauses
have constraints refutational theorem proving might be incomplete.

Distinguishing goal clauses (prefix \sat{goal})
from theory clauses may help in finding proofs faster.
Inferences in which at least one premise
is derived from a goal clause are selected with higher priority
(without violating fairness, however).

There is one important side condition that we make but don't check:
\sat{[]} and \sat{[{\underscore}|{\underscore}]}
should not be used as function or predicate symbols.
Also, certain symbols, in particular ``not'' and ``:'', that
have a meaning on the level of atoms or goals in Prolog programs
should not be used. \emph{Very} strange thing may happen, otherwise.

\section{The Interaction Cycle}
%\htmlLabel{26}
\label{sec-interaction}

\subsection{Reading Clauses}
%\htmlLabel{27}
The commands \cmd{in} 
or \cmd{add}
read files containing clauses and meta-logical directives.
We support structured theories, the separation between logical and
meta-logical items and the use of pre-saturated theory modules.
The clauses in the database can have different origins.
 The command \cmd{l} displays the current
saturation status of the current theory.

\subsection{Selecting the Inference System}
%\htmlLabel{28}
Before starting a saturation, the user defines the 
various parameters of the saturation process.
All commands that set some system parameter start with the prefix \sat{sa}
for ``set active ... ''.
The system comes with default settings that should be fine for initial experimentation.
Parameter settings are also predefined specifically for each example directory
(cf. \cmd{cd}) and may be included in problem definitions
(cf. \cmd{in}).

The inference system is set 
 with  the commands \cmd{sair} and 
\cmd{saes}
The inference system is further parameterized by a selection strategy for
negative literals. This strategy is (re-)defined with the
command \cmd{sass}.

\subsection{Selecting Ordering and Selection Function}
%\htmlLabel{29}
Orderings are defined with \cmdptr{add}{orddecl}{ordering declarations}
in a file or, interactively, with the \cmd{prec} command.

\subsection{Selecting the redundancy proof techniques}
%\htmlLabel{30}
 This is done with the command \cmd{sarp}.
 Redundancy proofs allow to
\begin{itemize}
        \item 
simplify clauses, including
        \begin{itemize}
        \item 
simplification by (contextual) reduction (demodulation),
        \item
simplification by totality resolution,
        \item
condensement,
        \item
applying specific propositional techniques to sets of ground clauses, and
        \item
simplification by applying ``noncritical'' tableau expansions;
        \end{itemize}
\item
delete redundant clauses by
        \begin{itemize}
        \item
tautology detection,
        \item
subsumption,
        \item
case analysis over all possible orderings of variables, and
        \item
clausal rewriting.
        \end{itemize}
\end{itemize}
More information on these techniques is contained in
\cite{BachmairGanzinger-94-jlc}
and a paper by
\link{../papers/abstracts.html#NN-PAPER}{Nivela and Nieuwenhuis}.\latex{\footnote{This paper is provided with the \Sat\ distribution in the \sat{papers} subdirectory.}}

\subsection{Selecting the output information}
%\htmlLabel{31}
The command \cmd{sams}  allows to control the 
output information that is presented to the user during a saturation proccess.

\subsection{Selecting timing points}
%\htmlLabel{32}
 The command \cmd{satp} allows to profile execution times for the main
saturation modules.

\subsection{Saturating a system}
%\htmlLabel{33}
The command \cmd{sat} saturates the current data base.
When the saturation is finished, the the final set of axioms is displayed,
together with the proof, if the empty clause was generated.
Saturation can be forced to terminate with a
partially saturated system by providing an upper bound on clause generation.

\subsection{Saving (partially) saturated set}
%\htmlLabel{34}
The command \cmd{out}
dumps the current theory in its current saturation state onto
a specified file. Under that name the theory may be included
as a module into other theories. In that case, any subsequent saturation
for the enriched thepry will not compute any inferences between theory
module clauses. That is incomplete in case the module was not fully
saturated at the tome when it was dumped.

\subsection{Proof Printing}
%\htmlLabel{35}
   The command \cmd{rp} displays the proof of the empty clause.
   The proof for every other clause with number $N$ in the data base can be obtained
   by the command $\msat{rp}(N)$.

\section{Saturate Commands}
%\htmlLabel{36}
\label{sec-commands}

\subsection{\sat{add}: Adding Input}
%\htmlLabel{37}
\label{cmd-add}
$$
\msat{add}(I),\ \msat{addsrc}(I)
$$
read input file(s) specified by $I$
and adds their contents to the current theory.

Input files define a first-order theory
given in the form of general clauses.
Input files may also specify a reduction ordering 
and other meta-logical directives that
serve to guide the saturation process.
Before reading the details
of this section, you may want to look at a few
\cmdptr{add}{examples}{examples} of input files first.

\Saturate\ (from version 2.4 onwards)
also accepts input files in Otter format or in TPTP format
(with \sat{include} declarations and \sat{input-clause} facts).
From version~2.5 onwards clauses may consist of
\emph{general literals} which are arbitrary, signed first-order formulas,
possibly with quantifiers.

More precisely, input files consist of sequences of 
\hyref{sec-syntax}{clauses}, together with optional
\begin{itemize}
\item
\hyref{cmd-add-use}{use declarations}
\item
\hyref{cmd-add-preddecl}{predicate declarations}
\item
\hyref{cmd-add-orddecl}{ordering declarations}
\item
\hyref{cmd-add-precdecl}{precedence declarations}
\item
\hyref{cmd-add-out}{outputs from \cmd{out} commands}
\item
\hyref{cmd-add-flags}{flag settings}
\item
\hyref{cmd-add-options}{option settings.}
\end{itemize}
Clauses, or theories and problems, rather, 
may also be specified in the form of DFG-Syntax. For an example see
\example{pell24}{\sat{Pelletier 24}} in DFG-notation.

Following the conventions for Prolog terms,
each item must be terminated by a dot ``.'' .
Terms and lists of items are to be written in Prolog notation.
Comments are written as in Prolog, that is, a single line of comment
is indicated by a leading ``\percent'' character. Other comments are
included in ``/*'' and ``*/'' brackets.

We suggest that meta-logical directives 
be kept separate from theory presentations.
How to achieve such separation is described \hyref{cmd-add-separation}{below}.

\subsubsection{Use Declarations}
%\htmlLabel{38}
\label{cmd-add-use}
Use declarations are of the form \sat{use($F$)},
where $F$ is an atom denoting a theory to be included.
The meaning of that declaration is equivalent to 
the execution of the command \sat{add($F$)}.

\subsubsection{Predicate Declarations}
%\htmlLabel{39}
\label{cmd-add-preddecl}
Predicates that occur in axioms may (but need not) be declared.
Only one predicates declaration is allowed in a file.
$$
        \msat{predicates(list(PredicateSymbols)).}
$$
In addition, 
if $R1$ is a binary predicate,
by writing
$$
        \msat{reflexive\underscore{}closure($R1$,$R2$)}.
$$
one declares $R2$ to be the reflexive closure of $R1$.
An explicit declaration of the reflexive closure is a shorthand
for writing 
explicitly axioms of the form

\begin{eqnarray*}
R1(X,Y) & \imp & R2(X,Y). \\
R2(X,Y)  & \imp  & R1(X,Y),\ X=Y.
\end{eqnarray*}

\subsubsection{Ordering Declarations}
%\htmlLabel{40}
\label{cmd-add-orddecl}
By an optional declaration of the
form
$$
        \msat{ordering($Ord$)}.
$$
one specifies the (kind of the) termination ordering to
be used for ordered inferences and for redundancy proofs. 
$Ord$ may be either 
\begin{itemize}
        \item 
\sat{lpo},
for the lexicographic path ordering which is
the default setting, or 
        \item
\sat{aclpo} for the AC-lexicographic path ordering which is
the default setting when AC-operators are present,
        \item
\sat{sto} for a precedence-based
subterm ordering, or
        \item
\sat{poly} for (linear) polynomial interpretations\footnote{Only with the SICStus 3.0 version
of \Sat\ .}
\end{itemize}
The \sat{sto} ordering is the union of the subterm ordering
with inequations $s=f(\ldots) > t=g(\ldots t_i \ldots)$
such that any of the $t_i$
are subterms of $s$ and $f > g$ in the precedence.
The atom ordering 
is a certain lexicographic extension of
this term ordering.
$sto$ is useful, probably, only in the non-equational case
when one tries to prove locality of an inference system,
cf. \link{http://www.mpi-sb.mpg.de/~hg/papers/conferences/LICS96.ps.gz}{ocality and saturation}.

\subsubsection{Precedence Declarations}
%\htmlLabel{41}
\label{cmd-add-precdecl}
All orderings that one may select require a
complete precedence of function and predicate symbols.
This precedence may be partially or completely defined by the user.
Partial precedences will be completed automatically by the system.

The optional declaration of the
form
$$
        \msat{top\underscore{}predicates\underscore{}precedence(list(PredicateSymbols)).}
$$
lists all the predicates (in deceasing precedence)
that are considered to be greater
than any function symbol (including those that occur in subsequent
enrichments of this theory) and greater than any other predicate symbol.
(In previous versions of Saturate the term \sat{first\underscore{}predicate\underscore{}precedence} was used.)
The declaration
$$
        \msat{precedence(list(FunctionAndPredicateSymbols)).}
$$
specifies the possibly partial precedence of the \emph{non-top}
predicate and function symbols
in decreasing order.
There is a pre-defined constant \sat{'\dollar{}min'} which is smaller than any other symbol.
\sat{'\dollar{}min'} may occur in clauses but must not occur in the precedence
declaration. We have examples in which saturation is much faster
if the smallest constant is employed
(e.g., modal logic \example{modal-logic/kd45}{KD45}).

Each theory module may have separate [top predicates] precedence declarations
associated with it in which the symbols of the module are related to
each other. When combining modules by importing them into
another module, the union of the precedences must be non-circular.
In particular it is not allowed to declare a predicate as a ``top predicate''
in one module and at the same time include it in a precedence declaration
for non-top symbols in another module.
Precedence declarations
in a module which imports one or several modules must be consistent with
the declarations in the module(s).

The automatic completion of the precedence seems to work well in most cases
for predicate symbols. For function symbols that occur in equations
some rather simple pragmatic assumptions are made. In particular, the system
attemps to define the precedence such that equations are oriented from left
to right.

\subsubsection{Reading Outputs from \sat{out}}
%\htmlLabel{42}
\label{cmd-add-out}
        In this case, saturated sets of clauses are recognized as such, and corresponding 
        inferences will not be recomputed.

\subsubsection{Calls to Flag Settings}
%\htmlLabel{43}
\label{cmd-add-flags}
Calls to flag settings are of the form
$$
        \msat{:- flag($S$).}
$$
        where 
\begin{verbatim}
     flag    : sair | saes | saci | sass | sarp |sams | satp 
 \end{verbatim}
The setting $S$ is flag-specific and explained
for the respective \cmd{sa}{${<}\msat{xx}{>}$ command,

        Before reading a file, flags are set to the defaults as given
        by the defaults file in the current directory. If no such file
        exists it is created with a certain standard set of flag settings.
        If flag settings should not be reset to their defaults, use
        \sat{inc($F$)} rather than \sat{in($F$)}.

\subsubsection{Options Settings}
%\htmlLabel{44}
\label{cmd-add-options}
Option settings are of the form
$$
        \msat{:- option(list(O)).}
$$
        where
\begin{verbatim}
   O : term_size_weight | term_var_weight | term_var_weight_gt_small |
       normal_term_weight | increment(N) | var_depth(N) |
       special_relations(on) | special_relations(off) |
       ac(on) | ac(off) |
       memo_constraints(on) | memo_constraints(off)
\end{verbatim}
        The weight options set the weight function for terms and clauses
        which is used for inference selection. 
\begin{description}
\item[\sat{term\underscore{}size\underscore{}weight}]: 
\begin{quotation}
weight = number of nodes in a term
\end{quotation}
\item[\sat{term\underscore{}var\underscore{}weight}]
\begin{quotation}
 weight = weighted product of term size, term depth
                        and number of different variables
\end{quotation}

\item[\sat{term\underscore{}var\underscore{}weight\underscore{}gt\underscore{}small}]
 similar, except that ground terms
                        are made very small

\item[\sat{normal\underscore{}term\underscore{}weight}] (default) 
 \begin{quotation}
weight = weighted product of term size
                        and depth
\end{quotation}


\item[\sat{increment($N$)}]
 Inferences are computed from clauses up to a certain
                weight. If no proof is found, the bound is increased by
                $N$. Defaults:
                $N = 15$ for \sat{term\underscore{}size\underscore{}weight}, \sat{normal\underscore{}term\underscore{}weight},
                $N = 30$, otherwise.    

\item[\sat{var\underscore{}depth(N)}]
 Clauses are preprocessed into rules in an order that also
depends on the number of different variables occuring in it.
If this number exceeds $N$ (default value is 3), processing of the clause
is delayed.

\item[\sat{special\underscore{}relations($S$)}]
 $S=\msat{on}$ turns on the special treatment of
                transitive relations by chaining inferences; default.
                In this mode, transitivity, reflexivity, irreflexivity
                totality, density and no endpoint axioms are treated
                specifically. Saturate recognizes these properties
                automatically, provided they are not hidden, i.e.,
                follow in a non-trivial way from other properties.
                Actually Saturate should be more clever in recognizing
                these properties.

                $S=\msat{off}$: transitive relations are treated as any other
                predicate. 
                This option should be specified textually before
                any axioms for the respective predicates.
                This option essentially reduces the inference system
                to ordered resolution. It should be used when Saturate is
                applied in order to prove the <\link{sec-locality}{locality} of a Horn theory.


\item[\sat{ac(S)}]
  $S=\sat{on}$ (default) results in employing AC-superposition
based on AC-unification and extended rules for AC symbols. 

                $S=\msat{off}$ results in the treatment of AC-symbols by ordered rewriting.This option
                must textually preceed any AC laws.
\item[\sat{memo\underscore{}constraints(S)}]
  $S=\msat{on}$ switches memoization for ordering constraints on.
                This is the recommended setting for cases in which big
                ordering constraints are generated. This is the case in
                particular when clausal rewriting is turned on.

                $S=\msat{off}$ (default): no memoization

\end{description}

\sat{option/1} may also be called interactively.

\subsubsection{Examples}
%\htmlLabel{45}
\label{cmd-add-examples}
\html{
\begin{itemize}
        \item 
\example{g}{group theory}
        item
\example{g.ord}{an ordering file} for group theory
        \item
\example{bledsoe/ivt}{intermediate value theorem}
        \item
\example{bledsoe/ivt.ord}{an ordering file} for the ivt
        \item
\example{bledsoe/ivtth}{intermediate value theorem} based on ...
        \item
... a theory of 
\example{bledsoe/continuity}{continuous functions},
based on a theory of ...
        \item
... \example{bledsoe/dto}{dense total orderings.}
        \item
\example{LocalTheories/congHO}{congruence closure}
        \item
... and an ordering and 
\example{LocalTheories/congHO.ord}{directives} file
for proving subterm locality of congruence closure
\end{itemize}
For more examples browse the \sat{\example{}{examples}} directory.}
\latex{For examples browse the \sat{examples} directory of the \Sat\ distribution.}}

\subsubsection{Separating Logic and Meta-Logical Directives}
%\htmlLabel{46}
\label{cmd-add-separation}
We suggest (but do not strictly require)
that ordering declarations and other meta-logical directives 
be kept separate from theory presentations.
In the \sat{add} and \sat{addsrc} commands
$I$ must be an atom $F$, or a pair
\sat{[$FO,F$]} of atoms, representing one or two file names,
respectively. 
In the second form of the command, $FO$ is supposed to specify
the name of the file containing the meta-logical directives,
while $F$ is supposed to denote the file containing the theory.
When using the first form of the command, the system checks for the presence
of a file named \sat{$F$.ord}.
If a file by that name exists, it is assumed that it contains
relevant meta-logical information associated with $F$.
In that case, \sat{in($F$)} is equivalent to
\sat{in([$F$.ord,$F$])}.

Theories may exist in different presentations. In particular it is
possible to dump a (partially) saturated theory module
to a file and read it back in
later (cf. \cmd{out}~command). 
In that case inferences will not be (re-)computed if 
each premise belongs to the (same) theory module. 
For fully saturated theories such a linear strategy is complete.
For partially completed theories it may be incomplete but nevertheless be
be useful as a strategy.
It is assumed that files with names of the form \sat{$F$.o}
are dumped, partially saturated theory modules. 
If a file by that name exists, \sat{in($F$)} will
read \sat{$F$.o} rather than $F$ itself.
In cases where this default behaviour is not wanted, \sat{addsrc($F$)}
should be used, which is otherwise equivalent to \sat{in($F$)}.

\subsection{\sat{cd}}
%\htmlLabel{47}
\label{cmd-cd}
$$
\msat{cd($D$)}
$$

Changes current working directory to $D$, that is,
$D$ becomes the working directory for any subsequent input and output. 

The default settings for flags for this directory become the
current flag settings and the
active defaults for subsequent changes (sa?? commands).
If the directory does not contain a
defaults specification it will be created
in some predefined way and stored
in a file (named \sat{defaults}) in that directory.
Changes to these defaults can be made subsequently by the
\sat{set active ... } commands together with the
\sat{save active ...} commands.

$D$
must be a Prolog atom denoting the directory. 
Sorry, no abbreviations allowed. 
Write single quotes `` ' '' around $D$, if $D$ contains delimiters 
such as `` . '' or `` / ''  such as in \sat{cd('/HG/usr/hg/saturate/examples').}

\subsection{\sat{cl}: Clearing the Database}
%\htmlLabel{48}
\label{cmd-cl}
Clears the data base.
This is done automatically when calling \cmd{in}.

\subsection{Flag Settings}
%\htmlLabel{49}
\label{cmd-sa}
The flag setting commands are named $\msat{sa}{<}xx{>}$,
for ``Set Active $xx$'' where $xx$ is a two-letter identifier for 
a flag.
The commands can either be called without a parameter for an
interactive setting of flags, or with a single parameter
$S$ which is a list of options for that flag.
Calls to \sat{sa}-commands with parameter
may also appear in \cmdptr{add}{flags}{input files}.
Options are given by natural numbers. Their
meaning is flag-specific and is described below.
If the list is prefixed by a ``\sat{+}'', the listed options
are added to the set of current options for the flag. If the list
is prefixed by a ``\sat{-}'' they are deleted.

All flags have a default setting that is determined by
a file named \sat{defaults} in the current directory.
\Sat\ will generate such a defaults file upon
changing into a directory with \cmd{cd} where there is no
defaults file yet.
The defaults file can be changed into user-specified defaults
with the family of \cmd{sv} commands.

\subsubsection{\sat{saci}: Settings for Constraint Inheritance}
%\htmlLabel{50}
\label{cmd-saci}
$$
\msat{saci}
$$
specify the setting of the constraint Inheritance strategy.
The (pairwise exclusive) options $O$ for constraint inheritance are
\begin{description}
\item[$O=1$:]
no constraint inheritance but complete immediate checking (default),
\item[$O=2$:]
hereditary ordering constraint,
\item[$O=3$:]
hereditary equality constraint: basic strategies.
\end{description}

With option 1 one gets a complete checking of ordering constraints
with each inference. 

With option 2, ordering constaints are inherited from the premises
to the conclusion of an inference, enriched by the ordering constraint
for that inference.
In this case ordering constraints may become prohibitively large.
Constraints are only inherited for non-unit clauses.
No constraint weakening is performed.
That is,
even when $C$ subsumes $D$ but the constraint of $D$
does not imply the constraint of $C$, $D$ will not be deleted.
An alternative would be to delete $D$, and at the same time
weaken the constraint for $C$ such that the weaker constraint
is implied.

Option 3 is incompletely implemented and should not be used
at present. 

If all options are turned off by calling \sat{saci([])}
clauses are
preoriented once and for all, and inferences are computed with
maximal literals and terms according to this preorientation.
This corresponds to checking ordering constraints before 
the unfier is applied. If big clauses are produced during
saturation, solving
ordering constraints may be prohibitively expensive and 
\sat{saci([])} might be a good choice.

\subsubsection{\sat{saes}: Settings for Eager Simplification}
%\htmlLabel{51}
\label{cmd-saes}
$$
\msat{saes}
$$
The \sat{saes}-flag specifies
the list of simplification rules $S$ that are 
to be applied eagerly on each clause
so as to ensure refutational completeness of a certain inference
system. At present we have only one such inference,
called ``variable elimination', and denoted by $S=1$, which should 
usually be turned on.

Variable elimination for orderings in \Sat\ is explained in~\cite{BachmairGanzinger-94-cade}.
Variable elimination also includes splitting of variable-disjoint parts of clauses
or variable-disjoint sides of equations.

\subsubsection{\sat{sair}: Settings for Inference Rules}
%\htmlLabel{52}
\label{cmd-sair}
$$
\msat{sair}
$$
This flag lists the set of inference rules $R$
that are to be applied fairly to persisting clauses.
 
The rules are identified by numbers as follows:
\begin{description}
\item[$R=1$:]
 reflexivity resolution
\item[$R=2$:]
right superposition and chaining
\item[$R=3$:]
left superposition and negative chaining
\item[$R=4$:]
factoring
\item[$R=5$:]
ordered resolution
\item[$R=6$:]
 transitivity resolution
\item[$R=7$:]
tableau expansion
\end{description}

The inference system consisting of all theses rules
is refutationally complete
In the case of dense orderings, one
 additionally needs to switch on variable elimination for refutational
 completeness, cf. command \cmd{saes}.
The default setting is determined by the current theory
and assures that sufficiently many inference rules are turned on.
Transitivity resolution is only needed for specific cases
of transitive relations.

 It is a good strategy (with respect to time efficiency) to set active inferences
 according to the problem at hand; for instance, for a purely equational problem
 only inference 3 (right superposition) is needed.

The inference system can be further instantiated with strategies for
\begin{enumerate}
\item
constraint inheritance: command \cmd{saci}
\item
selecting negative literals: command \cmd{sass}, and
\item
eager simplifications: command \cmd{saes}.
\end{enumerate}

For a description of these inferences we refer to our
\hyref{sec-inferences}{overview} and to~\cite{BachmairGanzinger-95-mpii2-009}.

\subsubsection{\sat{sams}: Messages}
%\htmlLabel{53}
\label{cmd-sams}
$$
\msat{sams}
$$
settings for the printing of MeSsages during saturation.
Find out about the flags interactively by calling \sat{sams}
without parameters.

\subsubsection{\sat{sarp}: Selecting Redundancy Proof Techniques}
%\htmlLabel{54}
\label{cmd-sarp}
$$
\msat{sarp}
$$
specifies the set of
techniques for Redundancy Proofs and for simplification.

These methods are currently
implemented and associated with these options $P$:
\begin{description}
\item[$P=1$:]
tautology elimination
\item[$P=2$:]
forward subsumption
\item[$P=3$:]
backward subsumption
\item[$P=4$:]
condensement
\item[$P=5$:]
propositional reasoning for ground clauses
\item[$P=6$:]
forward simplification by reduction
\item[$P=7$:]
backward simplification by reduction
\item[$P=8$:]
redundancy tests by case analysis (forward)
\item[$P=9$:]
redundancy tests by case analysis (backward)
\item[$P=10$:]
redundancy tests by clausal rewriting (forward)
\item[$P=12$:]
totality resolution
\item[$P=13$:]
extensionality resolution
\item[$P=14$:]
minimal level of reduction
\item[$P=15$:]
maximal level of reduction
\end{description}

If $P=15$ is set,
reduction is \emph{recursive rewriting} of ``maximal strength''
where most clauses and their contrapositives
are considered as conditional rewrite rules.
Reduction
also includes \emph{convergence tests} for inequalities in clauses 
with respect to the current set of positive unit inequalities.
This setting can be very expensive.
With $P=14$, only unit clauses are used for reduction
which usually is much faster.
If neither option is present, an intermediate level of reduction strength
is assumed (default setting).

Subsumption always includes a particular form of contextual reduction,
also called \emph{resolution subsumption}.
 Consider a resolution inference
$$
      \inferencepattern{C,A}{D,B}{D}
$$
 in the case when $A\sigma = \neg B$ and $C\sigma\subseteq D$. 
 Here the conclusion subsumes the second premise which can
 then be deleted. As to whether such an inference is possible
 is detected by a subsumption-like algorithm. This is why
 it has been included into subsumption so as to not duplicate
 work. Reductions of this form are extremely useful in many
 examples.

Propositional reasoning for ground clauses refers to an integration
of an incremental Davis-Putnam-like procedure for testing satisfiablity
of propositional clauses contributed by 
\link{ftp://www.mpi-sb.mpg.de/pub/tools/CLPPB/clppb.html}{Peter Barth}.
The procedure is part of his CLP(PB)-system and is operational
only in the SICStus 3.0 version of \Sat\.
Refutational completeness with this method switched on is
guaranteed only for ordered strategies without selection
as invoked through \cmdp{saci}{[]}.

\emph{Totality resolution} eliminates, in the case of total 
 relations $p$, all negative occurrences of $p$ by swapping them to
 the other side of the sequent. This option, by contrast to using the totality
 axiom lazily, is generally recommended for total orderings,
 in particular when combined with a positive strategy (\cmdp{sass}{[2]}).

\emph{Extensionality resolution} is a simplification related to the presence
of an extensionality axiom for equality or some other transitive relation.
It is somewhat experimental in nature.

Case analysis and
clausal rewriting are described in more detail
in paper by \link{../papers/abstracts.html\#NN-PAPER}{Nivela and Nieuwenhuis}.
Case analysis is useful for theories with AC-operators that
are to be dealt with by ordered rewriting  with \sat{option(ac(off))}.
Clausal rewriting should be turned on for non-trivial consistent theories that
one wants to saturate finitely.
For refutational theorem proving it should be turned off
as it is very expensive.

\subsubsection{\sat{sass}: Choosing a Selection Strategy}
%\htmlLabel{55}
\label{cmd-sass}
$$
\msat{sass}
$$
specifying the Selection  Strategy.
Selection
has a similar meaning as in SLD-resolution.
Selection is, in addition to the reduction ordering, the second main
parameter to the chaining and paramodulation inference systems.

One may choose from 4 alternatives.
\sat{sass([])} turns selection off, resulting in a fully ordered strategy.
\sat{sass([$F$])} specifies one of three selection strategies:
\begin{description}
\item[$F=1$:] (default)
automatic selection of a maximal literal in non-reductive clauses
\item[$F=2$:]
automatic selection of a small literal in non-positive clauses
 \item[$F=3$:]
user guided literal selection
\end{description}

Option $F=3$ is the one where the user is asked interactively for
each non-positive clause to select a negative literal for
chaining and superposition.

 In option $F=1$ which is fully automatic, no negative literal is selected 
 if the clause has a positive literal which is strictly greater than
 all negative literals.
 Otherwise one, usually maximal, negative literal is selected.

 Option $F=2$ always selects a (if possible non-maximal) literal in any 
 non-positive clause. This results in a positive strategy.

 The system indicates, by printing an asterix ``*'', those clauses for which a literal
 has been selected. The selected literal is listed first in
 the antecedent.

 Option $F=1$ sounds like applying usual ordering constraints to
 inferences. It is different in that we now perform all negative
 chainings into the selected literal, even in cases where the substituted
 literal (after applying the unifier of the inference) is not maximal.
 What we gain is that we never need to chain \emph{from} that clause.
 Moreover the ordering constraints are simpler and hence faster
 to check.

 This strategy seems to work better than the fully ordered strategy
 most of the time. Highly recommended in cases where clauses are
 too long to admit full checking of ordering constraints.

\sat{sass} has been called \sat{sama} in earlier versions
of \Sat{}.

\subsubsection{\sat{satp}: Timing}
%\htmlLabel{56}
\label{cmd-satp}
$$
\msat{satp}
$$
Show/Set the Active Timing Points $T$ for profiling.

Profiling can measure times for
\begin{description}
\item[$T=1$:]
inference computation
\item[$T=2$:]
forward simplification and redundancy tests
\item[$T=3$:]
backward simplification and redundancy tests
\item[$T=4$:]
constraint solving
\item[$T=5$:]
clause preprocessing
\item[$T=6$:]
rewriting.
\end{description}
Can be quite expensive.

\subsubsection{\sat{sv}: Saving Default Flag Settings}
%\htmlLabel{57}
\label{cmd-sv}
$$
\msat{sv${<}xx{>}$d}
$$
SaVe the setting for flag 
$xx \in \{\msat{ci},\msat{es},\msat{ir},\msat{ma},\msat{rp},\msat{tp}\}$ as default
into the \sat{defaults} file in the current directory.

\subsection{\sat{help}}
%\htmlLabel{58}
\label{cmd-help}
$$
\msat{help}
$$
informs an already running
web browser, or calls the web browser that has been specified upon
installation, for accessing this manual.

\subsection{\sat{in}, \sat{insrc}: Reading Input Files}
%\htmlLabel{59}
\label{cmd-in}
$$
\msat{in}(I), \msat{insrc}(I)
$$
Reads input file(s) specified by $I$.
$I$ must be an atom $F$, or a pair
\msat{[$FO$,$F$]} of atoms, specifying one or two file names,
respectively,
and adds them to the {\bf empty} theory.
Except for the fact that the database is cleared before
reading, the meaning is the same as for 
\cmdp{add}{$I$} and 
$\msat{addsrc}(I)$, respectively.

\subsection{\sat{l}: Listing }
%\htmlLabel{60}
\label{cmd-l}
Lists the contents of the database.
In that listing \emph{new clauses} and \emph{persisting clauses}, sometimes
also called \emph{rules},
are distinguished. Rules are clauses that have been preprocessed
by the system. The distinction is reminiscent of that between equations
and (oriented) rewrite rules.

\subsection{\sat{lprec}: Listing of the Precedence}
%\htmlLabel{61}
\label{cmd-lprec}
Lists the current precedence.

\subsection{\sat{out}: Dumping Theories to Files}
%\htmlLabel{62}
\label{cmd-out}
$$
\msat{out($F$)}
$$
Saves the current theory in its current perhaps only partially
saturated form, including the ordering definition, into file $F$.
The saved file can be used as a theory module in
\sat{in} and \sat{add} commands as well as in \sat{use}
directives, cf.
\cmd{add}.
If the module is part of a theory that is to be saturated,
no inferences will be computed in which all premises
are clauses of the theory module.

{\bf Warning:} even if the theory is not fully saturated upon saving,
later re-uses of the theory might not consider all inferences
between theory clauses.

\subsection{\sat{prec}: Precedence Definition}
%\htmlLabel{63}
\label{cmd-prec}
$$
\msat{prec}
$$
ask for a file $f$ for reading \cmdptr{add}{precdecl}{predecence declarations}.
For $f=\msat{user}$ the predecence declarations may be typed in interactively,
terminated by \sat{\^{}D}.

\subsection{\sat{prove}: Theorem Proving}
%\htmlLabel{64}
\label{cmd-prove}
$$
\msat{prove($F$)}
$$
invokes a theorem proving process for $F$ by negating $F$ and saturating
$\neg F$.
The general form of \sat{prove} is
$$
\msat{prove($F,L,M,O$)}
$$
for proving $F$ in logic $L$ with translation option $M$ and \Sat\ options
$O$. $L$ and $M$ are as for the function \cmd{translate}.
$O$ is a list of \cmd{sa} flag settings or \cmdptr{add}{options}{option settings}.

\subsection{\sat{rp}: Displaying Proofs}
%\htmlLabel{65}
\label{cmd-rp}
$$
\msat{rp,\ rp($N$)}
$$
Displays the proof of clause $N$.
If no argument is provided, the proof of the empty clause
is printed. Fails, if the specified clause does not exist (anymore).

\subsection{\sat{sat}: Starting Saturation}
%\htmlLabel{66}
\label{cmd-sat}
$$
\msat{sat, sat($N$)}
$$
This starts the saturation of the set of clauses/rules in the database
according to the chosen strategy. In case a number $N$ is 
provided, saturation stops after $N$ non-redundant
clauses have been generated.

Strategies are defined by calling
the \cmd{sa}{${<}\msat{xx}{>}$} commands for
setting the various parameters.
If no settings are provided explicitly, the directory-specific
default settings as contained in the local \sat{defaults}
file are assumed.

\subsection{\sat{translate}: Translating Modal Logic Formulas}
%\htmlLabel{67}
\label{cmd-translate}
$$
\msat{translate}
$$
invokes the \link{../translate.html}{translation} of a given modal logic formula into 
first-order logic by means of various semantic embedding techniques that one may choose
from. The results from \sat{translate} may be used as an input to \sat{make\underscore{}file}
for creating saturate input files for the background theory of a logic and/or for a problem.

\section{Heuristics for the Definition of Meta-Logical Directives}
%\htmlLabel{68}

\subsection{General}
%\htmlLabel{69}
There are two essential ways in which a user can
influence the saturation strategy: orderings and selection.
The orderings that are available in \Sat\ have been described
\cmdptr{add}{orddecl}{above}.
For the precedence-based orderings,
it is difficult to provide generally useful heuristics for setting
up the precedence. In any case the ordering should be such that
smaller terms and atoms are closer to a canonical form that we want
to approximate. That implies that derived symbols usually should
get a higher precedence than the symbols they are derived from.
Constants are usually minimal. Often predicates should be
maximal and \cmdptr{add}{precdecl}{top predicates}, 
in particular when their definitions are to be expanded out
such as in certain formulations of \example{set}{set theory}.
Sometimes it is helpful when Skolem functions
have a high precedence. For Skolem functions introduced by the system,
they are given a precedence higher than any user function.
Generated Skolem functions are ordered according to generation order:
later symbols (corresponding to inner quantifiers) are smaller 
than symbols generated earlier. 
That is, by choosing the ordering of the variables in a quantifier prefix,
a user can take influence on the ordering of the corresponding
Skolem functions. An example where this is crucial
is a certain lemma for the verification of \example{hoare/qs2}{quick sort}.
Equations in input formulas should be written in the way that one
wants them to be ordered. These heuristics are applied 
when \Sat\ computes or completes precedences automatically.

While the ordering essentially guides rewriting and search,
the selection strategies specify how negative literals should be treated.
The available strategies are explained with the \cmd{sass} command.
Again it is hard to say which strategy to apply in general.
With the ordering-guided strategies
\sat{sass([])} and \sat{sass([1])} simplification by recursive (contextual) rewriting
seems to have a better effect. Actually, only clauses in which
no negative literal is selected may become a potential simplifier
at present. For clauses with a selected negative literal we only
check as to whether they subsume (or subsume-reduce) some other clause.

Apart from these two pricipal ways of taking influence on search
and simplification, one may choose the way how ordering constraints
are handled (\cmd{saci} command). 
One needs to find the right balance between precision
and the fraction of runtime allocated for constraint solving.
Constraint solving for the \sat{lpo} is NP-complete, and the present implementation
clearly shows that. For the future we would like to improve our
implementation by providing better heuristics for constraint simplification.
The best choice usually is \sat{saci([1])}.
Some examples run much better with constraint inheritance \sat{saci([2])},
e.g., this formulation
of the theorem of the sum of two continuous
functions being \example{bledsoe/jar3}{continuous}.
Constraint inheritance might be crucial for the finite saturation of a consistent theory.

Finally, we have a number of \cmdptr{add}{flags}{flags} and
\cmdptr{add}{options}{options} that one may set
in addition.
These, among others, affect the selection of inferences according
to certain complexity measures on terms and clauses.
Setting them one way or another is hacking, and
nothing general can be said about it.

\subsection{Settings for Refutational Theorem Proving}
%\htmlLabel{70}
\label{sec-flags-tp}
For refutational theorem proving,
we have to find the right balance between forward computation
(search) and simplification. A modest amount of simplification should
be applied. A refutationally complete inference system is usually wanted.
We get this automatically with the default settings of the system.
We either call \cmd{prove}
or else read a set of clauses (command \cmd{in}) containing
the theory and the negation of the theorem to be proved,
and then enter \cmd{sat} to invoke
saturation.
We recommend to use the lexicographic path ordering (default
ordering) for refutational theorem proving. Then the definition
of an ordering reduces to defining the precedences between the
symbols (cf. \cmd{in}).

\subsection{Saturation of a Theory}
%\htmlLabel{71}
\label{sec-flags-sat}
When we are interested in the finite saturation of a theory,
we don't expect to find a contradiction and hence want to
limit forward computation as much as possible.
In that case we might want to switch on some of the more complex
proof techniques for redundancy such as case analysis or clausal
rewriting (cf. \cmd{sarp} command).
Case analysis is particularly useful in the presence of \hyref{sec-ac}{AC-symbols}.
Clausal rewriting has no effect on purely equational theories.
It works best in a resolution context when equality plays no role at all.
The positive selection strategy (\sat{sass([2])}) is usually not appropriate
in this context.
Usually the lexicographic path orderings \sat{lpo} and \sat{aclpo}
with an aprropriately defined precedence work best in this context.
Once we have managed to saturate a theory finitely, all proofs
with respect to that theory are linear in the sense that they
have the set-of-support property.

\subsection{Establishing Complexity Bounds}
%\htmlLabel{72}
\label{sec-flags-locality}
Three aspects are of importance when using \Sat\ to
derive complexity bounds for entailment.
\begin{itemize}
        \item 
We need to use an ordering in which ground terms have at 
most finitely many smaller terms. An lpo is, hence, in most cases
not suitable.
        \item
The treatment of transitive relations by chaining has to be turned off
(cf. \cmdptr{add}{flags}{flag settings}) to invoke ordered
resolution also for transitive relations and, in particular, for
the transitivity axiom itself.
        \item
No selection of negative literals is allowed, cf.~command~\cmd{sass}.
\end{itemize}
For establishing a polynomial complexity
bound, the (precedence-modified)
subterm ordering \sat{sto} should be chosen 
with an appropriate
\cmdptr{add}{orddecl}{ordering declaration}.
Finitely saturating a theory under an instance of this class of partial orderings
(actually one saturates with respect to all possible well-founded
completions of 
that instance simultaneously) 
proves that the entailment problem for the respective theory
is decidable in polynomial time if the theory is Horn, and in CoNP,
if it is not Horn. 
We refer to~\cite{BasinGanzinger-95-mpii2-006}
for a detailed explanation of the theoretical basis.

The subdirectory 
\sat{\example{LocalTheories}{LocalTheories}}
of \sat{saturate/examples} shows examples that we have saturated with
respect to the sto, including the theory of term
\example{LocalTheories/emb}{embedding},
\example{LocalTheories/congHO}{congruence closure},
various fragments of 
\example{LocalTheories/bool}{propositional calculus},
and the largest PTIME fragment of Allen's interval logic: the theory
of \example{LocalTheories/ord}{partial nonstrict orderings}.
A formulation of \example{LocalTheories/lk}{sequent calculus}
has been saturated modulo AC and with respect to a linear interpretation
function as ordering. The details are explained in the respective file.
Term orderings via linear interpretations are available only
in the \Sat\ version under SICStus 3.0. Such interpretations 
may be useful when one
intends to prove exponential upper bounds for the complexity of
entailment problems.

Proving the locality of a theory usually requires clausal rewriting with
an appropriate setting of
\cmd{sarp}.
in addition to the usual simplification and deletion techniques.
In some cases hereditary ordering constraints  with \cmdp{sass}{[2]} will be useful.

%\sectionlevel{0}{f}{Relevant literature}
%\htmlLabel{73}
\bibliography{/HG/usr/hg/papers/literatur/meineWerke,/HG/usr/hg/papers/literatur/huge}
\bibliographystyle{agsm}

%\sectionlevel{0}{f}{Appendix}
%\htmlLabel{74}
\appendix

\section{Release Notes}
%\htmlLabel{75}

%\sectionlevel{1}{f}{^}
%\htmlLabel{76}

%\sectionlevel{2}{f}{^}
%\htmlLabel{77}

\paragraph{Version 2.5 (October 1996)}
%\htmlLabel{78}
\begin{itemize}
\item
We admit general clauses with general first-order formulas
as literals and integrate a kind of lazy CNF transformation into saturation.
\item
AC-superposition is now fully implemented.
However, the AC-unification and matching module is a rather slow
prototype. 
The AC-LPO is available as the default ordering in the presence of
AC-symbols. Constraint solving happens by means of a generic solver
for ordering constraints which is necessarily incomplete.
\item
Saturate can also read input files in DFG notation.
\end{itemize}

\paragraph{Version 2.4 (April 1996)}
%\htmlLabel{79}
\begin{itemize}
\item
 Precedences are generated automatically by some analysis
of dependencies between predicate and function symbols.
Now Saturate can be run fully automatically on a set of clauses
without caring about the ordering.
This seems to work well in many cases.
\item
 Saturate can also read input files in TPTP notation.
\end{itemize}

\paragraph{Version 2.3.1 (November 1995)}
%\htmlLabel{80}
\begin{itemize}
\item
 We have added support for hierarchical theories.
\item
 Ordering declarations and directives for saturation may be
kept separately from the definition of theories, cf.~command \cmd{in}.
\item
 We have integrated a Davis-Putnam-like satisfiability checker
contributed by Peter Barth
(SICStus 3.0 only).
This is useful for medium-sized to large near-propositional problems
such as in this \example{happy/andrews3}{example}.
\end{itemize}

\paragraph{Version 2.3 (September 1995)}
%\htmlLabel{81}
A new rewrite module has been added. Contextual simplification
is now more powerful than it was before.

\paragraph{Version 2.2 (August 1995)}
%\htmlLabel{82}
Inheritance for ordering constraints has been implemented,
cf.~command \cmd{saci}.

\paragraph{Version 2.2 (June 1995)}
%\htmlLabel{83}
Adapted to SICStus 3.0.

\paragraph{Version 2.1 (May 1995)}
%\htmlLabel{84}
We have added a constraint solver for the (lexicographic extension
to atoms of the) subterm ordering. This ordering should be used
when trying to apply Saturate for proving the locality of certain
theories, (cf. subdirectory 
\sat{\example{LocalTheories}{LocalTheories}}
of  \sat{saturate/examples}).
Finitely saturating a theory under this (partial) ordering 
(actually one saturates with respect to an arbitrary completion of 
that ordering) proves that the entailment problem for the respective theory
is decidable in polynomial time if the theory is Horn, and in CoNP,
if it is not Horn. The paper~\cite{BasinGanzinger-96-lics}
explains the details.

\paragraph{Version 2.0 (April 1995)}
%\htmlLabel{85}
In this version we use substitution tree indexing for
(forward) reduction and subsumption.
This makes the system substantially faster on larger examples.

We have made clausal rewriting more powerful
such that more theories can be finitely saturated

We support equivalences between (nonequational) atoms $A, B$, written
$A\equ B$.
Equivalences may also occur on literal positions in clauses, cf.~\cmd{in} command.

\paragraph{Version 1.6}
%\htmlLabel{86}
In this version in all kinds of transitive relations
are dealt with in a uniform way by chaining inferences.

There is still no full implementation for inheriting constraints.

Subdirectories  \example{hoare}{hoare}
and  \example{bledsoe}{bledsoe} of  \sat{saturate/examples}
exercise ordering relations.
In  \sat{hoare} you find lemmas that occur in the verification
of quicksort and binary search algorithms.
The directory  \sat{bledsoe} contains examples from various  papers
by Bledsoe,
including the intermediate value theorem and the challenge problems
stated in a JAR paper from 1990.

\paragraph{Version 1.0}
%\htmlLabel{87}
This is (was) the first version of the system for logic with equality.

In this version there are no specific redundancy provers for the cases
when equality and/or ordering constraints are inherited.
Also for the general case, more powerful redundancy notions are 
being developed.

Since ordering constraint solving is NP-complete, sometimes for very
large constraints (say, more than one screen full) it is not possible to decide
satisfiability in a reasonable time. In a future version some 
time-out mechanism has to be provided for these cases.
You can circumvent the problem by setting the constraint inheritance
mode to \sat{[]}, cf. command \cmd{saci}. In this case, a less complete and less
time consuming constraint solving mode is applied.

\section{Known Bugs}
%\htmlLabel{88}
\Sat\ is a prototype that we use to try out some of our theoretical ideas.
Many things should be improved, above all, speed.
Certainly, \Sat\ contains bugs that we haven't found yet.
There is no correctness guarantee whatsover that
we can provide with this system and no liability can be assumed
in any regard.

The following list describes bugs that are related to
certain implementation issues.

\cmdptr{add}{preddecl}{Reflexive closure declarations}
should be made only for strict
total orderings. This is not checked. For other transitive relations
it may result in cross incompleteness of the prover.

Certain Prolog-operators, in particular \sat{[\underscore{}|\underscore{}]}, ``\sat{not}'' and ``\sat{:}'' should
not appear as function symbols in clauses. Otherwise many things
could go wrong. This is not checked.

\end{document}
