{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:16:14Z","timestamp":1754486174542},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540651918"},{"type":"electronic","value":"9783540495192"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-49519-3_7","type":"book-chapter","created":{"date-parts":[[2007,10,20]],"date-time":"2007-10-20T06:37:12Z","timestamp":1192862232000},"page":"82-99","source":"Crossref","is-referenced-by-count":34,"title":["A Tutorial on St\u00e5lmarck\u2019s Proof Procedure for Propositional Logic"],"prefix":"10.1007","author":[{"given":"Mary","family":"Sheeran","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gunnar","family":"St\u00e5lmarck","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"key":"7_CR1","first-page":"309","volume":"18","author":"E.W. Beth","year":"1955","unstructured":"E.W. Beth: Semantic entailment and formal derivability. Mededelingen der Kon. Nederlandes Akademie van Wetenschappen. Afd. letterkunde, n.s., 18, 309\u2013342, Amsterdam, 1955.","journal-title":"Mededelingen der Kon. Nederlandes Akademie van Wetenschappen. Afd. letterkunde"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"P. Bjesse, K. Claessen, M. Sheeran and S. Singh: Lava: Hardware Design in Haskell. Proc. Int. Conf. on Functional Programming, ACM Press, 1998.","DOI":"10.1145\/289423.289440"},{"key":"7_CR3","series-title":"Lect Notes Comput Sci","volume-title":"Proc. 9th Int. Conf. on Computer Aided Verification","author":"A. Bor\u00c4lv","year":"1997","unstructured":"A. Bor\u00c4lv:The industrial success of verification tools based on St\u00e5lmarck\u2019s method. Proc. 9th Int. Conf. on Computer Aided Verification, Springer-Verlag LNCS vol. 1254, 1997."},{"key":"7_CR4","unstructured":"A. Bor\u00c4lv and G. St\u00e5lmarck. Prover Technology in Railways, In Industrial-Strength Formal Methods, Academic Press, 1998."},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"R. Bryant: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. Comp., vol. c-35, no. 8, 1986.","DOI":"10.1109\/TC.1986.1676819"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"S.A. Cook: The complexity of theorem-proving procedures. In Proc. 3rd ACM Symp. on the Theory of Computing, 1971.","DOI":"10.1145\/800157.805047"},{"key":"7_CR7","unstructured":"M. D\u2019Agostino: Investigation into the complexity of some propositional calculi. D. Phil. Dissertation, Programming Research Group, Oxford University, 1990."},{"key":"7_CR8","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"M. Davis, G. Logemann and D. Loveland: A machine program for theorem proving. Communications of the ACM, 5:34\u2013397, 1962. Reprinted in [21].","journal-title":"Communications of the ACM"},{"key":"7_CR9","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"M. Davis and H. Putnam: A computing procedure for quantification theory. Journal of the ACM, 7:201\u2013215, 1960. Reprinted in [21].","journal-title":"Journal of the ACM"},{"key":"7_CR10","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1935","unstructured":"G. Gentzen: Untersuchungen \u00fcber das logische Schliessen. Mathematische Zeitschrift, 39, 176\u2013210, 1935. English translation in The Collected Papers of Gerhard Gentzen, Szabo (ed.), North-Holland, Amsterdam, 1969.","journal-title":"Mathematische Zeitschrift"},{"key":"7_CR11","unstructured":"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."},{"key":"7_CR12","series-title":"Lect Notes Comput Sci","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"1996","unstructured":"J. Harrison: The St\u00e5lmarck Method as a HOL Derived Rule. Theorem Proving in Higher Order Logics, Springer-Verlag LNCS vol. 1125, 1996."},{"key":"7_CR13","unstructured":"J.K.J. Hintikka: Form and content in quantification theory. Acta Philosophica Fennica, VII, 1955."},{"key":"7_CR14","unstructured":"S. Kanger: Provability in Logic. Acta Universitatis Stockholmiensis, Stockholm Studies in Philosopy, 1, 1957."},{"key":"7_CR15","volume-title":"Mathematical Logic","author":"S. C. Kleene","year":"1967","unstructured":"S. C. Kleene: Mathematical Logic. John Wiley and Sons Inc., New York, 1967."},{"key":"7_CR16","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1109\/43.310903","volume":"13","author":"W. Kunz","year":"1994","unstructured":"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.","journal-title":"IEEE Trans. CAD"},{"key":"7_CR17","unstructured":"M. Mondadori: An improvement of Jeffrey\u2019s deductive trees. Annali dell\u2019Universita di Ferrara; Sez III; Discussion paper 7, Universita di Ferrara, 1989."},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"K. Sch\u00fctte: Proof Theory, Springer-Verlag, Berlin, 1977.","DOI":"10.1007\/978-3-642-66473-1"},{"key":"7_CR19","unstructured":"G. St\u00e5lmarck: 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)."},{"key":"7_CR20","unstructured":"M. Sheeran and A. Bor\u00c4lv: How to prove properties of recursively defined circuits using St\u00e5lmarck\u2019s method. Proc. Workshop on Formal Methods for Hardware and Hardware-like systems, Marstrand, June 1998."},{"volume-title":"Automation of Reasoning","year":"1983","key":"7_CR21","unstructured":"J. Siekman and G. Wrightson (editors): Automation of Reasoning. Springer-Verlag, New York, 1983."},{"key":"7_CR22","volume-title":"First Order Logic","author":"R.M. Smullyan","year":"1969","unstructured":"R.M. Smullyan: First Order Logic. Springer, Berlin, 1969."},{"key":"7_CR23","series-title":"Lect Notes Comput Sci","volume-title":"Proc. Int. Conf. on Formal Methods in Computer-Aided Design","year":"1996","unstructured":"M. Srivas and A. Camilleri (editors): Proc. Int. Conf. on Formal Methods in Computer-Aided Design. Springer-Verlag LNCS vol. 1146, 1996."},{"key":"7_CR24","unstructured":"M. S\u00c4flund: Modelling and formally verifying systems and software in industrial applications. Proc. second Int. Conf. on Reliability, Maintainability and Safety (ICRMS\u2019 94), Xu Ferong (ed.), 1994."},{"key":"7_CR25","unstructured":"O. \u00e5kerlund, G. St\u00e5lmarck 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."}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49519-3_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T17:59:14Z","timestamp":1556906354000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49519-3_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651918","9783540495192"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-49519-3_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1998]]}}}