Abstract
We explain Stålmarck’s proof procedure for classical propositional logic. The method is implemented in a commercial tool that has been used successfully in real industrial verification projects. Here, we present the proof system underlying the method, and motivate the various design decisions that have resulted in a system that copes well with the large formulas encountered in industrial-scale verification. We also discuss possible applications in Computer Aided Design of electronic circuits.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
E.W. Beth: Semantic entailment and formal derivability. Mededelingen der Kon. Nederlandes Akademie van Wetenschappen. Afd. letterkunde, n.s., 18, 309–342, Amsterdam, 1955.
P. Bjesse, K. Claessen, M. Sheeran and S. Singh: Lava: Hardware Design in Haskell. Proc. Int. Conf. on Functional Programming, ACM Press, 1998.
A. BorÄlv:The industrial success of verification tools based on Stålmarck’s method. Proc. 9th Int. Conf. on Computer Aided Verification, Springer-Verlag LNCS vol. 1254, 1997.
A. BorÄlv and G. Stålmarck. Prover Technology in Railways, In Industrial-Strength Formal Methods, Academic Press, 1998.
R. Bryant: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. Comp., vol. c-35, no. 8, 1986.
S.A. Cook: The complexity of theorem-proving procedures. In Proc. 3rd ACM Symp. on the Theory of Computing, 1971.
M. D’Agostino: Investigation into the complexity of some propositional calculi. D. Phil. Dissertation, Programming Research Group, Oxford University, 1990.
M. Davis, G. Logemann and D. Loveland: A machine program for theorem proving. Communications of the ACM, 5:34–397, 1962. Reprinted in [21].
M. Davis and H. Putnam: A computing procedure for quantification theory. Journal of the ACM, 7:201–215, 1960. Reprinted in [21].
G. Gentzen: Untersuchungen über das logische Schliessen. Mathematische Zeitschrift, 39, 176–210, 1935. English translation in The Collected Papers of Gerhard Gentzen, Szabo (ed.), North-Holland, Amsterdam, 1969.
J.F. Groote, J.W.C. Koorn and S.F.M. van Vlijmen: The Safety Guaranteeing System at Station Hoorn-Kersenboogerd. Technical Report 121, Logic Group Preprint Series, Utrecht Univ., 1994.
J. Harrison: The Stålmarck Method as a HOL Derived Rule. Theorem Proving in Higher Order Logics, Springer-Verlag LNCS vol. 1125, 1996.
J.K.J. Hintikka: Form and content in quantification theory. Acta Philosophica Fennica, VII, 1955.
S. Kanger: Provability in Logic. Acta Universitatis Stockholmiensis, Stockholm Studies in Philosopy, 1, 1957.
S. C. Kleene: Mathematical Logic. John Wiley and Sons Inc., New York, 1967.
W. Kunz and D.K. Pradhan: Recursive Learning: A New Implication Technique for Efficient Solutions to CAD-problems: Test, Verification and Optimization. IEEE Trans. CAD, vol. 13, no. 9, 1994.
M. Mondadori: An improvement of Jeffrey’s deductive trees. Annali dell’Universita di Ferrara; Sez III; Discussion paper 7, Universita di Ferrara, 1989.
K. Schütte: Proof Theory, Springer-Verlag, Berlin, 1977.
G. Stålmarck: A system for determining propositional logic theorems by applying values and rules to triplets that are generated from a formula, 1989. Swedish Patent No. 467 076 (approved 1992), U.S. Patent No. 5 276 897 (approved 1994), European Patent No. 0403 454 (approved 1995).
M. Sheeran and A. BorÄlv: How to prove properties of recursively defined circuits using Stålmarck’s method. Proc. Workshop on Formal Methods for Hardware and Hardware-like systems, Marstrand, June 1998.
J. Siekman and G. Wrightson (editors): Automation of Reasoning. Springer-Verlag, New York, 1983.
R.M. Smullyan: First Order Logic. Springer, Berlin, 1969.
M. Srivas and A. Camilleri (editors): Proc. Int. Conf. on Formal Methods in Computer-Aided Design. Springer-Verlag LNCS vol. 1146, 1996.
M. SÄflund: Modelling and formally verifying systems and software in industrial applications. Proc. second Int. Conf. on Reliability, Maintainability and Safety (ICRMS’ 94), Xu Ferong (ed.), 1994.
O. åkerlund, G. Stålmarck and M. Helander: Formal Safety and Reliability Analysis of Embedded Aerospace Systems at Saab. Proc. 7th IEEE Int. Symp. on Software Reliability Engineering (Industrial Track), IEEE Computer Society Press, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sheeran, M., Stålmarck, G. (1998). A Tutorial on Stålmarck’s Proof Procedure for Propositional Logic. In: Gopalakrishnan, G., Windley, P. (eds) Formal Methods in Computer-Aided Design. FMCAD 1998. Lecture Notes in Computer Science, vol 1522. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49519-3_7
Download citation
DOI: https://doi.org/10.1007/3-540-49519-3_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65191-8
Online ISBN: 978-3-540-49519-2
eBook Packages: Springer Book Archive