Hyper tableaux

1. Peter Baumgartner and Ulrich Furbach. Hyper Tableaux and Disjunctive Logic Programming. Fachberichte Informatik 13-96, Universität Koblenz-Landau, Universität Koblenz-Landau, Institut für Informatik, Rheinau 1, D-56075 Koblenz, 1996.

   Google Scholar 

2. B. Beckert and R. Hähnle. An Improved Method for Adding Equality to Free Variable semantic Tableaux. In D. Kapur, editor, 11th International Conference on Automated Deduction, volume 607 of LNCS, pages 507–521. Springer, 1992.

   Google Scholar 

3. Bernhard Beckert and Joachim Posegga. leanTAP: Lean tableaubased deduction. Journal of Automated Reasoning, 1994. To appear.

   Google Scholar 

4. Jean-Paul Billon. The Disconnection Method. In P. Moscato, U. Moscato, D. Mundici, and M. Ornaghi, editors, Theorem Proving with Analytic Tableaux and Related Methods, volume 1071 of Lecture Notes in Artificial Intelligence. Springer, 1996.

   Google Scholar 

5. F. Bry and A. Yaha. Minimal model generation with unit hyper-resolution tableau. In 5th Workshop of Analytic Tableaux and Related methods, LNCS. Springer, 1996.

   Google Scholar 

6. C. Chang and R. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973.

   Google Scholar 

7. M. Fitting. First Order Logic and Automated Theorem Proving. Texts and Monographs in Computer Science. Springer, 1990.

   Google Scholar 

8. H. Fujita and R. Hasegawa. A Model Generation Theorem Prover in KL1 using a Ramified-Stack Algorithm. In Proc. of the Eigth International Conference on Logic Programming, pages 535–548, Paris, France, 1991.

   Google Scholar 

9. R. Hähnle, B. Beckert, and S. Gerberding. The Many-Valued Theorem Prover 3TAP. Interner Bericht 30/94, Universität Karlsruhe, 1994.

   Google Scholar 

10. R. Hähnle. Positive tableaux. Research note, 1995.

    Google Scholar 

11. R. Letz, K. Mayr, and C. Goller. Controlled Integrations of the Cut Rule into Connection Tableau Calculi. Journal of Automated Reasoning, 13, 1994.

    Google Scholar 

12. D. Loveland, D. Reed, and D. Wilson. SATCHMORE: SATCHMO with RElevance. Journal of Autmated Reasoning, 14:325–351, 1995.

    Article  Google Scholar 

13. R. Manthey and F. Bry. SATCHMO: a theorem prover implemented in Prolog. In Proc. 9th CADE. Argonnee, Illinois, Springer LNCS, 1988.

    Google Scholar 

14. I. Niemelä. Implementing circumscription using a tableau method. In Proceedings of the European Conference on Artificial Intelligence, Budapest, Hungary, August 1996. John Wiley. To appear.

    Google Scholar 

15. I. Niemelä. A tableau calculus for minimal model reasoning. In Proceedings of the Fifth Workshop on Theorem Proving with Analytic Tableaux and Related Methods, pages 278–294, Terrasini, Italy, May 1996. Springer-Verlag.

    Google Scholar 

16. F. Oppacher and E. Suen. HARP: A Tableau-Based Theorem Prover. Journal of Automated Reasoning, 4:69–100, 1988.

    Article  Google Scholar 

17. Arcot Rajasekar. Semantics for Disjunctive Logic Programs. PhD thesis, University of Maryland, 1989.

    Google Scholar 

18. J. A. Robinson. Automated deduction with hyper-resolution. Internat. J. Comput. Math., 1:227–234, 1965.

    Google Scholar 

19. Jörg H. Siekmann. Unification Theory. Journal of Symbolic Computation, 7(1):207–274, January 1989.

    Google Scholar 

20. G. Sutcliffe, C. Suttner, and T. Yemenis. The TPTP problem library. In A. Bundy, editor, Proc. CADE-12, volume 814 of LNAI. Springer, 1994.

    Google Scholar 

Download references