Check-ins Using Download Hex

Artifact a8cae8845ef7961ed31cce963f9c67565314046f7d4dab5c7708ddf5e2e41e70:

\chapter{BOOLEAN: A package for boolean algebra} 
\label{BOOLEAN}
\typeout{{BOOLEAN: A package for boolean algebra}}

{\footnotesize
\begin{center}
Herbert Melenk\\
Konrad--Zuse--Zentrum f\"ur Informationstechnik Berlin \\
Takustra\"se 7 \\
D--14195 Berlin--Dahlem, Germany \\[0.05in]
e--mail:  melenk@zib.de
\end{center}
}

\ttindex{BOOLEAN}
The package {\bf Boolean} supports the computation with boolean
expressions in the propositional calculus.  The data objects are
composed from algebraic expressions (``atomic parts'', ``leafs'')
connected by the infix boolean operators {\bf and}, {\bf or}, {\bf
implies}, {\bf equiv}, and the unary prefix operator {\bf not}.  {\bf
Boolean} allows simplification of expressions built from these
operators, and to test properties like equivalence, subset property
etc.  Also the reduction of a boolean expression by a partial
evaluation and combination of its atomic parts is supported.

\section{Entering boolean expressions}

In order to distinguish boolean data expressions from 
boolean expressions in the \REDUCE\ programming
language ({\em e.g.} in an {\bf if} statement), each expression
must be tagged explicitly by an operator {\bf boolean}.
Otherwise the boolean operators are not accepted in the
\REDUCE\  algebraic mode input.
The first argument of {\bf boolean} can be any boolean expression,
which may contain references to other boolean values.
\begin{verbatim}
    load_package boolean;
    boolean (a and b or c);
    q := boolean(a and b implies c);
    boolean(q or not c);
\end{verbatim}
Brackets are used to override the operator precedence as usual.
The leafs or atoms of a boolean expression are those parts which
do not contain a leading boolean operator.  These are
considered as constants during the boolean evaluation.  There
are two pre-defined values:
\begin{itemize}
\item {\bf true}, {\bf t} or {\bf 1}
\item {\bf false}, {\bf nil} or {\bf 0}
\end{itemize}
These represent the boolean constants.  In a result
form they are used only as {\bf 1} and {\bf 0}.

By default, a {\bf boolean} expression is converted  to a
disjunctive normal form.

On output, the operators {\bf and} and {\bf or} are represented as
\verb+/\+ and \verb+\/+, respectively.
\begin{verbatim}
boolean(true and false);    ->   0
boolean(a or not(b and c)); -> boolean(not(b) \/ not(c) \/ a)
boolean(a equiv not c);     -> boolean(not(a)/\c \/ a/\not(c))
\end{verbatim}

\section{Normal forms}

The {\bf disjunctive} normal form is used by default. 
Alternatively a {\bf conjunctive} normal form can be
selected as simplification target, which is a form with
leading operator {\bf and}.  To produce that form add the keyword {\bf and}
as an additional argument to a call of {\bf boolean}.
\begin{verbatim}
boolean (a or b implies c); 
                    -> 
     boolean(not(a)/\not(b) \/ c)

boolean (a or b implies c, and); 
                    ->
     boolean((not(a) \/ c)/\(not(b) \/ c))
\end{verbatim}

Usually the result is a fully reduced disjunctive or conjuntive normal
form, where all redundant elements have been eliminated following the
rules

$ a \wedge b \vee \neg a \wedge b \longleftrightarrow b$

$ a \vee b \wedge \neg a \vee b \longleftrightarrow b$
 
Internally the full normal forms are computed
as intermediate result; in these forms each term contains
all leaf expressions, each one exactly once.  This unreduced form is
returned when the additional keyword {\bf full} is set:
\newpage
\begin{verbatim}
boolean (a or b implies c, full);
                   ->
boolean(a/\b/\c \/ a/\not(b)/\c \/ not(a)/\b/\c \/ not(a)/\not(b)/\c

         \/ not(a)/\not(b)/\not(c))
\end{verbatim}

The keywords {\bf full} and {\bf and} may be combined.

\section{Evaluation of a boolean expression}

If the leafs of the boolean expression are algebraic expressions which
may evaluate to logical values because the environment has changed
({\em e.g.\ }variables have been bound), one can re--investigate the
expression using the operator \f{TESTBOOL}\ttindex{TESTBOOL} with the
boolean expression as argument.  This operator tries to evaluate all
leaf expressions in \REDUCE\ boolean style.  As many terms as possible
are replaced by their boolean values; the others remain unchanged.
The resulting expression is contracted to a minimal form.  The result
{\bf 1} (= true) or {\bf 0} (=false) signals that the complete
expression could be evaluated.

In the following example the leafs are built as numeric greater test.
For using ${\bf >}$ in the expressions the greater sign must
be declared operator first.  The error messages are meaningless.
\begin{verbatim}
operator >;
fm:=boolean(x>v or not (u>v));
        ->
    fm := boolean(not(u>v) \/ x>v)

v:=10$ testbool fm;

   ***** u - 10 invalid as number
   ***** x - 10 invalid as number

        ->
   boolean(not(u>10) \/ x>10)

x:=3$ testbool fm;

   ***** u - 10 invalid as number

        ->
   boolean(not(u>10))

x:=17$ testbool fm;

   ***** u - 10 invalid as number

        ->
    1
\end{verbatim}
REDUCE Historical
[ REDUCE Sourceforge Project | Historical SVN Repository | GitHub Mirror | SourceHut Mirror | NotABug Mirror | Chisel Mirror | Chisel RSS ]