<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{BauFurNie:ht}
\citation{Robinson:adwh}
\citation{ChaLee:slamtp}
\citation{Baumgartner:httng}
\citation{BauFurNie:ht}
\@writefile{toc}{\contentsline {paragraph}{Keywords:}{1}}
\@writefile{toc}{\contentsline {paragraph}{MSC codes:}{1}}
\@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{1}}
\citation{Baumgartner:httng}
\citation{Giese:pswbui}
\citation{Baumgartner:FDPLL}
\citation{Beckert:dfpswb}
\@writefile{toc}{\contentsline {section}{\numberline {2}Basic Definitions}{2}}
\@writefile{toc}{\contentsline {paragraph}{Language}{2}}
\@writefile{toc}{\contentsline {paragraph}{Substitutions}{2}}
\@writefile{toc}{\contentsline {paragraph}{Substitutions as Formulas}{3}}
\@writefile{toc}{\contentsline {paragraph}{Variable Constraints}{3}}
\@writefile{toc}{\contentsline {paragraph}{Tableaux, Branches}{3}}
\@writefile{toc}{\contentsline {paragraph}{Initialization}{4}}
\@writefile{toc}{\contentsline {paragraph}{Copy}{4}}
\@writefile{toc}{\contentsline {paragraph}{Extend}{4}}
\@writefile{toc}{\contentsline {paragraph}{Constraint Merge for Closure}{5}}
\@writefile{toc}{\contentsline {paragraph}{Tableau Bundles}{5}}
\@writefile{toc}{\contentsline {paragraph}{Open and Closed Bundles, Open and Closed Tableaux}{5}}
\@writefile{toc}{\contentsline {section}{\numberline {3}Soundness, Model Generation, Completeness}{6}}
\newlabel{VarDiff}{{2}{6}}
\@writefile{toc}{\contentsline {section}{\numberline {4}Refutation Proof Examples}{8}}
\@writefile{toc}{\contentsline {paragraph}{Syllogistic Reasoning}{9}}
\@writefile{toc}{\contentsline {paragraph}{Reasoning about Relations}{10}}
\@writefile{toc}{\contentsline {paragraph}{Closure by Copying}{10}}
\@writefile{toc}{\contentsline {paragraph}{Generation of Multiple Closing Substitutions}{10}}
\@writefile{toc}{\contentsline {paragraph}{Closure by Merge}{11}}
\@writefile{toc}{\contentsline {paragraph}{An AI Puzzle}{11}}
\@writefile{toc}{\contentsline {section}{\numberline {5}Model Generation Examples}{13}}
\@writefile{toc}{\contentsline {paragraph}{No All-Positive Clause Present}{13}}
\@writefile{toc}{\contentsline {paragraph}{Incompatible Branches}{13}}
\@writefile{toc}{\contentsline {paragraph}{Infinitary Tableau Development}{14}}
\@writefile{toc}{\contentsline {paragraph}{Open Tableau; No Further Rules Applicable}{14}}
\@writefile{toc}{\contentsline {section}{\numberline {6}Minimal Model Generation}{15}}
\@writefile{toc}{\contentsline {paragraph}{Reduction}{15}}
\@writefile{toc}{\contentsline {section}{\numberline {7}Fair Computation}{16}}
\@writefile{toc}{\contentsline {section}{\numberline {8}Adding Equality Reasoning}{16}}
\@writefile{toc}{\contentsline {section}{\numberline {9}Related Work}{16}}
\citation{EijHegNua:trap}
\bibstyle{acm}
\bibdata{/home/jve/texmacros/mybibentries}
\bibcite{Baumgartner:httng}{1}
\bibcite{Baumgartner:FDPLL}{2}
\bibcite{BauFurNie:ht}{3}
\bibcite{Beckert:dfpswb}{4}
\bibcite{ChaLee:slamtp}{5}
\bibcite{EijHegNua:trap}{6}
\bibcite{Giese:pswbui}{7}
\bibcite{Haskell98:rep}{8}
\@writefile{toc}{\contentsline {section}{\numberline {10}Adding Constraints to Free Variable Tableaux: The General Perspective}{17}}
\@writefile{toc}{\contentsline {section}{\numberline {11}To Do List}{17}}
\@writefile{toc}{\contentsline {paragraph}{Acknowledgement}{17}}
\bibcite{Robinson:adwh}{9}