This is a preview of subscription content, log in via an institution to check access.
References
L. Bachmair and H. Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):217–247, 1994.
L. Bachmair and H. Ganzinger. Rewrite techniques for transitive relations. In Proc. 9th IEEE Symposium on Logic in Computer Science, pages 384–393. IEEE Computer Society Press, 1994.
L. Bachmair, H. Ganzinger, Chr. Lynch, and W. Snyder. Basic paramodulation. Information and Computation, 121(2):172–192, 1995.
L. Bachmair, H. Ganzinger, and U. Waldmann. Superposition with simplification as a decision procedure for the monadic class with equality. In G. Gottlob, A. Leitsch, and D. Mundici, editors, Proc. of Third Kurt Gödel Colloquium, KGC'93, volume 713 of Lecture Notes in Computer Science, pages 83–96, Berlin, 1993. Springer-Verlag.
D. Basin and H. Ganzinger. Automated complexity analysis based on ordered resolution. Research Report MPI-I-95-2-006, Max-Planck-Institut für Informatik, Saarbrücken, 1995. Extended abstract to appear in Proc. LICS'96.
R. Nieuwenhuis. Basic paramodulation and decidable theories. In Proc. 11th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 1994. To appear.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ganzinger, H. (1996). Saturation-based theorem proving (abstract). In: Meyer, F., Monien, B. (eds) Automata, Languages and Programming. ICALP 1996. Lecture Notes in Computer Science, vol 1099. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61440-0_113
Download citation
DOI: https://doi.org/10.1007/3-540-61440-0_113
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61440-1
Online ISBN: 978-3-540-68580-7
eBook Packages: Springer Book Archive