Abstract
In this paper we present Seduct, which is a theorem prover for many-sorted first order logic. Seduct has been specially tailored to economically discharge proof obligations arising during the process of software verification. We will mainly describe those features of Seduct which distinguish this theorem prover from other theorem provers and which make it especially suited for software verification.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Leo Bachmair. Canonical Equational Proofs. Birkhäuser Boston, Inc., Boston, MA, 1991.
R. S. Boyer and J. S. Moore. A Computational Logic. Academic Press, Orlando, Florida, 1979.
R. E. Bryant. Graph Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, 35(8):677–691, 1986.
W. Büttner and H. Simonis. Embedding Boolean expressions into logic programming. Journal of Symbolic Computation, 4:191–205, October 1987.
Nachum Dershowitz. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Vol. B, chapter 6, pages 243–320. Elsevier Science Publishers, 1990.
J. Gallier. Logic for Computer Science. Harper & Row, New York, 1986.
Stephen J. Garland and John V. Guttag. A guide to LP, the Larch Prover. Report 82, DEC Systems Research Center, Palo Alto, CA, December 1991.
Jieh Hsiang and Michaël Rusinowitch. On word problems in equational theories. In Thomas Ottmann, editor, Automata, Languages and Programming, volume 267 of Lecture Notes in Computer Science, pages 54–71. Springer-Verlag, 1987.
M. Heisel, W. Reif, and W. Stephan. Tactical theorem proving in program verification. In M. E. Stickel, editor, 10th International Conference on Automated Deduction, volume 449 of Lecture Notes in Computer Science, pages 117–131. Springer Verlag, 1990.
Donald E. Knuth and P. B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297. Pergamon Press, Oxford, Oxford, 1970.
Claus Bendix Nielsen. Boolean unification: a case study in verification with Seduct. Technical report, Siemens AG, Corporate Research and Development, 81730 Munich, Germany, 1994.
W. Reif. The Kiv-approach to software verification. This volume.
Karl Stroetmann and Claus Bendix Nielsen. A Guide to Seduct. Siemens AG, Munich, Germany, second edition, 1994.
R. M. Smullyan. First Order Logic. Springer Verlag, 1968.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Stroetmann, K. (1995). Seduct — A proof compiler for first order logic. In: Broy, M., Jähnichen, S. (eds) KORSO: Methods, Languages, and Tools for the Construction of Correct Software. Lecture Notes in Computer Science, vol 1009. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0015469
Download citation
DOI: https://doi.org/10.1007/BFb0015469
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60589-8
Online ISBN: 978-3-540-47802-7
eBook Packages: Springer Book Archive