{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T23:50:17Z","timestamp":1725580217582},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642203978"},{"type":"electronic","value":"9783642203985"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-20398-5_10","type":"book-chapter","created":{"date-parts":[[2011,4,6]],"date-time":"2011-04-06T19:29:49Z","timestamp":1302118189000},"page":"116-130","source":"Crossref","is-referenced-by-count":6,"title":["Integrating an Automated Theorem Prover into Agda"],"prefix":"10.1007","author":[{"given":"Simon","family":"Foster","sequence":"first","affiliation":[]},{"given":"Georg","family":"Struth","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/11559306_17","volume-title":"Frontiers of Combining Systems","author":"A. Abel","year":"2005","unstructured":"Abel, A., Coquand, T., Norell, U.: Connecting a logical framework to a first-order logic prover. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol.\u00a03717, pp. 285\u2013301. Springer, Heidelberg (2005)"},{"key":"10_CR2","first-page":"1","volume-title":"Resolution of Equations in Algebraic Structures","author":"L. Bachmair","year":"1989","unstructured":"Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion Without Failure. In: Resolution of Equations in Algebraic Structures, pp. 1\u201330. Academic Press, London (1989)"},{"key":"10_CR3","volume-title":"The Algebra of Programming","author":"R. Bird","year":"1997","unstructured":"Bird, R., de Moor, O.: The Algebra of Programming. Prentice-Hall, Englewood Cliffs (1997)"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-14052-5_11","volume-title":"Interactive Theorem Proving","author":"J.C. Blanchette","year":"2010","unstructured":"Blanchette, J.C., Nipkow, T.: Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 131\u2013146. Springer, Heidelberg (2010)"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-14203-1_9","volume-title":"Automated Reasoning","author":"S. B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Nipkow, T.: Sledgehammer: Judgement day. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 107\u2013121. Springer, Heidelberg (2010)"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-642-14052-5_14","volume-title":"Interactive Theorem Proving","author":"S. B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 179\u2013194. Springer, Heidelberg (2010)"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-642-03359-9_6","volume-title":"Theorem Proving in Higher Order Logics","author":"A. Bove","year":"2009","unstructured":"Bove, A., Dybjer, P., Norell, U.: A brief overview of agda \u2013 A functional language with dependent types. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 73\u201378. Springer, Heidelberg (2009)"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Foster, S., Struth, G.: Integrating an automated theorem prover into Agda. Tech. Rep. CS-10-06, Department of Computer Science, University of Sheffield (2010)","DOI":"10.1007\/978-3-642-20398-5_10"},{"key":"10_CR9","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/BF01360048","volume":"132","author":"R. Harrop","year":"1956","unstructured":"Harrop, R.: On disjunctions and existential statements in intuitionistic systems of logic. Mathematische Annalen\u00a0132, 347\u2013361 (1956)","journal-title":"Mathematische Annalen"},{"issue":"2","key":"10_CR10","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1023\/A:1005872405899","volume":"18","author":"T. Hillenbrand","year":"1997","unstructured":"Hillenbrand, T., Buch, A., Vogt, R., L\u00f6chner, B.: Waldmeister: High performance equational deduction. Journal of Automated Reasoning\u00a018(2), 265\u2013270 (1997)","journal-title":"Journal of Automated Reasoning"},{"key":"10_CR11","unstructured":"Hurd, J.: System description: The Metis proof tactic. In: Benzm\u00fcller, C., Harrison, J., Sch\u00fcrmann, C. (eds.) ESHOL 2005, pp. 103\u2013104, arXiv.org (2005)"},{"key":"10_CR12","series-title":"LNCS","volume-title":"RaMiCS 2011","author":"W. Kahl","year":"2011","unstructured":"Kahl, W.: Dependently-typed formalisation of relation-algebraic abstractions. In: de Swart, H.C.M. (ed.) RaMiCS 2011. LNCS, Springer, Heidelberg (to appear 2011)"},{"key":"10_CR13","unstructured":"Kanso, K., Setzer, A.: Integrating automated and interactive theorem proving in type theory. In: Bendisposto, J., Leuschel, M., Roggenbach, M. (eds.) AVOCS 2010 (2010)"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1007\/11617990_10","volume-title":"TYPES","author":"F. Lindblad","year":"2006","unstructured":"Lindblad, F., Benke, M.: A tool for automated theorem proving in Agda. In: Filli\u00e2tre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol.\u00a03839, pp. 154\u2013169. Springer, Heidelberg (2006)"},{"issue":"1","key":"10_CR15","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1017\/S0956796803004829","volume":"14","author":"C. McBride","year":"2004","unstructured":"McBride, C., McKinna, J.: The view from the left. Journal of Functional Programming\u00a014(1), 69\u2013111 (2004)","journal-title":"Journal of Functional Programming"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/978-3-540-70594-9_15","volume-title":"Mathematics of Program Construction","author":"S.C. Mu","year":"2008","unstructured":"Mu, S.C., Ko, H.S., Jansson, P.: Algebra of programming using dependent types. In: Audebaud, P., Paulin-Mohring, C. (eds.) MPC 2008. LNCS, vol.\u00a05133, pp. 268\u2013283. Springer, Heidelberg (2008)"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"10_CR18","series-title":"LNAI","first-page":"748","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS (LNAI), vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"10_CR19","volume-title":"Term Rewriting Systems","author":"Terese","year":"2003","unstructured":"Terese: Term Rewriting Systems. Cambridge University Press, Cambridge (2003)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-20398-5_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,21]],"date-time":"2021-11-21T06:48:30Z","timestamp":1637477310000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-20398-5_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642203978","9783642203985"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-20398-5_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}