Preview
Unable to display preview. Download preview PDF.
References
Leo Bachmair and Harald Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):217–247, 1994.
Thierry Boy de la Tour. An optimality result for clause form translation. Journal of Symbolic Computation, 14:283–301, 1992.
Li Dafa. The Formulation of the Halting Problem is Not Suitable for Describing the Halting Problem. Association for Automated Reasoning Newsletter, 27:1–7, October 1994.
Peter Graf. Substitution tree indexing. In Rewriting Techniques and Applications, RTA-95, volume 914 of LNCS, pages 117–131. Springer, 1995.
William McCune. Otter 2.0. In 10th International Conference on Automated Deduction, CADE-10, volume 449 of LNCS, pages 663–664. Springer, 1990.
Hans-Jürgen Ohlbach and Manfred Schmidt-Schauß. The lion and the unicorn. Journal of Automated Reasoning, 1(3):327–332, 1985.
Hans-Jürgen Ohlbach and Christoph Weidenbach. A note on assumptions about skolem functions. Journal of Automated Reasoning, 15(2):267–275, 1995.
Francis Jeffry Pelletier. Seventy-five problems for testing automatic theorem provers. Journal of Automated Reasoning, 2(2):191–216, 1986. Errata: Journal of Automated Reasoning, 4(2):235–236,1988.
Francis Jeffry Pelletier and Geoff Sutcliffe. An Erratum for Some Errata to Automated Theorem Proving Problems. Association for Automated Reasoning Newsletter, 31:8–14, December 1995.
G.E. Peterson. A technique for establishing completeness results in theorem proving with equality. SIAM Journal of Computation, 12(1):82–100, February 1983.
Georg Rock. Transformations of first-order formulae for automated reasoning. Master's thesis, Max-Planck-Institut für Informatik, Germany, April 1995. Supervisors: H.J. Ohlbach, C. Weidenbach.
Manfred Schmidt-Schauß and Gerd Smolka. Attributive concept description with complements. Artificial Intelligence, 48:1–26, 1991.
Mark Stickel. Schubert's steamroller problem: Formulations and solutions. Journal of Automated Reasoning, 2(1):89–101, 1986.
Christoph Weidenbach. Extending the resolution method with sorts. In Proc. of 13th International Joint Conference on Artificial Intelligence, IJCAI-93, pages 60–65. Morgan Kaufmann, 1993.
Christoph Weidenbach. First-order tableaux with sorts. Journal of the Interest Group in Pure and Applied Logics, IGPL, 3(6):887–906, 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Weidenbach, C., Gaede, B., Rock, G. (1996). SPASS & FLOTTER version 0.42. In: McRobbie, M.A., Slaney, J.K. (eds) Automated Deduction — Cade-13. CADE 1996. Lecture Notes in Computer Science, vol 1104. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61511-3_75
Download citation
DOI: https://doi.org/10.1007/3-540-61511-3_75
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61511-8
Online ISBN: 978-3-540-68687-3
eBook Packages: Springer Book Archive