<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 />
\begin{thebibliography}{1}

\bibitem{Baumgartner:httng}
{\sc Baumgartner, P.}
\newblock Hyper tableaux --- the next generation.
\newblock In {\em Proceedings International Conference on Automated Reasoning
  with Analytic Tableaux and Related Methods\/} (1998), H.~d. Swart, Ed.,
  no.~1397 in Lecture Notes in Computer Science, Springer, pp.~60--76.

\bibitem{Baumgartner:FDPLL}
{\sc Baumgartner, P.}
\newblock {FDPLL} --- a first-order {D}avis-{P}utnam-{L}ogeman-{L}oveland
  procedure.
\newblock In {\em Automated Deduction\/} (2000), D.~McAllester, Ed., LNAI.
\newblock CADE-17.

\bibitem{BauFurNie:ht}
{\sc Baumgartner, P., Fr\"{o}hlich, P., and Niemel\"{a}, I.}
\newblock Hyper tableaux.
\newblock In {\em Proceedings {JELIA} 96\/} (1996), Lecture Notes in Artificial
  Intelligence, Springer.

\bibitem{Beckert:dfpswb}
{\sc Beckert, B.}
\newblock Depth-first proof search without backtracking for free variable
  clausal tableaux.
\newblock In {\em Proceedings International Workshop on First-Order Theorem
  Proving, St. Andrews, Scotland\/} (2000), P.~Baumgartner and H.~Zhang, Eds.,
  pp.~44--55.
\newblock Available online at
  \verb^http://i12www.ira.uka.de/~key/doc/2000/beckert00a.ps.gz^.

\bibitem{ChaLee:slamtp}
{\sc Chang, C., and Lee, R.}
\newblock {\em Symbolic Logic and Mechanical Theorem Proving}.
\newblock Academic Press, 1973.

\bibitem{EijHegNua:trap}
{\sc Eijck, J.~v., Heguiabehere, J., and Nuall\'ain, B.~O.}
\newblock Tableau reasoning and programming with dynamic first order logic.
\newblock Accepted for publication in the Logic Journal of the IGPL.
  Electronically available from
  \verb^http://www.cwi.nl/~jve/dynamo/papers/trap.ps.gz^, December 2000.

\bibitem{Giese:pswbui}
{\sc Giese, M.}
\newblock Proof search without backtracking using instance streams, position
  paper.
\newblock In {\em Proc.\ Int.\ Workshop on First-Order Theorem Proving, St.\
  Andrews, Scotland\/} (2000).
\newblock Available online at
  \href{http://i12www.ira.uka.de/~key/doc/2000/giese00.ps.gz}
  {\texttt{http://i12www.ira.uka.de/\~{}key/doc/2000/giese00.ps.gz}}.

\bibitem{Haskell98:rep}
{\sc Jones, S.~P., Hughes, J., et~al.}
\newblock Report on the programming language {H}askell 98.
\newblock Available from the {H}askell homepage: \verb+http://www.haskell.org+,
  1999.

\end{thebibliography}