\contentsline {chapter}{\numberline {1.}Introduction}{1}
\addvspace {10\p@ } %Added Manually to conform to UIowa Thesis Specification
\contentsline {section}{\numberline {1.1}Motivation}{2}
\contentsline {section}{\numberline {1.2}Related Work}{3}
\contentsline {section}{\numberline {1.3}Problem Statement}{4}
\contentsline {section}{\numberline {1.4}Contribution of the thesis}{4}
\contentsline {section}{\numberline {1.5}Outline of the thesis}{5}
\contentsline {chapter}{\numberline {2.}Preliminaries}{7}
\contentsline {chapter}{\numberline {3.}Congruence Closure}{10}
\addvspace {10\p@ } %Added Manually to conform to UIowa Thesis Specification
\contentsline {section}{\numberline {3.1}What is Congruence Closure?}{10}
\contentsline {section}{\numberline {3.2}Decision Procedures for Combination of Theories}{11}
\contentsline {subsection}{\numberline {3.2.1}The Nelson and Oppen Approach}{12}
\contentsline {subsection}{\numberline {3.2.2}Shostak's Approach}{15}
\contentsline {section}{\numberline {3.3}CVC}{20}
\contentsline {subsection}{\numberline {3.3.1}CVC Input}{20}
\contentsline {subsection}{\numberline {3.3.2}The $\@mathcal Arr$ decision procedure}{22}
\contentsline {chapter}{\numberline {4.}The Rewriting-based Approach}{24}
\addvspace {10\p@ } %Added Manually to conform to UIowa Thesis Specification
\contentsline {section}{\numberline {4.1}Introduction}{24}
\contentsline {section}{\numberline {4.2}The Approach}{25}
\contentsline {subsection}{\numberline {4.2.1}Flattening}{25}
\contentsline {subsection}{\numberline {4.2.2}Using a Superposition-based theorem prover}{26}
\contentsline {section}{\numberline {4.3}$\@mathcal SP$ as a Decision Procedure for different theories}{29}
\contentsline {section}{\numberline {4.4}$\@mathcal SP$ as a decision procedure for other theories}{30}
\contentsline {chapter}{\numberline {5.}The E theorem Prover}{31}
\addvspace {10\p@ } %Added Manually to conform to UIowa Thesis Specification
\contentsline {section}{\numberline {5.1}Introduction}{31}
\contentsline {section}{\numberline {5.2}Proof Search Process}{31}
\contentsline {subsection}{\numberline {5.2.1}Clause Selection Order}{32}
\contentsline {subsection}{\numberline {5.2.2}Literal Selection}{35}
\contentsline {subsection}{\numberline {5.2.3}Term Ordering}{36}
\contentsline {subsection}{\numberline {5.2.4}Automatic Mode}{37}
\contentsline {section}{\numberline {5.3}Implementation Features}{37}
\contentsline {section}{\numberline {5.4}Proof Objects and Proof Checking}{37}
\contentsline {chapter}{\numberline {6.}Experiments}{39}
\addvspace {10\p@ } %Added Manually to conform to UIowa Thesis Specification
\contentsline {section}{\numberline {6.1}Background Theory}{39}
\contentsline {section}{\numberline {6.2}Types of Input}{40}
\contentsline {section}{\numberline {6.3}Strategies}{41}
\contentsline {subsection}{\numberline {6.3.1}E-Auto Strategy}{41}
\contentsline {subsection}{\numberline {6.3.2}E-SOS1 Strategy}{41}
\contentsline {subsection}{\numberline {6.3.3}E-SOS2 Strategy}{42}
\contentsline {section}{\numberline {6.4}Experimental Results}{43}
\contentsline {subsection}{\numberline {6.4.1}Example Problems from SVC}{43}
\contentsline {subsection}{\numberline {6.4.2}storecomm(N)}{44}
\contentsline {subsection}{\numberline {6.4.3}swap(N)}{46}
\contentsline {subsection}{\numberline {6.4.4}swap(N) - Alternative Presentation}{48}
\contentsline {chapter}{\numberline {7.}Discussion of the Experimental Results}{51}
\contentsline {chapter}{\numberline {8.}Summary and Future Research}{53}
\addvspace {10\p@ } %Added Manually to conform to UIowa Thesis Specification
\contentsline {section}{\numberline {8.1}Future Research}{54}
\contentsline {chapter}{BIBLIOGRAPHY}{56}