{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T11:03:13Z","timestamp":1777892593410,"version":"3.51.4"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2000,1]]},"DOI":"10.1023\/a:1008725524946","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T11:37:32Z","timestamp":1040557052000},"page":"23-58","source":"Crossref","is-referenced-by-count":61,"title":["A Tutorial on St\u00e5lmarck's Proof Procedure for Propositional Logic"],"prefix":"10.1007","volume":"16","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","reference":[{"key":"243846_CR1","doi-asserted-by":"crossref","unstructured":"M. Ajtai, \u201cThe complexity of the pigeonhole principle,\u201d in Proc. 29th Annual Symposium on Foundations of Computer Science, IEEE Press, pp. 346\u2013355, 1988.","DOI":"10.1109\/SFCS.1988.21951"},{"key":"243846_CR2","first-page":"309","volume":"18","author":"E.W. Beth","year":"1955","unstructured":"E.W. Beth, \u201cSemantic entailment and formal derivability,\u201d Mededelingen der Kon. Nederlandse Akademie van Wetenschappen. Afd. letterkunde, n.s., 18, Amsterdam, pp. 309\u2013342, 1955.","journal-title":"Mededelingen der Kon. Nederlandse Akademie van Wetenschappen. Afd. letterkunde"},{"key":"243846_CR3","doi-asserted-by":"crossref","unstructured":"P. Bjesse, K. Claessen, M. Sheeran, and S. Singh, \u201cLava: Hardware design in Haskell,\u201d in '98, ACM Press, 1998.","DOI":"10.1145\/289423.289440"},{"key":"243846_CR4","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1007\/3-540-63166-6_3","volume":"1254","author":"A. Bor\u00e4lv","year":"1997","unstructured":"A. Bor\u00e4lv, \u201cThe industrial success of verification tools based on St\u00b0almarck's method,\u201d in Proc. 9th Int. Conf. on Computer Aided Verification, Springer-Verlag, LNCS Vol. 1254, pp. 7\u201310, 1997.","journal-title":"Proc. 9th Int. Conf. on Computer Aided Verification, Springer-Verlag"},{"issue":"4","key":"243846_CR5","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1007\/s001650050021","volume":"10","author":"A. Bor\u00e4lv","year":"1999","unstructured":"A. Bor\u00e4lv, \u201cCase study: Formal verification of a computerized railway interlocking,\u201d Formal Aspects of Computing, Vol. 10, No. 4, pp. 338\u2013360, April 1999.","journal-title":"Formal Aspects of Computing"},{"key":"243846_CR6","volume-title":"Industrial-Strength Formal Methods in Practice","author":"A. Bor\u00e4lv","year":"1999","unstructured":"A. Bor\u00e4lv and G. St\u00e5lmarck, \u201cAutomated verification in railways,\u201d in M.G. Hinchey and J.P. Bowen (Eds.), Industrial-Strength Formal Methods in Practice, Springer-Verlag, London, 1999."},{"key":"243846_CR7","doi-asserted-by":"crossref","unstructured":"A. Biere, A. Cimatti, E. Clarke, and Y. Zhu, \u201cSymbolic model checking without BDDs,\u201d in '99, 1999.","DOI":"10.21236\/ADA360973"},{"issue":"8","key":"243846_CR8","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"c-35","author":"R. Bryant","year":"1986","unstructured":"R. Bryant, \u201cGraph-based algorithms for boolean function manipulation,\u201d IEEE Trans. Comp., Vol. c-35, No. 8, pp. 677\u2013691, August 1986.","journal-title":"IEEE Trans. Comp."},{"key":"243846_CR9","doi-asserted-by":"crossref","unstructured":"S.A. Cook, \u201cThe complexity of theorem-proving procedures,\u201d in Proc. 3rd ACM Symp. on the Theory of Computing, 1971.","DOI":"10.1145\/800157.805047"},{"key":"243846_CR10","unstructured":"M. D'Agostino, \u201cInvestigation into the complexity of some propositional calculi,\u201d D. Phil. Dissertation, Programming Research Group, Oxford University, 1990."},{"key":"243846_CR11","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"M. Davis, G. Logemann, and D. Loveland, \u201cA machine program for theorem proving,\u201d Communications of the ACM, Vol. 5, pp. 394\u2013397, 1962. Reprinted in [30].","journal-title":"Communications of the ACM"},{"key":"243846_CR12","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"M. Davis and H. Putnam, \u201cA computing procedure for quantification theory,\u201d Journal of the ACM, Vol. 7, pp. 201\u2013215, 1960. Reprinted in [30].","journal-title":"Journal of the ACM"},{"key":"243846_CR13","unstructured":"ESPRIT Project No. 25581-FAST. Integrating Formal Approaches to Specification, Test Case Generation and Automatic Design Verification. http:\/\/www.prover.com\/fast\/"},{"key":"243846_CR14","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1935","unstructured":"G. Gentzen, \u201cUntersuchungen \u00fcber das logische Schliessen,\u201d Mathematische Zeitschrift, Vol. 39, pp. 176\u2013210, 1935. English translation in The Collected Papers of Gerhard Gentzen, M.E. Szabo (Ed.), North-Holland, Amsterdam, 1969.","journal-title":"Mathematische Zeitschrift"},{"key":"243846_CR15","doi-asserted-by":"crossref","unstructured":"G. Gopalakrishnan and P. Windley (Eds.), in Proc. Int. Conf. on Formal Methods in Computer-Aided Design, LNCS Vol. 1522, Springer-Verlag, 1998.","DOI":"10.1007\/3-540-49519-3"},{"key":"243846_CR16","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1007\/BF00121264","volume":"8","author":"J.F. Groote","year":"1996","unstructured":"J.F. Groote, \u201cHiding propositional constants in BDDs,\u201d Formal Methods in System Design, Vol. 8, pp. 91\u201396, 1996.","journal-title":"Formal Methods in System Design"},{"key":"243846_CR17","doi-asserted-by":"crossref","unstructured":"J.F. Groote, J.W.C. Koorn, and S.F.M. van Vlijmen, \u201cThe safety guaranteeing system at station Hoorn-Kersenboogerd (extended abstract),\u201d in Proc. 10th Annual Conference on Computer Assurance (COMPASS' 95), IEEE Press, pp. 57\u201368, 1995. A longer version appears as Technical Report 121, Logic Group Preprint Series, Department of Philosophy, Utrecht University, 1994.","DOI":"10.1109\/CMPASS.1995.521887"},{"key":"243846_CR18","doi-asserted-by":"crossref","unstructured":"J. Harrison, \u201cThe St\u00e5lmarck method as a HOL derived rule,\u201d Theorem Proving in Higher Order Logics, LNCS Vol. 1125, Springer-Verlag, 1996.","DOI":"10.1007\/BFb0105407"},{"key":"243846_CR19","unstructured":"J.K.J. Hintikka, \u201cForm and content in quantification theory,\u201d Acta Philosophica Fennica, VII, 1955."},{"key":"243846_CR20","unstructured":"S. Kanger, \u201cProvability in logic,\u201d Stockholm Studies in Philosophy, 1, Acta Universitatis Stockholmiensis, 1957."},{"key":"243846_CR21","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":"243846_CR22","doi-asserted-by":"crossref","unstructured":"W. Kunz and D.K. Pradhan, \u201cRecursive learning: A new implication technique for efficient solutions to CAD-problems: Test, verification and optimization,\u201d IEEE Trans. CAD, Vol. 13, No. 9, 1994.","DOI":"10.1109\/43.310903"},{"key":"243846_CR23","doi-asserted-by":"crossref","unstructured":"N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud, \u201cThe synchronous dataflow programming language LUSTRE,\u201d Proc. IEEE, Vol. 79, No. 9, 1991.","DOI":"10.1109\/5.97300"},{"key":"243846_CR24","doi-asserted-by":"crossref","unstructured":"N. Halbwachs, F. Lagnier, and C. Ratel, \u201cProgramming and verifying real-time systems by means of the synchronous data-flow programming language Lustre,\u201d in IEEE Transactions on Software Engineering, September 1992.","DOI":"10.1109\/32.159839"},{"key":"243846_CR25","volume-title":"Formal modelling and automatic verification of Lustre programs using NP-tools","author":"M. Ljung","year":"1999","unstructured":"M. Ljung, \u201cFormal modelling and automatic verification of Lustre programs using NP-tools,\u201d Master's Project Thesis, Prover Technology AB and Department of Teleinformatics, KTH, Stockholm, 1999."},{"key":"243846_CR26","unstructured":"M. Mondadori, \u201cAn improvement of Jeffrey's deductive trees,\u201d Annali dell'Universita di Ferrara, Sez III, Discussion paper 7, Universita di Ferrara, 1989."},{"key":"243846_CR27","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-66473-1","volume-title":"Proof Theory","author":"K. Sch\u00fctte","year":"1977","unstructured":"K. Sch\u00fctte. Proof Theory, Springer-Verlag, Berlin, 1977."},{"key":"243846_CR28","unstructured":"G. St\u00e5lmarck, \u201cA system for determining propositional logic theorems by applying values and rules to triplets that are generated from a formula,\u201d 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":"243846_CR29","unstructured":"M. Sheeran and G. St\u00e5lmarck, \u201cModel checking using induction and boolean satisfiability,\u201d Technical Report U-99003, Prover Technology, June 1999."},{"key":"243846_CR30","volume-title":"Automation of Reasoning","year":"1983","unstructured":"J. Siekman and G. Wrightson (Eds.), Automation of Reasoning, Springer-Verlag, New York, 1983."},{"key":"243846_CR31","unstructured":"S. Singh and C.J. Lillieroth, \u201cFormal verification of reconfigurable cores,\u201d in Proc. Int. Conf. on Field-Programmable Custom Computing Machines, FCCM'99, IEEE Press, 1999."},{"key":"243846_CR32","volume-title":"First Order Logic","author":"R.M. Smullyan","year":"1969","unstructured":"R.M. Smullyan, First Order Logic, Springer-Verlag, Berlin, 1969."},{"key":"243846_CR33","doi-asserted-by":"crossref","unstructured":"M. Srivas and A. Camilleri (Eds.), in Proc. Int. Conf. on Formal Methods in Computer-Aided Design, LNCS Vol. 1146, Springer-Verlag, 1996.","DOI":"10.1007\/BFb0031795"},{"key":"243846_CR34","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1016\/0020-0190(89)90086-0","volume":"31","author":"G. St\u00e5lmarck","year":"1989","unstructured":"G. St\u00e5lmarck, \u201cA note on the computational complexity of the pure classical implication calculus,\u201d Information Processing Letters, Vol. 31, pp. 277\u2013278, June 1989.","journal-title":"Information Processing Letters"},{"key":"243846_CR35","first-page":"31","volume-title":"Proc. Int. Conf. on Safety of Computer Control Systems, IFAC SafeComp'90","author":"G. St\u00e5lmarck","year":"1990","unstructured":"G. St\u00e5lmarck and M. S\u00e4flund, \u201cModeling and verifying systems and software in propositional logic,\u201d in Proc. Int. Conf. on Safety of Computer Control Systems, IFAC SafeComp'90, Pergamon Press, Oxford, pp. 31\u201336, 1990."},{"key":"243846_CR36","unstructured":"M. S\u00e4flund, \u201cModelling and formally verifying systems and software in industrial applications,\u201d in '94), Xu Ferong (Ed.), International Academic Publishers, pp. 169\u2013174, June 1994."},{"key":"243846_CR37","unstructured":"J. \u00c5hrman, \u201cEvaluation of an algorithm for generating partial models in propositional logic using St\u00b0almarck's method,\u201d Master's Thesis, Royal Institute of Technology, Department of Numerical Analysis and Computing Science, 1998."},{"key":"243846_CR38","unstructured":"O. \u00c5kerlund, G. St\u00e5lmarck, and M. Helander, \u201cFormal safety and reliability analysis of embedded aerospace systems at Saab,\u201d in Proc. 7th IEEE Int. Symp. on Software Reliability Engineering (Industrial Track), IEEE Computer Society Press, 1996."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008725524946.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1008725524946\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008725524946.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T04:16:01Z","timestamp":1754367361000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1008725524946"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,1]]},"references-count":38,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2000,1]]}},"alternative-id":["243846"],"URL":"https:\/\/doi.org\/10.1023\/a:1008725524946","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2000,1]]}}}