{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T14:57:38Z","timestamp":1773154658536,"version":"3.50.1"},"reference-count":316,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2009,10,1]],"date-time":"2009-10-01T00:00:00Z","timestamp":1254355200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000083","name":"Directorate for Computer and Information Science and Engineering","doi-asserted-by":"publisher","award":["6.46E+12"],"award-info":[{"award-number":["6.46E+12"]}],"id":[{"id":"10.13039\/100000083","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000144","name":"Division of Computer and Network Systems","doi-asserted-by":"publisher","award":["CNS-0823086"],"award-info":[{"award-number":["CNS-0823086"]}],"id":[{"id":"10.13039\/100000144","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000104","name":"National Aeronautics and Space Administration","doi-asserted-by":"publisher","award":["NNX08AY53A"],"award-info":[{"award-number":["NNX08AY53A"]}],"id":[{"id":"10.13039\/100000104","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Comput. Surv."],"published-print":{"date-parts":[[2009,10]]},"abstract":"<jats:p>Automated deduction uses computation to perform symbolic logical reasoning. It has been a core technology for program verification from the very beginning. Satisfiability solvers for propositional and first-order logic significantly automate the task of deductive program verification. We introduce some of the basic deduction techniques used in software and hardware verification and outline the theoretical and engineering issues in building deductive verification tools. Beyond verification, deduction techniques can also be used to support a variety of applications including planning, program optimization, and program synthesis.<\/jats:p>","DOI":"10.1145\/1592434.1592437","type":"journal-article","created":{"date-parts":[[2009,10,8]],"date-time":"2009-10-08T17:31:08Z","timestamp":1255023068000},"page":"1-56","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":27,"title":["Automated deduction for verification"],"prefix":"10.1145","volume":"41","author":[{"given":"Natarajan","family":"Shankar","sequence":"first","affiliation":[{"name":"SRI International, Menlo Park, CA"}]}],"member":"320","published-online":{"date-parts":[[2009,10,9]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press","author":"Abdulla P. A."},{"key":"e_1_2_1_2_1","unstructured":"Abramsky S. Gabbay D. M. and Maibaum T. S. E. Eds. 1992a. Handbook of Logic in Computer Science; Volume 1 Background: Mathematical Structures. Oxford Science Publications Oxford UK. Abramsky S. Gabbay D. M. and Maibaum T. S. E. Eds. 1992a. Handbook of Logic in Computer Science; Volume 1 Background: Mathematical Structures. Oxford Science Publications Oxford UK."},{"key":"e_1_2_1_3_1","unstructured":"Abramsky S. Gabbay D. M. and Maibaum T. S. E. Eds. 1992b. Handbook of Logic in Computer Science; Volume 2 Background: Computational Structures. Oxford Science Publications Oxford UK. Abramsky S. Gabbay D. M. and Maibaum T. S. E. Eds. 1992b. Handbook of Logic in Computer Science; Volume 2 Background: Computational Structures. Oxford Science Publications Oxford UK."},{"key":"e_1_2_1_4_1","unstructured":"Abrial J.-R. 1980. The Specification Language Z: Syntax and Semantics. Programming Research Group Oxford University Oxford UK. Abrial J.-R. 1980. The Specification Language Z: Syntax and Semantics. Programming Research Group Oxford University Oxford UK."},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Abrial J.-R. 1996. The B-Book: Assigning Programs to Meanings. Cambridge University Press Cambridge MA. Abrial J.-R. 1996. The B-Book: Assigning Programs to Meanings. Cambridge University Press Cambridge MA.","DOI":"10.1017\/CBO9780511624162"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/646528.695189"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/11560548_20"},{"key":"e_1_2_1_8_1","unstructured":"Andrews P. B. 1986. An Introduction to Logic and Type Theory: To Truth through Proof. Academic Press New York NY. Andrews P. B. 1986. An Introduction to Logic and Type Theory: To Truth through Proof. Academic Press New York NY."},{"key":"e_1_2_1_9_1","volume-title":"9th International Conference on Automated Deduction (CADE), E. Lusk and R. Overbeek, Eds. Lecture Notes in Computer Science","volume":"310","author":"Andrews P. B."},{"key":"e_1_2_1_10_1","volume-title":"TAME: A specialized specification and verification system for timed automata. In Work In Progress (WIP) Proceedings of the 17th IEEE Real-Time Systems Symposium (RTSS'96)","author":"Archer M.","year":"1996"},{"key":"e_1_2_1_11_1","volume-title":"CADE. Lecture Notes in Computer Science","volume":"2392","author":"Audemard G."},{"key":"e_1_2_1_12_1","doi-asserted-by":"crossref","unstructured":"Baader F. and Nipkow T. 1998. Term Rewriting and All That. Cambridge University Press Cambridge MA. Baader F. and Nipkow T. 1998. Term Rewriting and All That. Cambridge University Press Cambridge MA.","DOI":"10.1017\/CBO9781139172752"},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Baader F. and Snyder W. 2001. Unification theory. Handbook of Automated Reasoning. Elsevier Science Amsterdam The Netherlands 445--533. Baader F. and Snyder W. 2001. Unification theory. Handbook of Automated Reasoning. Elsevier Science Amsterdam The Netherlands 445--533.","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Bachmair L. and Ganzinger H. 2001. Resolution theorem proving. Handbook of Automated Reasoning. Elsevier Science Amsterdam The Netherlands 19--99. Bachmair L. and Ganzinger H. 2001. Resolution theorem proving. Handbook of Automated Reasoning. Elsevier Science Amsterdam The Netherlands 19--99.","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"e_1_2_1_15_1","volume-title":"Ed. Lecture Notes in Computer Science","volume":"607","author":"Bachmair L."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:JARS.0000009518.26415.49"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"e_1_2_1_18_1","volume-title":"Handbook of Logic in Computer Science","author":"Barendregt H. P."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69149-5_16"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_4"},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the 19th International Conference on Computer Aided Verification, CAV 2007. Lecture Notes in Computer Science","volume":"4590","author":"Barrett C."},{"key":"e_1_2_1_22_1","unstructured":"Barrett C. Tinelli C. Sebastiani R. and Seshia S. 2009. Satisfiability modulo theories. See Biere et al. {2009}. Barrett C. Tinelli C. Sebastiani R. and Seshia S. 2009. Satisfiability modulo theories. See Biere et al. {2009}."},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the Symposium on Computer-Aided Verification, CAV '02","author":"Barrett C. W."},{"key":"e_1_2_1_24_1","volume-title":"Studies in Logic and the Foundations of Mathematics","volume":"90","author":"Barwise J., Ed.","year":"1978"},{"key":"e_1_2_1_25_1","first-page":"5","article-title":"An introduction to first-order logic. In Handbook of Mathematical Logic. North-Holland, Amsterdam, The Netherlands","volume":"1","author":"Barwise J.","year":"1978","journal-title":"Chapter"},{"key":"e_1_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Basu S. Pollack R. and Roy M.-F. 2003. Algorithms in Real Algebraic Geometry. Springer-Verlag Berlin Germany. Basu S. Pollack R. and Roy M.-F. 2003. Algorithms in Real Algebraic Geometry. Springer-Verlag Berlin Germany.","DOI":"10.1007\/978-3-662-05355-3"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390634"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006050629424"},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the International Conference on Computer-Aided Verification, CAV '98","volume":"1427","author":"Bensalem S."},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS","volume":"2619","author":"Berezin S.","year":"2003"},{"key":"e_1_2_1_31_1","doi-asserted-by":"crossref","unstructured":"Bertot Y. and Cast\u00e9ran P. 2004. Interactive Theorem Proving and Program Development. Springer. Coq home page: http:\/\/coq.inria.fr\/. Bertot Y. and Cast\u00e9ran P. 2004. Interactive Theorem Proving and Program Development. Springer. Coq home page: http:\/\/coq.inria.fr\/.","DOI":"10.1007\/978-3-662-07964-5"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/83471.83475"},{"key":"e_1_2_1_33_1","first-page":"2","article-title":"PicoSAT essentials","volume":"4","author":"Biere A.","year":"2008","journal-title":"J. SAT"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/309847.309942"},{"key":"e_1_2_1_35_1","unstructured":"Biere A. Heule M. van Maaren H. and Walsh T. Eds. 2009. Handbook of Satisfiability. IOS Press. Biere A. Heule M. van Maaren H. and Walsh T. Eds. 2009. Handbook of Satisfiability. IOS Press."},{"key":"e_1_2_1_36_1","doi-asserted-by":"crossref","unstructured":"Blackburn P. de Rijke M. and Venema Y. 2002. Modal Logic. Cambridge University Press Cambridge MA. Blackburn P. de Rijke M. and Venema Y. 2002. Modal Logic. Cambridge University Press Cambridge MA.","DOI":"10.1017\/CBO9781107050884"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(74)90009-5"},{"key":"e_1_2_1_38_1","doi-asserted-by":"crossref","unstructured":"Bockmayr A. and Weispfenning V. 2001. Solving numerical constraints. In Handbook of Automated Reasoning. Elsevier Science Amsterdam The Netherlands 751--742. Bockmayr A. and Weispfenning V. 2001. Solving numerical constraints. In Handbook of Automated Reasoning. Elsevier Science Amsterdam The Netherlands 751--742.","DOI":"10.1016\/B978-044450813-3\/50014-X"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_27"},{"key":"e_1_2_1_40_1","volume-title":"Proceedings of the 19th International Conference on Computer-Aided Verification, CAV. Lecture Notes in Computer Science","volume":"4590","author":"Bogudlov I."},{"key":"e_1_2_1_41_1","unstructured":"Boolos G. S. and Jeffrey R. C. 1989. Computability and Logic third ed. Cambridge University Press Cambridge UK. Boolos G. S. and Jeffrey R. C. 1989. Computability and Logic third ed. Cambridge University Press Cambridge UK."},{"key":"e_1_2_1_42_1","doi-asserted-by":"crossref","unstructured":"B\u00f6rger E. Gr\u00e4del E. and Gurevich Y. 1997. The Classical Decision Problem. Perspectives in Mathematical Logic. Springer-Verlag Berlin Germany. B\u00f6rger E. Gr\u00e4del E. and Gurevich Y. 1997. The Classical Decision Problem. Perspectives in Mathematical Logic. Springer-Verlag Berlin Germany.","DOI":"10.1007\/978-3-642-59207-2"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00358-9"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/390016.808445"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02328452"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/321864.321875"},{"key":"e_1_2_1_47_1","unstructured":"Boyer R. S. and Moore J. S. 1979. A Computational Logic. Academic Press New York. Boyer R. S. and Moore J. S. 1979. A Computational Logic. Academic Press New York."},{"key":"e_1_2_1_48_1","unstructured":"Boyer R. S. and Moore J. S. 1988. A Computational Logic Handbook. Academic Press New York. Boyer R. S. and Moore J. S. 1988. A Computational Logic Handbook. Academic Press New York."},{"key":"e_1_2_1_49_1","unstructured":"Bradley A. R. and Manna Z. 2007. The Calculus of Computation: Decision Procedures with Applications to Verification. Springer-Verlag Berlin Germany. Bradley A. R. and Manna Z. 2007. The Calculus of Computation: Decision Procedures with Applications to Verification. Springer-Verlag Berlin Germany."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_28"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_28"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/136035.136043"},{"key":"e_1_2_1_53_1","volume-title":"Proceedings of the Symposium on Computer-Aided Verification, CAV '2002","volume":"2404","author":"Bryant R. E."},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1088216.1088219"},{"key":"e_1_2_1_55_1","volume-title":"Proceedings of the International Conference on Computer-Aided Verification, CAV'97","volume":"1254","author":"Bultan T."},{"key":"e_1_2_1_56_1","first-page":"845","article-title":"The automation of proof by mathematical induction. In Handbook of Automated Reasoning, vol. I. Elsevier Science, Amsterdam, The Netherlands","volume":"13","author":"Bundy A.","year":"2001","journal-title":"Chapter"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"e_1_2_1_58_1","volume-title":"Graduate Texts in Mathematics","volume":"78","author":"Burris S. N."},{"key":"e_1_2_1_59_1","volume-title":"Proceedings of the 19th AIAA\/IEEE Digital Avionics Systems Conference.","author":"Carre\u00f1o V."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.2307\/2371045"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"e_1_2_1_63_1","unstructured":"Clarke E. M. Grumberg O. and Peled D. 1999. Model Checking. MIT Press Cambridge MA. Clarke E. M. Grumberg O. and Peled D. 1999. Model Checking. MIT Press Cambridge MA."},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1976.233817"},{"key":"e_1_2_1_65_1","volume-title":"Proceedings of the 10th International Conference on Rewriting Techniques and Applications (RTA-99)","volume":"1631","author":"Clavel M."},{"key":"e_1_2_1_66_1","volume-title":"Proceedings of the World Congress on Formal Methods (FM'99)","volume":"1709","author":"Clavel M."},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1002\/cpa.3160220202"},{"key":"e_1_2_1_68_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 2nd GI Conference on Automata Theory and Formal Languages","author":"Collins G."},{"key":"e_1_2_1_69_1","unstructured":"Constable R. L. Allen S. F. Bromley H. M. Cleaveland W. R. Cremer J. F. Harper R. W. Howe D. J. Knoblock T. B. Mendler N. P. Panangaden P. Sasaki J. T. and Smith S. F. 1986. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall Englewood Cliffs NJ. Nuprl home page: http:\/\/www.cs.cornell.edu\/Info\/Projects\/NuPRL\/. Constable R. L. Allen S. F. Bromley H. M. Cleaveland W. R. Cremer J. F. Harper R. W. Howe D. J. Knoblock T. B. Mendler N. P. Panangaden P. Sasaki J. T. and Smith S. F. 1986. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall Englewood Cliffs NJ. Nuprl home page: http:\/\/www.cs.cornell.edu\/Info\/Projects\/NuPRL\/."},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"key":"e_1_2_1_71_1","volume-title":"Machine Intelligence 7","author":"Cooper D. C."},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337234"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_19"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.2307\/2963594"},{"key":"e_1_2_1_77_1","doi-asserted-by":"crossref","unstructured":"D'Agostino M. Gabbay D. M. H\u00e4nle R. and Posegga J. Eds. 1999. Handbook of Tableau Methods. Kluwer Academic Publishers Dordrecht. D'Agostino M. Gabbay D. M. H\u00e4nle R. and Posegga J. Eds. 1999. Handbook of Tableau Methods. Kluwer Academic Publishers Dordrecht.","DOI":"10.1007\/978-94-017-1754-0"},{"key":"e_1_2_1_78_1","unstructured":"Dalen D. V. 1983. Logic and Structure. Springer-Verlag Berlin Germany. Dalen D. V. 1983. Logic and Structure. Springer-Verlag Berlin Germany."},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1016\/0097-3165(73)90004-6"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(81)90014-X"},{"key":"e_1_2_1_81_1","unstructured":"Davis M. Ed. 1965. The Undecidable. Raven Press Hewlett NY. Davis M. Ed. 1965. The Undecidable. Raven Press Hewlett NY."},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"e_1_2_1_84_1","series-title":"Lecture Notes in Mathematics","volume-title":"Symposium on Automatic Demonstration","author":"de Bruijn N. G."},{"key":"e_1_2_1_85_1","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"de Bruijn N. G."},{"key":"e_1_2_1_86_1","volume-title":"Proceedings of the 19th International Conference on Computer Aided Verification, CAV 2007. Lecture Notes in Computer Science","volume":"4590","author":"de Moura L."},{"key":"e_1_2_1_87_1","volume-title":"Proceedings of the 18th International Conference on Automated Deduction (CADE). Lecture Notes in Computer Science","volume":"2392","author":"de Moura L."},{"key":"e_1_2_1_88_1","volume-title":"Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008. Lecture Notes in Computer Science","volume":"4963","author":"de Moura L. M."},{"key":"e_1_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090100049"},{"key":"e_1_2_1_90_1","volume-title":"Simplify: A theorem prover for program checking. Tech. Rep. HPL-2003-148, HP Labs.","author":"Detlefs D.","year":"2003"},{"key":"e_1_2_1_91_1","volume-title":"Tech. Rep. 159","author":"Detlefs D. L.","year":"1998"},{"key":"e_1_2_1_92_1","first-page":"1009","article-title":"Higher-order unification and matching. In Handbook of Automated Reasoning, vol. II. Elsevier Science, Amsterdam, The Netherlands","volume":"16","author":"Dowek G.","year":"2001","journal-title":"Chapter"},{"key":"e_1_2_1_93_1","doi-asserted-by":"publisher","DOI":"10.1145\/322092.322104"},{"key":"e_1_2_1_94_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2008.923410"},{"key":"e_1_2_1_95_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_11"},{"key":"e_1_2_1_96_1","unstructured":"Dutertre B. and de Moura L. 2006b. The Yices SMT solver. http:\/\/yices.csl.sri.com\/. Dutertre B. and de Moura L. 2006b. The Yices SMT solver. http:\/\/yices.csl.sri.com\/."},{"key":"e_1_2_1_97_1","unstructured":"Ebbinghaus H.-D. Flum J. and Thomas W. 1984. Mathematical Logic. Undergraduate Texts in Mathematics. Springer-Verlag Berlin Germany. Ebbinghaus H.-D. Flum J. and Thomas W. 1984. Mathematical Logic. Undergraduate Texts in Mathematics. Springer-Verlag Berlin Germany."},{"key":"e_1_2_1_98_1","volume-title":"Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing. Lecture Notes in Artificial Intelligence, Springer-Verlag","author":"E\u00e9n N."},{"key":"e_1_2_1_99_1","doi-asserted-by":"publisher","DOI":"10.5555\/648295.754704"},{"key":"e_1_2_1_100_1","volume-title":"Proceedings of the International Conference on Computer-Aided Verification, CAV '98","volume":"1427","author":"Elgaard J."},{"key":"e_1_2_1_101_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87873-5_11"},{"key":"e_1_2_1_102_1","unstructured":"Elspas B. Green M. Moriconi M. and Shostak R. 1979. A JOVIAL verifier. Tech. rep. Computer Science Laboratory SRI International. Jan. Elspas B. Green M. Moriconi M. and Shostak R. 1979. A JOVIAL verifier. Tech. rep. Computer Science Laboratory SRI International. Jan."},{"key":"e_1_2_1_103_1","doi-asserted-by":"publisher","DOI":"10.1145\/356599.356602"},{"key":"e_1_2_1_104_1","first-page":"995","article-title":"Temporal and modal logic. In Handbook of Theoretical Computer Science. vol. B: Formal Models and Semantics. Elsevier and MIT Press, Amsterdam, The Netherlands, and Cambridge, MA","volume":"16","author":"Emerson E. A.","year":"1990","journal-title":"Chapter"},{"key":"e_1_2_1_105_1","unstructured":"Enderton H. B. 1972. A Mathematical Introduction to Logic. Academic Press New York NY. Enderton H. B. 1972. A Mathematical Introduction to Logic. Academic Press New York NY."},{"key":"e_1_2_1_106_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.053"},{"key":"e_1_2_1_107_1","volume-title":"Handbook of Mathematical Logic. North-Holland","author":"Feferman S."},{"key":"e_1_2_1_108_1","unstructured":"Feferman S. 2006. Tarski's influence on computer science. Logi. Meth. Comput. Sci. 2 3:6 1--13. Feferman S. 2006. Tarski's influence on computer science. Logi. Meth. Comput. Sci. 2 3:6 1--13."},{"key":"e_1_2_1_109_1","volume-title":"CAV. Lecture Notes in Computer Science","volume":"4590","author":"Filli\u00e2tre J.-C."},{"key":"e_1_2_1_110_1","unstructured":"Fischer M. J. and Rabin M. O. 1974. Super-exponential complexity of presburger arithmetic. In Complexity of Computation. American Mathematical Society Providence RI 27--41. Fischer M. J. and Rabin M. O. 1974. Super-exponential complexity of presburger arithmetic. In Complexity of Computation. American Mathematical Society Providence RI 27--41."},{"key":"e_1_2_1_111_1","doi-asserted-by":"crossref","unstructured":"Fitting M. 1990. First-Order Logic and Automated Theorem Proving. Springer-Verlag Berlin Germany. Fitting M. 1990. First-Order Logic and Automated Theorem Proving. Springer-Verlag Berlin Germany.","DOI":"10.1007\/978-1-4684-0357-2"},{"key":"e_1_2_1_112_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_34"},{"key":"e_1_2_1_113_1","volume-title":"Mathematical Aspects of Computer Science","author":"Floyd R. W."},{"key":"e_1_2_1_114_1","unstructured":"Fourier J. B. J. 1826. Solution d'une question particuli\u00e8re du calcul des in\u00e9galit\u00e9s. Nouveau Bulletin des Sciences par la Soci\u00e9t\u00e9 philomathique de Paris 99--100. Fourier J. B. J. 1826. Solution d'une question particuli\u00e8re du calcul des in\u00e9galit\u00e9s. Nouveau Bulletin des Sciences par la Soci\u00e9t\u00e9 philomathique de Paris 99--100."},{"key":"e_1_2_1_115_1","unstructured":"Frege G. 1893--1903. Grundgesetze der Arithmetik Begriffsschriftlich abgeleitet. Verlag Hermann Pohle Jena. Frege G. 1893--1903. Grundgesetze der Arithmetik Begriffsschriftlich abgeleitet. Verlag Hermann Pohle Jena."},{"key":"e_1_2_1_116_1","volume-title":"Handbook of Philosophical Logic--Volume I: Elements of Classical Logic. Synthese Library","volume":"164","author":"Gabbay D. M."},{"key":"e_1_2_1_117_1","volume-title":"Handbook of Philosophical Logic--Volume II: Extensions of Classical Logic. Synthese Library","volume":"165","author":"Gabbay D. M."},{"key":"e_1_2_1_118_1","volume-title":"Synthese Library","volume":"166","author":"Gabbay D. M."},{"key":"e_1_2_1_119_1","doi-asserted-by":"publisher","DOI":"10.1145\/364099.364331"},{"key":"e_1_2_1_120_1","doi-asserted-by":"publisher","DOI":"10.1007\/11916277_34"},{"key":"e_1_2_1_121_1","volume-title":"Information Processing '80","author":"Gerhart S. L."},{"key":"e_1_2_1_122_1","doi-asserted-by":"publisher","DOI":"10.1147\/rd.41.0028"},{"key":"e_1_2_1_123_1","unstructured":"Girard J.-Y. Lafont Y. and Taylor P. 1989. Proofs and Types. Cambridge Tracts in Theoretical Computer Science Cambridge University Press Cambridge MA. Girard J.-Y. Lafont Y. and Taylor P. 1989. Proofs and Types. Cambridge Tracts in Theoretical Computer Science Cambridge University Press Cambridge MA."},{"key":"e_1_2_1_124_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_2_1_125_1","unstructured":"G\u00f6del K. 1930. \u00dcber die vollst\u00e4ndigkeit des logikkalk\u00fcls. Ph.D. dissertation University of Vienna. (Translated by Stefan Bauer-Mengelberg and reprinted in van Heijenoort {1967 pages 582--591}.) G\u00f6del K. 1930. \u00dcber die vollst\u00e4ndigkeit des logikkalk\u00fcls. Ph.D. dissertation University of Vienna. (Translated by Stefan Bauer-Mengelberg and reprinted in van Heijenoort {1967 pages 582--591}.)"},{"key":"e_1_2_1_126_1","unstructured":"G\u00f6del K. 1967. On formally undecidable propositions of principia mathematica and related systems. (First published 1930 and 1931.) G\u00f6del K. 1967. On formally undecidable propositions of principia mathematica and related systems. (First published 1930 and 1931.)"},{"key":"e_1_2_1_127_1","volume-title":"Proceedings of the 1st International Workshop on Conditional Term Rewriting Systems. Lecture Notes in Computer Science","volume":"308","author":"Goguen J."},{"key":"e_1_2_1_128_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.dam.2006.10.007"},{"key":"e_1_2_1_129_1","volume-title":"CSLI. Lecture Notes","volume":"7","author":"Goldblatt R.","year":"1992"},{"key":"e_1_2_1_130_1","volume-title":"Handbook of Knowledge Representation. Foundations of Artificial Intelligence","volume":"3","author":"Gomes C. P."},{"key":"e_1_2_1_131_1","first-page":"11","article-title":"Formal proof: The four-color theorem","volume":"55","author":"Gonthier G.","year":"2008","journal-title":"Notices Amer. Math. Soc."},{"key":"e_1_2_1_132_1","unstructured":"Goodstein R. L. 1964. Recursive Number Theory. North-Holland Amsterdam The Netherlands. Goodstein R. L. 1964. Recursive Number Theory. North-Holland Amsterdam The Netherlands."},{"key":"e_1_2_1_134_1","volume-title":"HOL: A machine oriented formulation of higher order logic. Tech. Rep. 68","author":"Gordon M.","year":"1985"},{"key":"e_1_2_1_135_1","unstructured":"Gordon M. Milner R. Morris L. Newey M. and Wadsworth C. 1977. A metalanguage for interactive proof in LCF. Tech. Rep. CSR-16-77 Department of Computer Science University of Edinburgh Edinburgh UK. Gordon M. Milner R. Morris L. Newey M. and Wadsworth C. 1977. A metalanguage for interactive proof in LCF. Tech. Rep. CSR-16-77 Department of Computer Science University of Edinburgh Edinburgh UK."},{"key":"e_1_2_1_136_1","volume-title":"Edinburgh LCF: A Mechanized Logic of Computation. Lecture Notes in Computer Science","volume":"78","author":"Gordon M."},{"key":"e_1_2_1_137_1","volume-title":"Current Trends in Hardware Verification and Theorem Proving","author":"Gordon M. J. C."},{"key":"e_1_2_1_138_1","unstructured":"Gordon M. J. C. and Melham T. F. Eds. 1993. Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press Cambridge UK. HOL home page: http:\/\/www.cl.cam.ac.uk\/Research\/HVG\/HOL\/. Gordon M. J. C. and Melham T. F. Eds. 1993. Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press Cambridge UK. HOL home page: http:\/\/www.cl.cam.ac.uk\/Research\/HVG\/HOL\/."},{"key":"e_1_2_1_139_1","volume-title":"Proceedings of the 4th International Workshop on the ACL2 Theorem Prover","author":"Greve D.","year":"2003"},{"key":"e_1_2_1_140_1","doi-asserted-by":"crossref","unstructured":"Gries D. and Schneider F. B. 1993. A Logical Approach to Discrete Math. Texts and Monographs in Computer Science. Springer-Verlag Berlin Germany. Gries D. and Schneider F. B. 1993. A Logical Approach to Discrete Math. Texts and Monographs in Computer Science. Springer-Verlag Berlin Germany.","DOI":"10.1007\/978-1-4757-3837-7"},{"key":"e_1_2_1_141_1","doi-asserted-by":"publisher","DOI":"10.5555\/647766"},{"key":"e_1_2_1_142_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_19"},{"key":"e_1_2_1_143_1","volume-title":"Proceedings of the International Congress of Mathematicians. Higher Education Press","author":"Hales T. C.","year":"2002"},{"key":"e_1_2_1_144_1","doi-asserted-by":"crossref","unstructured":"Hales T. C. 2007. The Jordan curve theorem formally and informally. AMM: The American Mathematical Monthly 114. Hales T. C. 2007. The Jordan curve theorem formally and informally. AMM: The American Mathematical Monthly 114.","DOI":"10.1080\/00029890.2007.11920481"},{"key":"e_1_2_1_145_1","unstructured":"Hales T. C. Harrison J. McLaughlin S. Nipkow T. Obua S. and Zumkeller R. 2009. A revision of the proof of the Kepler conjecture. Disc. Comput. Geom. http:\/\/www.springerlink.com\/content\/552kw4u6330952jk\/fulltext.pdf. Hales T. C. Harrison J. McLaughlin S. Nipkow T. Obua S. and Zumkeller R. 2009. A revision of the proof of the Kepler conjecture. Disc. Comput. Geom. http:\/\/www.springerlink.com\/content\/552kw4u6330952jk\/fulltext.pdf."},{"key":"e_1_2_1_146_1","unstructured":"Halmos P. R. 1960. Naive Set Theory. The University Series in Undergraduate Mathematics. Van Nostrand Reinhold Company New York NY. Halmos P. R. 1960. Naive Set Theory. The University Series in Undergraduate Mathematics. Van Nostrand Reinhold Company New York NY."},{"key":"e_1_2_1_147_1","doi-asserted-by":"publisher","DOI":"10.2307\/2687775"},{"key":"e_1_2_1_148_1","doi-asserted-by":"publisher","DOI":"10.5555\/1030033.1030059"},{"key":"e_1_2_1_149_1","doi-asserted-by":"crossref","unstructured":"Hamon G. de Moura L. and Rushby J. 2005. Automated test generation with SAL. Technical note Computer Science Laboratory SRI International Menlo Park CA. Sept. Available at: http:\/\/www.csl.sri.com\/users\/rushby\/abstracts\/sal-atg. Hamon G. de Moura L. and Rushby J. 2005. Automated test generation with SAL. Technical note Computer Science Laboratory SRI International Menlo Park CA. Sept. Available at: http:\/\/www.csl.sri.com\/users\/rushby\/abstracts\/sal-atg.","DOI":"10.1007\/978-3-540-27813-9_45"},{"key":"e_1_2_1_150_1","volume-title":"IEE Proceedings 133 Part E, 5 (Sept.), 242--254","author":"Hanna F. K."},{"key":"e_1_2_1_151_1","doi-asserted-by":"publisher","DOI":"10.1145\/356674.356677"},{"key":"e_1_2_1_152_1","volume-title":"Proceedings of the IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press","author":"Harper R."},{"key":"e_1_2_1_153_1","doi-asserted-by":"publisher","DOI":"10.5555\/646184.682934"},{"key":"e_1_2_1_154_1","unstructured":"Harrison J. 2001. The LCF approach to theorem proving. Available from http:\/\/www.cl.cam.ac.uk\/~jrh13\/slides\/manchester-12sep01\/slides.pdf. Harrison J. 2001. The LCF approach to theorem proving. Available from http:\/\/www.cl.cam.ac.uk\/~jrh13\/slides\/manchester-12sep01\/slides.pdf."},{"key":"e_1_2_1_155_1","doi-asserted-by":"publisher","DOI":"10.1007\/11757283_8"},{"key":"e_1_2_1_156_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792233.1792242"},{"key":"e_1_2_1_157_1","doi-asserted-by":"crossref","unstructured":"Harrison J. 2009. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press Cambridge MA. Harrison J. 2009. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press Cambridge MA.","DOI":"10.1017\/CBO9780511576430"},{"key":"e_1_2_1_158_1","doi-asserted-by":"publisher","DOI":"10.2307\/2267044"},{"key":"e_1_2_1_159_1","doi-asserted-by":"publisher","DOI":"10.2307\/2266967"},{"key":"e_1_2_1_160_1","doi-asserted-by":"publisher","DOI":"10.2307\/421107"},{"key":"e_1_2_1_161_1","volume-title":"Proceedings of the 10th International Workshop on Model Checking of Software (SPIN). Lecture Notes in Computer Science","volume":"2648","author":"Henzinger T. A."},{"key":"e_1_2_1_162_1","unstructured":"Herbrand J. 1930. Recherches sur la th\u00e9orie de la d\u00e9monstration. Ph.D. dissertation Universit\u00e9 de Paris Paris France. (English translation published in van Heijenoort {1967} and Herbrand Herbrand {1971}.) Herbrand J. 1930. Recherches sur la th\u00e9orie de la d\u00e9monstration. Ph.D. dissertation Universit\u00e9 de Paris Paris France. (English translation published in van Heijenoort {1967} and Herbrand Herbrand {1971}.)"},{"key":"e_1_2_1_163_1","doi-asserted-by":"crossref","unstructured":"Herbrand J. 1971. Logical Writings. Harvard University Press. Herbrand J. 1971. Logical Writings. Harvard University Press.","DOI":"10.1007\/978-94-010-3072-4"},{"key":"e_1_2_1_164_1","doi-asserted-by":"publisher","DOI":"10.1145\/1459352.1459354"},{"key":"e_1_2_1_165_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9904-1902-00923-3"},{"key":"e_1_2_1_166_1","doi-asserted-by":"publisher","DOI":"10.1145\/602382.602403"},{"key":"e_1_2_1_167_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69149-5_1"},{"key":"e_1_2_1_168_1","unstructured":"Hodges W. 1997. A Shorter Model Theory. Cambridge University Press Cambridge MA. Hodges W. 1997. A Shorter Model Theory. Cambridge University Press Cambridge MA."},{"key":"e_1_2_1_169_1","volume-title":"Wissenschaften","volume":"257","author":"H\u00f6rmander L.","year":"1983"},{"key":"e_1_2_1_170_1","unstructured":"Howard W. 1980. The formulas-as-types notion of construction. To H.B. Curry: Essays on Combinatory Logic Lambda-Calculus and Formalism. Academic Press New York 479--490. Howard W. 1980. The formulas-as-types notion of construction. To H.B. Curry: Essays on Combinatory Logic Lambda-Calculus and Formalism. Academic Press New York 479--490."},{"key":"e_1_2_1_171_1","volume-title":"Proceedings of the International Conference Computer-Aided Verification, CAV '98","volume":"1427","author":"Hu A. J."},{"key":"e_1_2_1_172_1","doi-asserted-by":"publisher","DOI":"10.5555\/83471.83476"},{"key":"e_1_2_1_173_1","volume-title":"Computer Science: Modelling and Reasoning about Systems","author":"Huth M. R. A.","year":"2000"},{"key":"e_1_2_1_174_1","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"Jackson D.","year":"2006"},{"key":"e_1_2_1_175_1","doi-asserted-by":"publisher","DOI":"10.1007\/11527695_15"},{"key":"e_1_2_1_176_1","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592438"},{"key":"e_1_2_1_177_1","unstructured":"Jones C. B. 1990. Systematic Software Development Using VDM second ed. Prentice-Hall International Series in Computer Science. Prentice-Hall Hemel Hempstead UK. Jones C. B. 1990. Systematic Software Development Using VDM second ed. Prentice-Hall International Series in Computer Science. Prentice-Hall Hemel Hempstead UK."},{"key":"e_1_2_1_179_1","doi-asserted-by":"publisher","DOI":"10.5555\/555902"},{"key":"e_1_2_1_180_1","volume-title":"COMPASS '96 (Proceedings of the Eleventh Annual Conference on Computer Assurance). IEEE Washington Section","author":"Kaufmann M."},{"key":"e_1_2_1_181_1","volume-title":"Proceedings of the 10th European Conference on Artificial Intelligence","author":"Kautz H."},{"key":"e_1_2_1_183_1","volume-title":"Proceedings of the Symposium on Mathematical Foundations of Computer Science. 54--71","author":"Kesten Y."},{"key":"e_1_2_1_184_1","unstructured":"King J. C. 1969. A program verifier. Ph.D. dissertation Carnegie Mellon University Pittsburgh PA. King J. C. 1969. A program verifier. Ph.D. dissertation Carnegie Mellon University Pittsburgh PA."},{"key":"e_1_2_1_185_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_2_1_186_1","doi-asserted-by":"publisher","DOI":"10.1145\/800161.805162"},{"key":"e_1_2_1_187_1","unstructured":"Kleene S. C. 1952. Introduction to Metamathematics. North-Holland Amsterdam The Netherlands. Kleene S. C. 1952. Introduction to Metamathematics. North-Holland Amsterdam The Netherlands."},{"key":"e_1_2_1_188_1","unstructured":"Kleene S. C. 1967. Mathematical Logic. Wiley New York. Kleene S. C. 1967. Mathematical Logic. Wiley New York."},{"key":"e_1_2_1_189_1","first-page":"239","article-title":"Pervasive verification of distributed real-time systems. In Software System Reliability and Security. IOS Press, NATO Security Through Science Series","volume":"9","author":"Knapp S.","year":"2007","journal-title":"Sub-Series D: Information and Communication Security"},{"key":"e_1_2_1_190_1","doi-asserted-by":"publisher","DOI":"10.1145\/800105.803406"},{"key":"e_1_2_1_191_1","doi-asserted-by":"publisher","DOI":"10.1145\/775832.775928"},{"key":"e_1_2_1_192_1","volume-title":"Decision Procedures: An Algorithmic Point of View","author":"Kr\u00f6ning D.","year":"2008"},{"key":"e_1_2_1_193_1","volume-title":"Set Theory: An Introduction to Independence Proofs. Studies in Logic and the Foundations of Mathematics","author":"Kunen K.","year":"1980"},{"key":"e_1_2_1_194_1","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming, Volume 2: Deduction Methodologies","author":"Leivant D."},{"key":"e_1_2_1_195_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2007.371254"},{"key":"e_1_2_1_196_1","doi-asserted-by":"publisher","DOI":"10.1109\/MAHC.1984.10036"},{"key":"e_1_2_1_197_1","doi-asserted-by":"publisher","DOI":"10.1145\/319151.319157"},{"key":"e_1_2_1_198_1","volume-title":"CSD Report STAN-CS-79-731, Stanford","author":"Luckham D. C.","year":"1979"},{"key":"e_1_2_1_199_1","volume-title":"Tech. Rep. ECS-LFCS-92-211","author":"Luo Z.","year":"1992"},{"key":"e_1_2_1_200_1","doi-asserted-by":"crossref","unstructured":"Manna Z. Stickel M. and Waldinger R. 1991. Monotonicity properties in automated deduction. In Artificial Intelligence and Mathematical Theorem of Computation: Papers in Honor of John McCarthy Academic Press Orlando FL 261--280. Manna Z. Stickel M. and Waldinger R. 1991. Monotonicity properties in automated deduction. In Artificial Intelligence and Mathematical Theorem of Computation: Papers in Honor of John McCarthy Academic Press Orlando FL 261--280.","DOI":"10.1016\/B978-0-12-450010-5.50021-9"},{"key":"e_1_2_1_201_1","doi-asserted-by":"publisher","DOI":"10.1145\/357084.357090"},{"key":"e_1_2_1_202_1","volume-title":"Proceedings of the 10th International Conference in Theory and Applications of Satisfiability Testing\u2014SAT","volume":"4501","author":"Manolios P.","year":"2007"},{"key":"e_1_2_1_203_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.769433"},{"key":"e_1_2_1_204_1","unstructured":"Martin-L\u00f6f P. 1980. Intuitionistic Type Theory. Bibliopolis Napoli Italy. Martin-L\u00f6f P. 1980. Intuitionistic Type Theory. Bibliopolis Napoli Italy."},{"key":"e_1_2_1_205_1","unstructured":"Matiyasevich Y. V. 1993. Hilbert's Tenth Problem. MIT Press Cambridge MA. Matiyasevich Y. V. 1993. Hilbert's Tenth Problem. MIT Press Cambridge MA."},{"key":"e_1_2_1_206_1","volume-title":"Proceedings of a Symposium in Pure Mathematics.","author":"McCarthy J.","year":"1962"},{"key":"e_1_2_1_207_1","volume-title":"Computer Programming and Formal Systems, North-Holland","author":"McCarthy J."},{"key":"e_1_2_1_208_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005843212881"},{"key":"e_1_2_1_209_1","unstructured":"McCune W. W. 1990. OTTER 2.0 users guide. Tech. Rep. ANL-90\/9 Mathematics and Computer Science Division Argonne National Laboratory Argonne IL. Mar. McCune W. W. 1990. OTTER 2.0 users guide. Tech. Rep. ANL-90\/9 Mathematics and Computer Science Division Argonne National Laboratory Argonne IL. Mar."},{"key":"e_1_2_1_210_1","unstructured":"McCune W. W. 2007. The Prover9 reference manual. http:\/\/www.cs.wnm.edu\/~mccune\/prover9\/manual-examples.html. McCune W. W. 2007. The Prover9 reference manual. http:\/\/www.cs.wnm.edu\/~mccune\/prover9\/manual-examples.html."},{"key":"e_1_2_1_211_1","doi-asserted-by":"crossref","unstructured":"McMillan K. L. 1993. Symbolic Model Checking. Kluwer Academic Publishers Boston MA. McMillan K. L. 1993. Symbolic Model Checking. Kluwer Academic Publishers Boston MA.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"e_1_2_1_212_1","volume-title":"Proceedings of the 15th International Conference on Computer Aided Verification, CAV","author":"McMillan K. L.","year":"2003"},{"key":"e_1_2_1_213_1","unstructured":"Mendelson E. 1964. Introduction to Mathematical Logic. The University Series in Undergraduate Mathematics. D. Van Nostrand Company New York NY. Mendelson E. 1964. Introduction to Mathematical Logic. The University Series in Undergraduate Mathematics. D. Van Nostrand Company New York NY."},{"key":"e_1_2_1_214_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70132-0"},{"key":"e_1_2_1_215_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69149-5_28"},{"key":"e_1_2_1_216_1","volume-title":"Proceedings of the 1st IFIP TC 2\/WG 2.3 Verified Software: Theories, Tools, Experiments, VSTTE","volume":"4171","author":"Meyer B.","year":"2005"},{"key":"e_1_2_1_217_1","volume-title":"Proceedings of the Symposium on Security and Privacy. IEEE Computer Society Press","author":"Millen J."},{"key":"e_1_2_1_218_1","volume-title":"Proceedings of the IEEE Symposium on Logic Programming. IEEE Computer Society Press","author":"Miller D."},{"key":"e_1_2_1_220_1","doi-asserted-by":"crossref","unstructured":"Miner P. S. Geser A. Pike L. and Maddalon J. 2004. A unified fault-tolerance protocol. In Proceedings of the Joint International Conferences on Formal Modelling and Analysis of Timed Systems FORMATS 2004 and Formal Techniques in Real-Time and Fault-Tolerant Systems FTRTFT 2004 Y. Lakhnech and S. Yovine Eds. Lecture Notes in Computer Science vol. 3253. Springer-Verlag Berlin Germany 167--182. Miner P. S. Geser A. Pike L. and Maddalon J. 2004. A unified fault-tolerance protocol. In Proceedings of the Joint International Conferences on Formal Modelling and Analysis of Timed Systems FORMATS 2004 and Formal Techniques in Real-Time and Fault-Tolerant Systems FTRTFT 2004 Y. Lakhnech and S. Yovine Eds. Lecture Notes in Computer Science vol. 3253. Springer-Verlag Berlin Germany 167--182.","DOI":"10.1007\/978-3-540-30206-3_13"},{"key":"e_1_2_1_221_1","volume-title":"CSLI Lecture Notes","volume":"30","author":"Mints G.","year":"1992"},{"key":"e_1_2_1_222_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_2_1_223_1","doi-asserted-by":"publisher","DOI":"10.1145\/96559.96570"},{"key":"e_1_2_1_224_1","volume-title":"Proceedings of the 16th Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence","volume":"1632","author":"Nadathur G."},{"key":"e_1_2_1_225_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01966091"},{"key":"e_1_2_1_226_1","unstructured":"Nederpelt R. P. Geuvers J. H. and de Vrijer R. C. 1994. Selected Papers on Automath. North-Holland Amsterdam The Netherlands. Nederpelt R. P. Geuvers J. H. and de Vrijer R. C. 1994. Selected Papers on Automath. North-Holland Amsterdam The Netherlands."},{"key":"e_1_2_1_228_1","volume-title":"Tech. Rep. STAN-CS-77-646, Computer Science Department","author":"Nelson G.","year":"1977"},{"key":"e_1_2_1_229_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_2_1_230_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_33"},{"key":"e_1_2_1_231_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217856.1217859"},{"key":"e_1_2_1_232_1","volume-title":"ESOP. Lecture Notes in Computer Science","volume":"582","author":"Nieuwenhuis R."},{"key":"e_1_2_1_233_1","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis R. and Rubio A. 2001. Paramodulation-based theorem proving. In Handbook of Automated Reasoning. Elsevier Science Amsterdam The Netherlands 371--443. Nieuwenhuis R. and Rubio A. 2001. Paramodulation-based theorem proving. In Handbook of Automated Reasoning. Elsevier Science Amsterdam The Netherlands 371--443.","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"e_1_2_1_234_1","doi-asserted-by":"crossref","unstructured":"Nipkow T. Paulson L. C. and Wenzel M. 2002. Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer-Verlag Berlin Germany. (Isabelle home page: http:\/\/isabelle.in.tum.de\/.) Nipkow T. Paulson L. C. and Wenzel M. 2002. Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer-Verlag Berlin Germany. (Isabelle home page: http:\/\/isabelle.in.tum.de\/.)","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_2_1_235_1","doi-asserted-by":"crossref","unstructured":"O'Connor R. 2005. Essential incompleteness of arithmetic verified by Coq. CoRR abs\/cs\/0505034. informal publication. O'Connor R. 2005. Essential incompleteness of arithmetic verified by Coq. CoRR abs\/cs\/0505034. informal publication.","DOI":"10.1007\/11541868_16"},{"key":"e_1_2_1_236_1","doi-asserted-by":"crossref","unstructured":"Ohlbach H. Nonnengart A. de Rijke M. and Gabbay D. 2001. Encoding two-valued nonclassical logics in classical logic. In Handbook of Automated Reasoning. Elsevier Science Amsterdam The Netherlands 1403--1486. Ohlbach H. Nonnengart A. de Rijke M. and Gabbay D. 2001. Encoding two-valued nonclassical logics in classical logic. In Handbook of Automated Reasoning. Elsevier Science Amsterdam The Netherlands 1403--1486.","DOI":"10.1016\/B978-044450813-3\/50023-0"},{"key":"e_1_2_1_237_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(80)90059-6"},{"key":"e_1_2_1_238_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.345827"},{"key":"e_1_2_1_239_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(76)90022-0"},{"key":"e_1_2_1_240_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10107-003-0387-5"},{"key":"e_1_2_1_241_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the International Conference on Typed Lambda Calculi and Applications","author":"Paulin-Mohring C."},{"key":"e_1_2_1_242_1","doi-asserted-by":"publisher","DOI":"10.5555\/353677.353681"},{"key":"e_1_2_1_243_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541"},{"key":"e_1_2_1_244_1","doi-asserted-by":"publisher","DOI":"10.1112\/S1461157000000449"},{"key":"e_1_2_1_245_1","first-page":"1063","article-title":"Logical frameworks. In Handbook of Automated Reasoning, vol. II. Elsevier Science, Amsterdam, The Netherlands","volume":"17","author":"Pfenning F.","year":"2001","journal-title":"Chapter"},{"key":"e_1_2_1_246_1","volume-title":"Proceedings of the 16th International Conference on Automated Deduction (CADE-16)","volume":"1632","author":"Pfenning F."},{"key":"e_1_2_1_247_1","volume-title":"Proceedings of the 8th International Computer Aided Verification Conference. Lecture Notes in Computer Science, Springer-Verlag","author":"Pnueli A."},{"key":"e_1_2_1_248_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1755-2567.1960.tb00558.x"},{"key":"e_1_2_1_249_1","doi-asserted-by":"publisher","DOI":"10.1145\/135226.135233"},{"key":"e_1_2_1_250_1","doi-asserted-by":"publisher","DOI":"10.5555\/174904.174910"},{"key":"e_1_2_1_251_1","first-page":"595","article-title":"Decidable theories. In Handbook of Mathematical Logic. Studies in Logic and the Foundations of Mathematics, vol. 90. North-Holland, Amsterdam, The Netherlands","volume":"8","author":"Rabin M. O.","year":"1978","journal-title":"Chapter"},{"key":"e_1_2_1_252_1","doi-asserted-by":"publisher","DOI":"10.5555\/647764.735695"},{"key":"e_1_2_1_253_1","unstructured":"Riazanov A. and Voronkov A. 2002. The design and implementation of VAMPIRE. AI Communications: Special issue on CASC 15 2 (Sept.) 91--110. Riazanov A. and Voronkov A. 2002. The design and implementation of VAMPIRE. AI Communications: Special issue on CASC 15 2 (Sept.) 91--110."},{"key":"e_1_2_1_254_1","unstructured":"Robinson A. and Voronkov A. Eds. 2001. Handbook of Automated Reasoning. Elsevier Science Amsterdam The Netherlands. Robinson A. and Voronkov A. Eds. 2001. Handbook of Automated Reasoning. Elsevier Science Amsterdam The Netherlands."},{"key":"e_1_2_1_255_1","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"e_1_2_1_256_1","unstructured":"Robinson L. Levitt K. N. and Silverberg B. A. 1979. The HDM Handbook. Computer Science Laboratory SRI International Menlo Park CA. Three Volumes. Robinson L. Levitt K. N. and Silverberg B. A. 1979. The HDM Handbook. Computer Science Laboratory SRI International Menlo Park CA. Three Volumes."},{"key":"e_1_2_1_257_1","volume-title":"Proceedings of the 1992 Workshop on Types for Proofs and Programs","author":"Rudnicki P.","year":"1992"},{"key":"e_1_2_1_258_1","volume-title":"Tech. Rep. CSL-SRI-04-01, SRI International, Computer Science Laboratory, 333 Ravenswood Ave","author":"Ruess H.","year":"2004"},{"key":"e_1_2_1_259_1","volume-title":"Proceedings of the Symposium on Computer-Aided Verification, CAV '96","volume":"1102","author":"Rue\u00df H."},{"key":"e_1_2_1_260_1","unstructured":"Russell B. 1903. The Principles of Mathematics. Cambridge University Press Cambridge MA. Russell B. 1903. The Principles of Mathematics. Cambridge University Press Cambridge MA."},{"key":"e_1_2_1_261_1","doi-asserted-by":"publisher","DOI":"10.2307\/2369948"},{"key":"e_1_2_1_262_1","first-page":"3","article-title":"A mechanical proof of quadratic reciprocity","volume":"8","author":"Russinoff D. M.","year":"1988","journal-title":"J. Automat. Reason."},{"key":"e_1_2_1_263_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008669628911"},{"key":"e_1_2_1_264_1","unstructured":"Ryan L. 2004. Efficient algorithms for clause-learning SAT solvers. M.S. thesis Simon Fraser University. Ryan L. 2004. Efficient algorithms for clause-learning SAT solvers. M.S. thesis Simon Fraser University."},{"key":"e_1_2_1_265_1","doi-asserted-by":"publisher","DOI":"10.5555\/647282.722913"},{"key":"e_1_2_1_266_1","volume-title":"Proceedings of the International Conference on Computer-Aided Verification, CAV'97","volume":"1254","author":"Sa\u00efdi H."},{"key":"e_1_2_1_267_1","volume-title":"Proceedings of the International Conference on Computer-Aided Verification, CAV '99","volume":"1633","author":"Sa\u00efdi H."},{"key":"e_1_2_1_268_1","article-title":"E\u2014A brainiac theorem prover","volume":"15","author":"Schulz S.","year":"2002","journal-title":"J. AI Communi."},{"key":"e_1_2_1_269_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90095-B"},{"key":"e_1_2_1_270_1","unstructured":"Shankar N. 1994. Metamathematics Machines and G\u00f6del's Proof. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press Cambridge UK. Shankar N. 1994. Metamathematics Machines and G\u00f6del's Proof. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press Cambridge UK."},{"key":"e_1_2_1_271_1","doi-asserted-by":"publisher","DOI":"10.1007\/11590156_4"},{"key":"e_1_2_1_272_1","volume-title":"International Conference on Rewriting Techniques and Applications (RTA '02)","volume":"2378","author":"Shankar N."},{"key":"e_1_2_1_273_1","doi-asserted-by":"publisher","DOI":"10.5555\/646186.683237"},{"key":"e_1_2_1_274_1","unstructured":"Shoenfield J. R. 1967. Mathematical Logic. Addison-Wesley Reading MA. Shoenfield J. R. 1967. Mathematical Logic. Addison-Wesley Reading MA."},{"key":"e_1_2_1_275_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359570"},{"key":"e_1_2_1_276_1","doi-asserted-by":"publisher","DOI":"10.1145\/2422.322411"},{"key":"e_1_2_1_277_1","series-title":"Lecture Notes in Computer Science","volume-title":"STP: A mechanized logic for specification and verification. In Proceedings of the 6th International Conference on Automated Deduction (CADE)","author":"Shostak R. E.","year":"1982"},{"key":"e_1_2_1_278_1","doi-asserted-by":"crossref","unstructured":"Siekmann J. and Wrightson G. Eds. 1983. Automation of Reasoning: Classical Papers on Computational Logic Volumes 1&amp;2. Springer-Verlag Berlin Germany. Siekmann J. and Wrightson G. Eds. 1983. Automation of Reasoning: Classical Papers on Computational Logic Volumes 1&amp;2. Springer-Verlag Berlin Germany.","DOI":"10.1007\/978-3-642-81952-0"},{"key":"e_1_2_1_279_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-004-9424-1"},{"key":"e_1_2_1_280_1","volume-title":"From Frege to G\u00f6del: A Sourcebook of Mathematical Logic","author":"Skolem T.","year":"1879"},{"key":"e_1_2_1_281_1","unstructured":"Skolem T. A. 1962. Abstract Set Theory. Number 8 in Notre Dame Mathematical Lectures. University of Notre Dame Press Notre Dame IN. Skolem T. A. 1962. Abstract Set Theory. Number 8 in Notre Dame Mathematical Lectures. University of Notre Dame Press Notre Dame IN."},{"key":"e_1_2_1_282_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_6"},{"key":"e_1_2_1_283_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.58788"},{"key":"e_1_2_1_285_1","doi-asserted-by":"crossref","unstructured":"Smullyan R. M. 1968. First-Order Logic. Springer-Verlag Berlin Germany. (Republished by Courier Dover Publications 1995.) Smullyan R. M. 1968. First-Order Logic. Springer-Verlag Berlin Germany. (Republished by Courier Dover Publications 1995.)","DOI":"10.1007\/978-3-642-86718-7"},{"key":"e_1_2_1_286_1","unstructured":"Spivey J. M. Ed. 1993. The Z Notation: A Reference Manual second ed. Prentice-Hall International Series in Computer Science. Prentice-Hall Hemel Hempstead UK. Spivey J. M. Ed. 1993. The Z Notation: A Reference Manual second ed. Prentice-Hall International Series in Computer Science. Prentice-Hall Hemel Hempstead UK."},{"key":"e_1_2_1_287_1","doi-asserted-by":"publisher","DOI":"10.5555\/95411"},{"key":"e_1_2_1_288_1","doi-asserted-by":"publisher","DOI":"10.5555\/6364.6365"},{"key":"e_1_2_1_289_1","unstructured":"Stickel M. E. Waldinger R. J. and Chaudhri V. K. 2000. A guide to SNARK. Tech. Note SRI International Artificial Intelligence Center. Stickel M. E. Waldinger R. J. and Chaudhri V. K. 2000. A guide to SNARK. Tech. Note SRI International Artificial Intelligence Center."},{"key":"e_1_2_1_290_1","series-title":"Lecture Notes in Computer Science","volume-title":"CVC: A cooperating validity checker. In Proceedings of the International Conference on Computer-Aided Verification, CAV'02","author":"Stump A.","year":"2002"},{"key":"e_1_2_1_291_1","doi-asserted-by":"crossref","unstructured":"Stump A. Barrett C. W. Dill D. L. and Levitt J. R. 2001. A decision procedure for an extensional theory of arrays. In LICS. 29--37. Stump A. Barrett C. W. Dill D. L. and Levitt J. R. 2001. A decision procedure for an extensional theory of arrays. In LICS. 29--37.","DOI":"10.1109\/LICS.2001.932480"},{"key":"e_1_2_1_292_1","unstructured":"Suppes P. 1972. Axiomatic Set Theory. Dover Publications Inc. New York NY. Suppes P. 1972. Axiomatic Set Theory. Dover Publications Inc. New York NY."},{"key":"e_1_2_1_293_1","doi-asserted-by":"publisher","DOI":"10.5555\/1143139.1143142"},{"key":"e_1_2_1_294_1","unstructured":"Szabo M. E. Ed. 1969. The Collected Papers of Gerhard Gentzen. North-Holland Amsterdam The Netherlands. Szabo M. E. Ed. 1969. The Collected Papers of Gerhard Gentzen. North-Holland Amsterdam The Netherlands."},{"key":"e_1_2_1_295_1","doi-asserted-by":"publisher","DOI":"10.1145\/321879.321884"},{"key":"e_1_2_1_296_1","unstructured":"Tarski A. 1948. A Decision Method for Elementary Algebra and Geometry. University of California Press. Tarski A. 1948. A Decision Method for Elementary Algebra and Geometry. University of California Press."},{"key":"e_1_2_1_297_1","unstructured":"Tarski A. Mostowski A. and Robinson R. M. 1971. Undecidable Theories. North-Holland Amsterdam The Netherlands. Tarski A. Mostowski A. and Robinson R. M. 1971. Undecidable Theories. North-Holland Amsterdam The Netherlands."},{"key":"e_1_2_1_298_1","unstructured":"The Coq Development Team. 2009. The Coq proof assistant reference manual version 8.2. Tech. rep. INRIA. Feb. The Coq Development Team. 2009. The Coq proof assistant reference manual version 8.2. Tech. rep. INRIA. Feb."},{"key":"e_1_2_1_299_1","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Proceedings of 15th International Conference on Automated Deduction (CADE)","author":"Th\u00e9ry L."},{"key":"e_1_2_1_300_1","doi-asserted-by":"publisher","DOI":"10.1007\/11538363_18"},{"key":"e_1_2_1_301_1","volume-title":"Kodkod: A relational model finder. In Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS","author":"Torlak E.","year":"2007"},{"key":"e_1_2_1_302_1","unstructured":"Troelstra A. and van Dalen D. 1988. Constructivity in Mathematics. North-Holland Amsterdam The Netherlands. Troelstra A. and van Dalen D. 1988. Constructivity in Mathematics. North-Holland Amsterdam The Netherlands."},{"key":"e_1_2_1_303_1","doi-asserted-by":"crossref","unstructured":"Tseitin G. 1968. On the complexity of derivation in propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic Part 11. Otdel Leningrad Russia 115--125. (Reprinted in Siekmann and Wrightson {1983}.) Tseitin G. 1968. On the complexity of derivation in propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic Part 11. Otdel Leningrad Russia 115--125. (Reprinted in Siekmann and Wrightson {1983}.)","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"e_1_2_1_304_1","volume-title":"The Undecidable","author":"Turing A. M.","year":"1937"},{"key":"e_1_2_1_305_1","volume-title":"Elements of Classical Logic","author":"van Benthem J.","year":"1983"},{"key":"e_1_2_1_306_1","volume-title":"Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems: TACAS","volume":"2031","author":"van den Berg J.","year":"2001"},{"key":"e_1_2_1_307_1","unstructured":"van Heijenoort J. Ed. 1967. From Frege to G\u00f6del: A Sourcebook of Mathematical Logic 1879--1931. Harvard University Press Cambridge MA. van Heijenoort J. Ed. 1967. From Frege to G\u00f6del: A Sourcebook of Mathematical Logic 1879--1931. Harvard University Press Cambridge MA."},{"key":"e_1_2_1_308_1","unstructured":"van Leeuwen J. Ed. 1990. In Handbook of Theoretical Computer Science. vol. B: Formal Models and Semantics. Elsevier and MIT Press Amsterdam The Netherlands and Cambridge MA. van Leeuwen J. Ed. 1990. In Handbook of Theoretical Computer Science. vol. B: Formal Models and Semantics. Elsevier and MIT Press Amsterdam The Netherlands and Cambridge MA."},{"key":"e_1_2_1_309_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-5662-3"},{"key":"e_1_2_1_310_1","doi-asserted-by":"publisher","DOI":"10.1007\/11591191_23"},{"key":"e_1_2_1_311_1","volume-title":"Proceedings of the 18th International Conference on Automated Deduction\u2014CADE-18","volume":"2392","author":"Weidenbach C."},{"key":"e_1_2_1_312_1","volume-title":"Proceedings 16th International Joint Conference on Artificial Intelligence (IJCAI).","author":"Weld D."},{"key":"e_1_2_1_313_1","doi-asserted-by":"publisher","DOI":"10.5555\/646526.694887"},{"key":"e_1_2_1_314_1","doi-asserted-by":"crossref","unstructured":"Weyhrauch R. W. 1980. Prolegomena to a theory of mechanized formal reasoning. Artif. Intell. 13 1 and 2 (Apr.) 133--170. Weyhrauch R. W. 1980. Prolegomena to a theory of mechanized formal reasoning. Artif. Intell. 13 1 and 2 (Apr.) 133--170.","DOI":"10.1016\/0004-3702(80)90015-6"},{"key":"e_1_2_1_315_1","doi-asserted-by":"publisher","DOI":"10.21236\/ADA006898"},{"key":"e_1_2_1_316_1","unstructured":"Wies T. Kuncak V. Zee K. Podelski A. and Rinard M. C. 2006. On verifying complex properties using symbolic shape analysis. CoRR abs\/cs\/0609104. informal publication. Wies T. Kuncak V. Zee K. Podelski A. and Rinard M. C. 2006. On verifying complex properties using symbolic shape analysis. CoRR abs\/cs\/0609104. informal publication."},{"key":"e_1_2_1_317_1","doi-asserted-by":"publisher","DOI":"10.1016\/0097-3165(76)90055-8"},{"key":"e_1_2_1_318_1","unstructured":"Yoeli M. Ed. 1990. Formal Verification of Hardware Design. IEEE Computer Society Press Los Alamitos CA. Yoeli M. Ed. 1990. Formal Verification of Hardware Design. IEEE Computer Society Press Los Alamitos CA."},{"key":"e_1_2_1_319_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01449999"},{"key":"e_1_2_1_320_1","doi-asserted-by":"publisher","DOI":"10.5555\/648233.753307"},{"key":"e_1_2_1_321_1","volume-title":"Proceedings of the 19th International Conference on Automated Deduction CADE-19","author":"Zhang L."},{"key":"e_1_2_1_322_1","doi-asserted-by":"publisher","DOI":"10.5555\/789083.1022835"}],"container-title":["ACM Computing Surveys"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1592434.1592437","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1592434.1592437","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:17:47Z","timestamp":1750249067000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1592434.1592437"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,10]]},"references-count":316,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2009,10]]}},"alternative-id":["10.1145\/1592434.1592437"],"URL":"https:\/\/doi.org\/10.1145\/1592434.1592437","relation":{},"ISSN":["0360-0300","1557-7341"],"issn-type":[{"value":"0360-0300","type":"print"},{"value":"1557-7341","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,10]]},"assertion":[{"value":"2009-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-10-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}