\contentsline {chapter}{\numberline {1}Introduction}{1}
\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}
\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}{21}
\contentsline {subsection}{\numberline {3.3.2}The $\@mathcal Arr$ decision procedure}{22}
\contentsline {chapter}{\numberline {4}The Rewriting-based Approach}{24}
\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}
\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}
\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}{42}
\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$)}{47}
\contentsline {subsection}{\numberline {6.4.4}swap($N$) - Alternative Presentation}{49}
\contentsline {chapter}{\numberline {7}Discussion of the Experimental Results}{51}
\contentsline {chapter}{\numberline {8}Summary and Future Research}{53}
\contentsline {section}{\numberline {8.1}Future Research}{54}
\contentsline {chapter}{BIBLIOGRAPHY}{55}