{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T11:59:05Z","timestamp":1754481545294},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540615873"},{"type":"electronic","value":"9783540706410"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0105407","type":"book-chapter","created":{"date-parts":[[2011,11,9]],"date-time":"2011-11-09T21:17:00Z","timestamp":1320873420000},"page":"221-234","source":"Crossref","is-referenced-by-count":22,"title":["St\u00e5lmarck\u2019s algorithm as a HOL derived rule"],"prefix":"10.1007","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,4,29]]},"reference":[{"key":"15_CR1","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/BF01459101","volume":"99","author":"P. Bernays","year":"1928","unstructured":"P. Bernays and M. Sch\u00f6nfinkel. Zum Entscheidungsproblem der mathematischen Logik. Mathematische Annalen, 99:401\u2013419, 1928.","journal-title":"Mathematische Annalen"},{"key":"15_CR2","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35:677\u2013691, 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"15_CR3","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R. E. Bryant","year":"1992","unstructured":"R. E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24:293\u2013318, 1992.","journal-title":"ACM Computing Surveys"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"S. A. Cook. The complexity of theorem-proving procedures. In Proceedings of the 3rd ACM Symposium on the Theory of Computing, pages 151\u2013158, 1971.","DOI":"10.1145\/800157.805047"},{"key":"15_CR5","volume-title":"Technical Monograph PRG-88","author":"M. D'Agostino","year":"1990","unstructured":"M. D'Agostino. Investigations into the complexity of some propositional calculi. Technical Monograph PRG-88, Oxford University Computing Laboratory, Programming Research Group, 11 Keble Road, Oxford, OX1 3QD, 1990. Author's PhD thesis."},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"M. Di Manzo, E. Giunchiglia, A. Armando, and P. Pecchiari. Proving formulas through reduction to decidable classes. In P. Torasso, editor, Proceedings of the 3rd Congress of the Italian Association for Artificial Intelligence, AI*IA\u2019 93, volume 728 of Lecture Notes in Computer Science, pages 1\u201310. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-57292-9_36"},{"key":"15_CR7","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/BF00121264","volume":"8","author":"J. F. Groote","year":"1996","unstructured":"J. F. Groote. Hiding propositional constants in BDDs. Formal Methods in System Design, 8:91\u201396, 1996.","journal-title":"Formal Methods in System Design"},{"key":"15_CR8","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1093\/comjnl\/38.2.162","volume":"38","author":"J. Harrison","year":"1995","unstructured":"J. Harrison. Binary decision diagrams as a HOL derived rule. The Computer Journal, 38:162\u2013170, 1995.","journal-title":"The Computer Journal"},{"key":"15_CR9","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0167-9236(88)90097-8","volume":"4","author":"J. N. Hooker","year":"1988","unstructured":"J. N. Hooker. A quantitative approach to logical inference. Decision Support Systems, 4:45\u201369, 1988.","journal-title":"Decision Support Systems"},{"key":"15_CR10","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0167-9236(88)90128-5","volume":"4","author":"R. G. Jereslow","year":"1988","unstructured":"R. G. Jereslow. Computation-oriented reductions of predicate to propositional logic. Decision Support Systems, 4:183\u2013197, 1988.","journal-title":"Decision Support Systems"},{"key":"15_CR11","volume-title":"The procurement of safety critical software in defence equipment","author":"U. K. Ministry of Defence","year":"1991","unstructured":"U. K. Ministry of Defence. The procurement of safety critical software in defence equipment. Interim Defence Standard 00-55, MOD Directorate of Standardization, Kentigern House, 65 Brown Stree, Glasgow G2 8EX, UK, 1991."},{"key":"15_CR12","unstructured":"M. S\u00e4flund. Modelling and formally verifying systems and software in industrial applications. Unpublished; available from the National Physical Laboratory, Teddington, Middlesex, TW11 0LW, UK, 1994."},{"key":"15_CR13","unstructured":"G. St\u00e5lmarck. A proof theoretic concept of tautological hardness. Unpublished manuscript, 1994."},{"key":"15_CR14","unstructured":"G. St\u00e5lmarck. System for determining propositional logic theorems by applying values and rules to triplets that are generated from Boolean formula. United States Patent number 5,276,897; see also Swedish Patent 467 076, 1994."},{"key":"15_CR15","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/B978-0-08-040953-5.50011-8","volume-title":"Safety of Computer Control Systems, 1990 (SAFECOMP\u2019 90)","author":"G. St\u00e5lmarck","year":"1990","unstructured":"G. St\u00e5lmarck and M. S\u00e4flund. Modeling and verifying systems and software in propositional logic. In B. K. Daniels, editor, Safety of Computer Control Systems, 1990 (SAFECOMP\u2019 90), pages 31\u201336, Gatwick, UK, 1990. Pergamon Press."},{"key":"15_CR16","unstructured":"C. B. Suttner and G. Sutcliffe. The TPTP problem library. Technical Report AR-95-03, Institut f\u00fcr Infomatik, TU M\u00fcnchen, Germany, 1995. Also available as TR 95\/6 from Dept. Computer Science, James Cook University, Australia, and on the Web."},{"key":"15_CR17","first-page":"34","volume-title":"1 st International Conference on Constraints in Computational Logics, volume 845 of Lecture Notes in Computer Science","author":"T. Uribe","year":"1994","unstructured":"T. Uribe and M. E. Stickel. Ordered Binary Decision Diagrams and the Davis-Putnam procedure. In J.-P. Jouannaud, editor, 1\n                  st\n                \n                International Conference on Constraints in Computational Logics, volume 845 of Lecture Notes in Computer Science, pages 34\u201349, Munich, 1994. Springer-Verlag."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0105407","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,16]],"date-time":"2019-02-16T13:28:08Z","timestamp":1550323688000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0105407"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615873","9783540706410"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/bfb0105407","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}