<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
\relax 
\citation{Eijck01:cht}
\citation{Haskell98:rep}
\citation{Eijck01:cht}
\citation{BauFurNie:ht}
\citation{Robinson:adwh}
\citation{Baumgartner:httng}
\@writefile{toc}{\contentsline {paragraph}{Keywords:}{1}}
\@writefile{toc}{\contentsline {paragraph}{MSC codes:}{1}}
\@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{1}}
\citation{Giese:pswbui}
\citation{Haehnle:tarm}
\citation{Giese:icofvt}
\@writefile{toc}{\contentsline {section}{\numberline {2}Revision History}{2}}
\@writefile{toc}{\contentsline {section}{\numberline {3}Indices, Terms, Formulas}{2}}
\@writefile{toc}{\contentsline {section}{\numberline {4}Variables in Terms}{5}}
\@writefile{toc}{\contentsline {section}{\numberline {5}Substitutions}{6}}
\@writefile{toc}{\contentsline {section}{\numberline {6}Composition of Substitution Representations}{9}}
\@writefile{toc}{\contentsline {section}{\numberline {7}Generating Skolem Terms}{10}}
\@writefile{toc}{\contentsline {section}{\numberline {8}From Standard Form to Quantifier Free Form}{10}}
\@writefile{toc}{\contentsline {section}{\numberline {9}Clauses and Substitution on Clauses}{12}}
\@writefile{toc}{\contentsline {section}{\numberline {10}From Quantifier Free Form to Clausal Form}{13}}
\@writefile{toc}{\contentsline {section}{\numberline {11}Unification}{16}}
\@writefile{toc}{\contentsline {section}{\numberline {12}Joining of Substitutions, Unification of Clauses}{18}}
\@writefile{toc}{\contentsline {section}{\numberline {13}Varianthood, Instances, Subsumption}{19}}
\@writefile{toc}{\contentsline {section}{\numberline {14}Merging Substitution Streams}{20}}
\@writefile{toc}{\contentsline {section}{\numberline {15}Variable Renaming}{21}}
\@writefile{toc}{\contentsline {section}{\numberline {16}Multiplicity Functions}{21}}
\@writefile{toc}{\contentsline {section}{\numberline {17}Branches}{23}}
\@writefile{toc}{\contentsline {section}{\numberline {18}Trace Primitive}{24}}
\@writefile{toc}{\contentsline {section}{\numberline {19}Nodes}{24}}
\newlabel{s:Nodes}{{19}{24}}
\@writefile{toc}{\contentsline {section}{\numberline {20}Initialization}{26}}
\@writefile{toc}{\contentsline {section}{\numberline {21}Node Indexing}{26}}
\@writefile{toc}{\contentsline {section}{\numberline {22}Fair Computation}{27}}
\@writefile{toc}{\contentsline {section}{\numberline {23}Rigid Variables of a Clause Instance}{27}}
\@writefile{toc}{\contentsline {section}{\numberline {24}Matching}{27}}
\@writefile{toc}{\contentsline {section}{\numberline {25}Branch Extension and Node Extension}{29}}
\@writefile{toc}{\contentsline {section}{\numberline {26}Update of Clause Pointer and Clause Counter}{31}}
\@writefile{toc}{\contentsline {section}{\numberline {27}Refutation}{31}}
\@writefile{toc}{\contentsline {section}{\numberline {28}Theorem Proving and Satisfiability Checking}{34}}
\@writefile{toc}{\contentsline {section}{\numberline {29}Examples}{35}}
\@writefile{toc}{\contentsline {paragraph}{Propositional reasoning}{35}}
\@writefile{toc}{\contentsline {paragraph}{Aristotelian Syllogisms and Property Reasoning}{35}}
\@writefile{toc}{\contentsline {paragraph}{Closure by Constraint Merge}{36}}
\citation{Eijck01:cht}
\@writefile{toc}{\contentsline {paragraph}{AI puzzle}{37}}
\@writefile{toc}{\contentsline {paragraph}{Baby Arithmetic}{39}}
\@writefile{toc}{\contentsline {paragraph}{Reasoning about Relations}{41}}
\@writefile{toc}{\contentsline {section}{\numberline {30}Discussion}{43}}
\newlabel{s:discussion}{{30}{43}}
\citation{EijHegNua:trap}
\bibstyle{acm}
\bibdata{/home/jve/texmacros/mybibentries}
\@writefile{toc}{\contentsline {section}{\numberline {31}Further Work}{44}}
\@writefile{toc}{\contentsline {paragraph}{Acknowledgement}{44}}