{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T17:14:35Z","timestamp":1725988475188},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319999562"},{"type":"electronic","value":"9783319999579"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-99957-9_4","type":"book-chapter","created":{"date-parts":[[2018,8,21]],"date-time":"2018-08-21T08:26:31Z","timestamp":1534839991000},"page":"54-69","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Formalizing Some \u201cSmall\u201d Finite Models of Projective Geometry in Coq"],"prefix":"10.1007","author":[{"given":"David","family":"Braun","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicolas","family":"Magaud","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pascal","family":"Schreck","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,8,22]]},"reference":[{"key":"4_CR1","unstructured":"Armand, M., Gr\u00e9goire, G., Keller, B., Th\u00e9ry, L., Werner, B.: Verifying SAT and SMT in Coq for a fully automated decision procedure. In: International Workshop on Proof-Search in Axiomatic Theories and Type Theories (PSATTT 2011) (2011)"},{"key":"4_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511665608","volume-title":"Combinatorics of Finite Geometries","author":"LM Batten","year":"1997","unstructured":"Batten, L.M.: Combinatorics of Finite Geometries. Cambridge University Press, Cambridge (1997)"},{"key":"4_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development, Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development, Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-662-07964-5"},{"key":"4_CR4","unstructured":"Braun, D., Magaud, N., Schreck, P.: An equivalence proof between rank theory and incidence projective geometry. In: Automated Deduction in Geometry (ADG 2016), pp. 62\u201377 (2016)"},{"volume-title":"Handbook of Incidence Geometry","year":"1995","key":"4_CR5","unstructured":"Buekenhout, F. (ed.): Handbook of Incidence Geometry. North Holland, Amsterdam (1995)"},{"key":"4_CR6","unstructured":"Coq Development Team: The Coq Proof Assistant Reference Manual, Version 8.6. LogiCal Project (2017)"},{"key":"4_CR7","volume-title":"Projective Geometry","author":"HSM Coxeter","year":"2003","unstructured":"Coxeter, H.S.M.: Projective Geometry. Springer, New York (2003)"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"issue":"2","key":"4_CR9","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1090\/S0002-9947-1943-0008892-4","volume":"54","author":"M Hall","year":"1943","unstructured":"Hall, M.: Projective planes. Trans. Am. Math. Soc. 54(2), 229\u2013277 (1943)","journal-title":"Trans. Am. Math. Soc."},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39799-8_1"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-642-21046-4_7","volume-title":"Automated Deduction in Geometry","author":"N Magaud","year":"2011","unstructured":"Magaud, N., Narboux, J., Schreck, P.: Formalizing projective plane geometry in Coq. In: Sturm, T., Zengler, C. (eds.) ADG 2008. LNCS (LNAI), vol. 6301, pp. 141\u2013162. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-21046-4_7"},{"issue":"8","key":"4_CR12","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1016\/j.comgeo.2010.06.004","volume":"45","author":"N Magaud","year":"2012","unstructured":"Magaud, N., Narboux, J., Schreck, P.: A case study in formalizing projective geometry in Coq: Desargues theorem. Comput. Geom.: Theor. Appl. 45(8), 406\u2013424 (2012)","journal-title":"Comput. Geom.: Theor. Appl."},{"key":"4_CR13","unstructured":"Mahboubi, A., Tassi, E.: Mathematical Components. Draft (2016)"},{"issue":"5","key":"4_CR14","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1142\/S0218195906002130","volume":"16","author":"D Michelucci","year":"2006","unstructured":"Michelucci, D., Schreck, P.: Incidence constraints: a combinatorial approach. Int. J. Comput. Geom. Appl. 16(5), 443\u2013460 (2006)","journal-title":"Int. J. Comput. Geom. Appl."},{"issue":"2","key":"4_CR15","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1090\/S0002-9947-1902-1500595-3","volume":"3","author":"FR Moulton","year":"1902","unstructured":"Moulton, F.R.: A simple non-desarguesian plane geometry. Trans. Am. Math. Soc. 3(2), 192\u2013195 (1902)","journal-title":"Trans. Am. Math. Soc."},{"key":"4_CR16","volume-title":"Matroid Theory","author":"JG Oxley","year":"2006","unstructured":"Oxley, J.G.: Matroid Theory, vol. 3. Oxford University Press, Oxford (2006)"},{"issue":"4","key":"4_CR17","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reason. 43(4), 337 (2009)","journal-title":"J. Autom. Reason."},{"key":"4_CR18","unstructured":"Tebbi, T., Gross, J.: A profiler for Ltac. In: Coq PL Workshop 2015 (2015)"}],"container-title":["Lecture Notes in Computer Science","Artificial Intelligence and Symbolic Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-99957-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,8,21]],"date-time":"2018-08-21T08:27:32Z","timestamp":1534840052000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-99957-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319999562","9783319999579"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99957-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}