{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T04:04:07Z","timestamp":1725595447025},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642226724"},{"type":"electronic","value":"9783642226731"}],"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-22673-1_4","type":"book-chapter","created":{"date-parts":[[2011,7,13]],"date-time":"2011-07-13T07:49:15Z","timestamp":1310543355000},"page":"45-57","source":"Crossref","is-referenced-by-count":1,"title":["Proof Assistant Decision Procedures for Formalizing Origami"],"prefix":"10.1007","author":[{"given":"Cezary","family":"Kaliszyk","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tetsuo","family":"Ida","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/3-540-44755-5_4","volume-title":"Theorem Proving in Higher Order Logics","author":"A. Adams","year":"2001","unstructured":"Adams, A., Dunstan, M., Gottliebsen, H., Kelsey, T., Martin, U., Owre, S.: Computer algebra meets automated theorem proving: Integrating Maple and PVS. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, pp. 27\u201342. Springer, Heidelberg (2001)"},{"issue":"2","key":"4_CR2","first-page":"12","volume":"30","author":"H. Aslaksen","year":"1996","unstructured":"Aslaksen, H.: Multiple-valued complex functions and computer algebra. SIGSAM Bulletin (ACM Special Interest Group on Symbolic and Algebraic Manipulation)\u00a030(2), 12\u201320 (1996)","journal-title":"SIGSAM Bulletin (ACM Special Interest Group on Symbolic and Algebraic Manipulation)"},{"key":"4_CR3","unstructured":"Barras, B., Boutin, S., Cornes, C., Courant, J., Coscoy, Y., Delahaye, D., de Rauglaudre, D., Filli\u00e2tre, J.C., Gim\u00e9nez, E., Herbelin, H., et al.: The Coq Proof Assistant Reference Manual Version\u00a08.3. LogiCal project (2010), http:\/\/coq.inria.fr\/refman\/"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-642-14128-7_17","volume-title":"Intelligent Computer Mathematics","author":"C. Cohen","year":"2010","unstructured":"Cohen, C., Mahboubi, A.: A formal quantifier elimination for algebraically closed fields. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) AISC 2010. LNCS, vol.\u00a06167, pp. 189\u2013203. Springer, Heidelberg (2010)"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Ghourabi, F., Ida, T., Kasem, A.: Proof documents for automated origami theorem proving. Submitted to ADG 2011 post-proceedings (2011)","DOI":"10.1007\/978-3-642-25070-5_5"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Formal Methods in Computer-Aided Design","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: HOL Light: A tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 265\u2013269. Springer, Heidelberg (1996)"},{"key":"4_CR7","unstructured":"Huzita, H.: Axiomatic development of origami geometry. In: Huzita, H. (ed.) Proceedings of the First International Meeting of Origami Science and Technology, pp. 143\u2013158 (1989)"},{"key":"4_CR8","unstructured":"Huzita, H.: The trisection of a given angle solved by the geometry of origami. In: Huzita, H. (ed.) Proceedings of the First International Meeting of Origami Science and Technology, pp. 195\u2013214 (1989)"},{"key":"4_CR9","unstructured":"Ida, T., Ghourabi, F., Kasem, A., Kaliszyk, C.: Towards theory of origami fold. Submitted to ISSAC (2011)"},{"issue":"1-2","key":"4_CR10","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10817-009-9135-8","volume":"44","author":"P. Janicic","year":"2010","unstructured":"Janicic, P.: Geometry constructions language. J. Autom. Reasoning\u00a044(1-2), 3\u201324 (2010)","journal-title":"J. Autom. Reasoning"},{"key":"4_CR11","unstructured":"Justin, J.: R\u00e9solution par le pliage de l\u2019\u00e9quation du troisi\u00e8me degr\u00e9 et applications g\u00e9om\u00e9triques. In: Huzita, H. (ed.) Proceedings of the First International Meeting of Origami Science and Technology, pp. 251\u2013261 (1989)"},{"key":"4_CR12","unstructured":"Kaliszyk, C.: Prototype computer algebra system in HOL Light, http:\/\/score.cs.tsukuba.ac.jp\/~kaliszyk\/holcas.php"},{"key":"4_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-540-73086-6_8","volume-title":"Towards Mechanized Mathematical Assistants","author":"C. Kaliszyk","year":"2007","unstructured":"Kaliszyk, C., Wiedijk, F.: Certified computer algebra on top of an interactive theorem prover. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM\/CALCULEMUS 2007. LNCS (LNAI), vol.\u00a04573, pp. 94\u2013105. Springer, Heidelberg (2007)"},{"issue":"1","key":"4_CR14","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/s11704-008-0009-8","volume":"2","author":"A. Kasem","year":"2008","unstructured":"Kasem, A., Ida, T.: Computational origami environment on the Web. Frontiers of Computer Science in China\u00a02(1), 39\u201354 (2008)","journal-title":"Frontiers of Computer Science in China"},{"key":"4_CR15","unstructured":"Kasem, A., Ida, T., Takahashi, H., Marin, M., Ghourabi, F.: E-origami system Eos. In: Proceedings of the Annual Symposium of Japan Society for Software Science and Technology, JSSST, Tokyo, Japan (September 2006)"},{"key":"4_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/11532231_22","volume-title":"Automated Deduction \u2013 CADE-20","author":"S. McLaughlin","year":"2005","unstructured":"McLaughlin, S., Harrison, J.: A proof-producing decision procedure for real arithmetic. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 295\u2013314. Springer, Heidelberg (2005)"},{"issue":"1","key":"4_CR17","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1016\/j.jsc.2009.07.002","volume":"45","author":"I. Medina-Bulo","year":"2010","unstructured":"Medina-Bulo, I., Palomo-Lozano, F., Ruiz-Reina, J.-L.: A verified Common Lisp implementation of Buchberger\u2019s algorithm in ACL2. J. Symb. Comput.\u00a045(1), 96\u2013123 (2010)","journal-title":"J. Symb. Comput."},{"issue":"2","key":"4_CR18","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10817-007-9071-4","volume":"39","author":"J. Narboux","year":"2007","unstructured":"Narboux, J.: A graphical user interface for formal proofs in geometry. J. Autom. Reasoning\u00a039(2), 161\u2013180 (2007)","journal-title":"J. Autom. Reasoning"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T. (eds.): Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"4_CR20","unstructured":"Pottier, L.: Connecting Gr\u00f6bner bases programs with Coq to do proofs in algebra, geometry and arithmetics. In: Rudnicki, P., Sutcliffe, G., Konev, B., Schmidt, R.A., Schulz, S. (eds.) LPAR Workshops. CEUR Workshop Proceedings, vol.\u00a0418, CEUR-WS.org (2008)"},{"key":"4_CR21","unstructured":"Critique of the Mathematical Abilities of CA Systems. In: Wester, M. (ed.) Contents of Computer Algebra Systems: A Practical Guide, John Wiley & Sons, Chichester (1999)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22673-1_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,12]],"date-time":"2019-06-12T19:19:47Z","timestamp":1560367187000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22673-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642226724","9783642226731"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22673-1_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}