References

[BHS93]

Bernhard Beckert, Reiner Hähnle, and Peter H. Schmidt. The even more liberalized d-rule in free variable semantic tableaux. In Alexander Leitsch, editor, Third Kurt Gödel Colloquium on Computational Logic and Proof Theory, Lecture Notes in Computer Science. Springer Verlag, 1993.

[Bib87]

Wolfgang Bibel. Automated Theorem Proving. Vieweg, second, revised edition, 1987.

[BP94]

Bernhard Beckert and Joachim Posegga. : Lean tableau-based theorem proving. In Alan Bundy, editor, 12th International Conference on Automated Deduction, volume 814 of Lecture Notes in Artificial Intelligence, pages 793--795, Nancy, France, June 1994. Springer Verlag.

[CL73]

Chin-Liang Chang and Richard Char-Tung Lee. Symbolic Logic and Mechanical Theorem Proving. Computer Science Classics. Academic Press, 1973.

[Fit83]

Melvin C. Fitting. Proof Methods for Modal and Intuitionistic Logics. Reidel Publishing Company, Dordrecht, 1983.

[Koh95]

Michael Kohlhase. Higher-order tableaux. In Workshop on Theorem Proving with Analytic Tableaux and Related Methods, 1995.

[Sha92]

Natarajan Shankar. Proof search in the intuitionistic sequent calculus. In Deepak Kapur, editor, 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 522--536, Saratoga Springs, New York, USA, June 1992. Springer Verlag.