%VERSION:	clause-form.2003.03.25.tex
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
\documentclass{article}

%FOR ASCII VERSION, COMMENT-OUT ABOVE LINE AND UNCOMMENT THE NEXT 3:
%ALSO:  CHANGE ANY OCCURRENCES OF "supertabular" TO "tabular"
% then use dvi2tty
%\documentclass{article}
%\textwidth 30em
%\hoffset -0.875in

\usepackage{amssymb,fullpage,times,mathptm}


%to draw a line across the page:
\newcommand{\blank}{\mbox{}\hrulefill\linebreak}

%uncomment this to make it double-spaced (default is single-spaced)
%\renewcommand{\baselinestretch}{2}


\parindent 0.5in

% the next line turns hyphenation OFF
\pretolerance=10000


\begin{document}

\noindent
\footnotesize
{\bf CSE 463/563, Spring 2003}
\hspace*{2in}
http://www.cse.buffalo.edu/$\sim$rapaport/563.html\\\\
\normalsize
\centerline{\bf CLAUSE FORM}

\noindent
{\bf Notation:} $X \rightarrow Y$ for: Rewrite all occurrences of $X$ as $Y$.

\noindent
{\bf Algorithm} Clause-Form;\\
\hspace*{1em}{\bf Input} A wff $\alpha$ of FOL (or propositional logic);\\
\hspace*{1em}{\bf Output} A logically equivalent formula in clause form;\\
{\bf begin}
\begin{enumerate}
\item
Convert $\alpha$ to a logically equivalent formula in Prenex Normal Form:
	\begin{enumerate}
	\item
	$(\alpha \equiv \beta) \rightarrow ((\alpha \supset \beta) \wedge (\beta \supset \alpha))$
	\item
	$(\alpha \supset \beta) \rightarrow (\neg\alpha \vee \beta)$
	\item
	{\bf repeat:}
		\begin{enumerate}
		\item
		$\neg\neg\alpha \rightarrow \alpha$
		\item
		$\neg(\alpha \wedge \beta)  \rightarrow (\neg \alpha \vee \neg\beta)$
		\item
		$\neg(\alpha \vee \beta)  \rightarrow (\neg \alpha \wedge \neg\beta)$
		\item
		$\neg\exists x [\alpha] \rightarrow \forall x[\neg \alpha]$
		\item
		$\neg\forall  x[\alpha] \rightarrow \exists x[\neg \alpha]$
		\end{enumerate}
	{\bf until} `$\neg$' only applies to atomic wffs;
	\item
	\small
	{\bf begin optional section:}
		\begin{enumerate}
		\item
		$(\alpha \vee \alpha )  \rightarrow \alpha$
		\item
		$(\alpha \wedge \alpha )  \rightarrow \alpha$
		%\item
		%Eliminate all occurrences of $(\alpha \vee \neg \alpha )$
		\end{enumerate}
	{\bf end optional section;}
	\item
	\normalsize
	Rename variables such that variables bound by different quantifiers
	have unique names
	\item
	Move all quantifiers to the left, without changing their order	
	\end{enumerate}
\item
Convert PNF($\alpha$) to Skolem Normal Form:\\
\hspace*{1em}{\bf repeat:}
	\begin{enumerate}
	\item
	$\forall x_1 \ldots \forall x_n \exists y [\alpha (y)]
	 \rightarrow
	 \forall x_1 \ldots \forall x_n [\alpha (f(x_1 \ldots x_n))]$
	// $f$ is a new Skolem function
	\item
	$\exists y [\alpha (y)]  \rightarrow \alpha (c)$
	// $c$ is a new Skolem constant
	\end{enumerate}
\hspace*{1em}{\bf until} all existential quantifiers are eliminated

\item
Convert SNF($\alpha$) to Conjunctive Normal Form:
	\begin{enumerate}
	\item
	$\forall x [\alpha (x)]  \rightarrow \alpha (x)$
	\item
	{\bf repeat:}
	\begin{enumerate}
	\item
	$(\alpha \vee ( \beta \wedge \gamma )) \rightarrow
		 ((\alpha \vee \beta ) \wedge (\alpha \vee \gamma ))$
	\item
	\small
	{\bf begin optional section:}
		\begin{enumerate}
		\item
		$(\alpha \vee \alpha )  \rightarrow \alpha$
		\item
		$(\alpha \wedge \alpha )  \rightarrow \alpha$
		%\item
		%Eliminate all occurrences of $(\alpha \vee \neg \alpha )$
		\end{enumerate}
	{\bf end optional section;}
	\end{enumerate}
	\normalsize
	{\bf until} the formula is a conjunction of disjunctions of literals
	\end{enumerate}
\item
(optionally:) Convert CNF($\alpha$) to Clause Form:
	\begin{enumerate}
	\item
	$(\alpha \vee \beta )  \rightarrow \alpha\beta$
	(or: $[\alpha , \beta ]$)
	// $\alpha\beta$ (or: $[\alpha , \beta ]$) is a  ``clause''
	\item
	$(\alpha \wedge \beta )  \rightarrow \{\alpha , \beta \}$
	// these are sets of clauses
	\item
	Rename variables again such that each clause has different variables
	\end{enumerate}
\end{enumerate}
{\bf end.}

\blank
\tiny
\copyright 2003, William J. Rapaport\\
rapaport@cse.buffalo.edu\\
http://www.cse.buffalo.edu/$\sim$rapaport/563/clause-form.2003.03.25.pdf
\end{document}

