Koutsoukou-Argyraki, Angeliki Formalising mathematics – in praxis; a mathematician’s first experiences with Isabelle/HOL and the why and how of getting started. (English) Zbl 07323056 Jahresber. Dtsch. Math.-Ver. 123, No. 1, 3-26 (2021). MSC: 03B35 68V15 68V20 68V35 PDF BibTeX XML Cite \textit{A. Koutsoukou-Argyraki}, Jahresber. Dtsch. Math.-Ver. 123, No. 1, 3--26 (2021; Zbl 07323056) Full Text: DOI
Zammit-Mangion, Andrew; Rougier, Jonathan Multi-scale process modelling and distributed computation for spatial data. (English) Zbl 1452.62364 Stat. Comput. 30, No. 6, 1609-1627 (2020). MSC: 62H11 05C15 62-08 62M20 62P12 65C05 PDF BibTeX XML Cite \textit{A. Zammit-Mangion} and \textit{J. Rougier}, Stat. Comput. 30, No. 6, 1609--1627 (2020; Zbl 1452.62364) Full Text: DOI
Doczkal, Christian; Pous, Damien Graph theory in Coq: minors, treewidth, and isomorphisms. (English) Zbl 07268887 J. Autom. Reasoning 64, No. 5, 795-825 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{C. Doczkal} and \textit{D. Pous}, J. Autom. Reasoning 64, No. 5, 795--825 (2020; Zbl 07268887) Full Text: DOI
Sant’Ana da Silva, Eduardo; Pedrini, Helio Vertex coloring of a graph for memory constrained scenarios. (English) Zbl 1455.68148 Math. Comput. Sci. 14, No. 1, 9-17 (2020). Reviewer: Charles J. Colbourn (Tempe) MSC: 68R10 05C15 68W25 PDF BibTeX XML Cite \textit{E. Sant'Ana da Silva} and \textit{H. Pedrini}, Math. Comput. Sci. 14, No. 1, 9--17 (2020; Zbl 1455.68148) Full Text: DOI
Mainzer, Klaus From mathesis universalis to provability, computability, and constructivity. (English) Zbl 07229615 Centrone, Stefania (ed.) et al., Mathesis universalis, computability and proof. Based on the Humboldt-Kolleg “Proof theory as mathesis universalis”, held at the German-Italian Centre for European Excellence, Villa Vigoni, Loveno di Menaggio, Como, Italy, July 24–28, 2017. Cham: Springer (ISBN 978-3-030-20446-4/hbk; 978-3-030-20447-1/ebook). Synthese Library 412, 203-234 (2019). MSC: 03A05 PDF BibTeX XML Cite \textit{K. Mainzer}, Synth. Libr. 412, 203--234 (2019; Zbl 07229615) Full Text: DOI
Gunther, Emmanuel; Pagano, Miguel; Sánchez Terraf, Pedro First steps towards a formalization of forcing. (English) Zbl 1434.03029 Accattoli, Beniamino (ed.) et al., Proceedings of the 13th workshop on logical and semantic frameworks with applications, LSFA 18, Fortaleza, Brazil, September 26–28, 2018. Amsterdam: Elsevier. Electron. Notes Theor. Comput. Sci. 344, 119-136 (2019). MSC: 03B35 03E35 68V20 PDF BibTeX XML Cite \textit{E. Gunther} et al., Electron. Notes Theor. Comput. Sci. 344, 119--136 (2019; Zbl 1434.03029) Full Text: DOI
Gómez-Ramírez, Danny A. J.; Fulla, Marlon; Rivera, Ismael; Vélez, Juan D.; Gallego, Edisson Category-based co-generation of seminal concepts and results in algebra and number theory: containment-division and Goldbach rings. (English) Zbl 1455.13035 JP J. Algebra Number Theory Appl. 40, No. 5, 887-901 (2018). MSC: 13F05 13P99 PDF BibTeX XML Cite \textit{D. A. J. Gómez-Ramírez} et al., JP J. Algebra Number Theory Appl. 40, No. 5, 887--901 (2018; Zbl 1455.13035) Full Text: DOI
Grayson, Daniel R. An introduction to univalent foundations for mathematicians. (English) Zbl 06945518 Bull. Am. Math. Soc., New Ser. 55, No. 4, 427-450 (2018). MSC: 03B35 03B15 PDF BibTeX XML Cite \textit{D. R. Grayson}, Bull. Am. Math. Soc., New Ser. 55, No. 4, 427--450 (2018; Zbl 06945518) Full Text: DOI
Stump, Aaron From realizability to induction via dependent intersection. (English) Zbl 06880845 Ann. Pure Appl. Logic 169, No. 7, 637-655 (2018). MSC: 03B15 03B40 68N18 68N30 PDF BibTeX XML Cite \textit{A. Stump}, Ann. Pure Appl. Logic 169, No. 7, 637--655 (2018; Zbl 06880845) Full Text: DOI
Song, Dan; Wang, Dongming; Chen, Xiaoyu Retrieving geometric information from images: the case of hand-drawn diagrams. (English) Zbl 1411.68135 Data Min. Knowl. Discov. 31, No. 4, 934-971 (2017). MSC: 68T10 62H35 PDF BibTeX XML Cite \textit{D. Song} et al., Data Min. Knowl. Discov. 31, No. 4, 934--971 (2017; Zbl 1411.68135) Full Text: DOI
Cruz-Filipe, Luís; Larsen, Kim S.; Schneider-Kamp, Peter Formally proving size optimality of sorting networks. (English) Zbl 1425.68372 J. Autom. Reasoning 59, No. 4, 425-454 (2017). MSC: 68T15 68N18 68Q17 68Q25 68Q60 PDF BibTeX XML Cite \textit{L. Cruz-Filipe} et al., J. Autom. Reasoning 59, No. 4, 425--454 (2017; Zbl 1425.68372) Full Text: DOI
Kari, Lila; Kopecki, Steffen; Meunier, Pierre-Étienne; Patitz, Matthew J.; Seki, Shinnosuke Binary pattern tile set synthesis is NP-hard. (English) Zbl 1370.68109 Algorithmica 78, No. 1, 1-46 (2017). MSC: 68Q17 05B45 68Q80 68T15 PDF BibTeX XML Cite \textit{L. Kari} et al., Algorithmica 78, No. 1, 1--46 (2017; Zbl 1370.68109) Full Text: DOI
Kerber, Manfred; Lange, Christoph; Rowat, Colin An introduction to mechanized reasoning. (English) Zbl 1368.68289 J. Math. Econ. 66, 26-39 (2016). MSC: 68T15 03B35 91B14 91B26 PDF BibTeX XML Cite \textit{M. Kerber} et al., J. Math. Econ. 66, 26--39 (2016; Zbl 1368.68289) Full Text: DOI
Hutchinson, Joan P. Some conjectures and questions in chromatic topological graph theory. (English) Zbl 1355.05110 Gera, Ralucca (ed.) et al., Graph theory. Favorite conjectures and open problems – 1. Cham: Springer (ISBN 978-3-319-31938-4/hbk; 978-3-319-31940-7/ebook). Problem Books in Mathematics, 195-210 (2016). Reviewer: Stelian Mihalas (Timişoara) MSC: 05C15 05C10 05-02 PDF BibTeX XML Cite \textit{J. P. Hutchinson}, in: Graph theory. Favorite conjectures and open problems -- 1. Cham: Springer. 195--210 (2016; Zbl 1355.05110) Full Text: DOI
Angelini, Patrizio; Bekos, Michael A.; Kaufmann, Michael; Roselli, Vincenzo Vertex-coloring with star-defects. (English) Zbl 06576379 Kaykobad, Mohammad (ed.) et al., WALCOM: algorithms and computation. 10th international workshop, WALCOM 2016, Kathmandu, Nepal, March 29–31, 2016. Proceedings. Cham: Springer (ISBN 978-3-319-30138-9/pbk; 978-3-319-30139-6/ebook). Lecture Notes in Computer Science 9627, 40-51 (2016). MSC: 68Wxx PDF BibTeX XML Cite \textit{P. Angelini} et al., Lect. Notes Comput. Sci. 9627, 40--51 (2016; Zbl 06576379) Full Text: DOI arXiv
Dabrowski, Frédéric; Loulergue, Frédéric; Pinsard, Thomas A formal semantics of nested atomic sections with thread escape. (English) Zbl 1387.68048 Comput. Lang. Syst. Struct. 42, 2-21 (2015). MSC: 68N15 68Q55 PDF BibTeX XML Cite \textit{F. Dabrowski} et al., Comput. Lang. Syst. Struct. 42, 2--21 (2015; Zbl 1387.68048) Full Text: DOI
Ziliani, Beta; Dreyer, Derek; Krishnaswami, Neelakantan R.; Nanevski, Aleksandar; Vafeiadis, Viktor Mtac: a monad for typed tactic programming in Coq. (English) Zbl 1420.68189 J. Funct. Program. 25, Paper No. e12, 59 p. (2015). MSC: 68T15 68N30 PDF BibTeX XML Cite \textit{B. Ziliani} et al., J. Funct. Program. 25, Paper No. e12, 59 p. (2015; Zbl 1420.68189) Full Text: DOI
Pąk, Karol Improving legibility of formal proofs based on the close reference principle is NP-hard. (English) Zbl 1356.68198 J. Autom. Reasoning 55, No. 3, 295-306 (2015). MSC: 68T15 03B35 68Q17 PDF BibTeX XML Cite \textit{K. Pąk}, J. Autom. Reasoning 55, No. 3, 295--306 (2015; Zbl 1356.68198) Full Text: DOI
Konev, Boris; Lisitsa, Alexei Computer-aided proof of Erdős discrepancy properties. (English) Zbl 1344.68205 Artif. Intell. 224, 103-118 (2015). MSC: 68T15 11B30 11K38 PDF BibTeX XML Cite \textit{B. Konev} and \textit{A. Lisitsa}, Artif. Intell. 224, 103--118 (2015; Zbl 1344.68205) Full Text: DOI
Kari, Lila; Kopecki, Steffen; Meunier, Pierre-Étienne; Patitz, Matthew J.; Seki, Shinnosuke Binary pattern tile set synthesis is NP-hard. (English) Zbl 1370.68108 Halldórsson, Magnús M. (ed.) et al., Automata, languages, and programming. 42nd international colloquium, ICALP 2015, Kyoto, Japan, July 6–10, 2015. Proceedings. Part I. Berlin: Springer (ISBN 978-3-662-47671-0/pbk; 978-3-662-47672-7/ebook). Lecture Notes in Computer Science 9134, 1022-1034 (2015). MSC: 68Q17 05B45 68Q80 68T15 PDF BibTeX XML Cite \textit{L. Kari} et al., Lect. Notes Comput. Sci. 9134, 1022--1034 (2015; Zbl 1370.68108) Full Text: DOI
Asperti, Andrea Computational complexity via finite types. (English) Zbl 1354.68091 ACM Trans. Comput. Log. 16, No. 3, Article No. 26, 25 p. (2015). MSC: 68Q15 PDF BibTeX XML Cite \textit{A. Asperti}, ACM Trans. Comput. Log. 16, No. 3, Article No. 26, 25 p. (2015; Zbl 1354.68091) Full Text: DOI
Théry, Laurent (ed.); Wiedijk, Freek (ed.) Foreword to the special focus on formal proofs for mathematics and computer science. (English) Zbl 1308.00050 Math. Comput. Sci. 9, No. 1, 1-3 (2015). MSC: 00B15 68T15 68-06 PDF BibTeX XML Cite \textit{L. Théry} (ed.) and \textit{F. Wiedijk} (ed.), Math. Comput. Sci. 9, No. 1, 1--3 (2015; Zbl 1308.00050) Full Text: DOI
Dufourd, Jean-François Formal study of functional orbits in finite domains. (English) Zbl 1317.68208 Theor. Comput. Sci. 564, 63-88 (2015). MSC: 68T15 68Q60 68Q65 68U05 PDF BibTeX XML Cite \textit{J.-F. Dufourd}, Theor. Comput. Sci. 564, 63--88 (2015; Zbl 1317.68208) Full Text: DOI
Courtieu, Pierre; Rieg, Lionel; Tixeuil, Sébastien; Urbain, Xavier Impossibility of gathering, a certification. (English) Zbl 1317.68264 Inf. Process. Lett. 115, No. 3, 447-452 (2015). MSC: 68W15 68T15 68T40 68U05 68W40 PDF BibTeX XML Cite \textit{P. Courtieu} et al., Inf. Process. Lett. 115, No. 3, 447--452 (2015; Zbl 1317.68264) Full Text: DOI
Poza, María; Domínguez, César; Heras, Jónathan; Rubio, Julio A certified reduction strategy for homological image processing. (English) Zbl 1354.68286 ACM Trans. Comput. Log. 15, No. 3, Article No. 23, 23 p. (2014). MSC: 68U10 03B35 55U15 68T15 92C55 PDF BibTeX XML Cite \textit{M. Poza} et al., ACM Trans. Comput. Log. 15, No. 3, Article No. 23, 23 p. (2014; Zbl 1354.68286) Full Text: DOI arXiv
Omodeo, Eugenio G.; Tomescu, Alexandru I. Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets. (English) Zbl 1315.68223 J. Autom. Reasoning 52, No. 1, 1-29 (2014). MSC: 68T15 03B35 05C75 PDF BibTeX XML Cite \textit{E. G. Omodeo} and \textit{A. I. Tomescu}, J. Autom. Reasoning 52, No. 1, 1--29 (2014; Zbl 1315.68223) Full Text: DOI
Ziegler, Günter M. Book review of: Alexander Soifer, The mathematical coloring book. Mathematics of coloring and the colorful life of its creators. (English) Zbl 1306.00028 Jahresber. Dtsch. Math.-Ver. 116, No. 4, 261-269 (2014). MSC: 00A17 05-01 05C15 05C55 05-03 01A60 PDF BibTeX XML Cite \textit{G. M. Ziegler}, Jahresber. Dtsch. Math.-Ver. 116, No. 4, 261--269 (2014; Zbl 1306.00028) Full Text: DOI
Pauly, Marc Can strategizing in round-robin subtournaments be avoided? (English) Zbl 1302.91087 Soc. Choice Welfare 43, No. 1, 29-46 (2014). MSC: 91B14 05C20 PDF BibTeX XML Cite \textit{M. Pauly}, Soc. Choice Welfare 43, No. 1, 29--46 (2014; Zbl 1302.91087) Full Text: DOI
Heras, Jónathan; Komendantskaya, Ekaterina Recycling proof patterns in Coq: case studies. (English) Zbl 1302.68243 Math. Comput. Sci. 8, No. 1, 99-116 (2014). MSC: 68T15 68T05 PDF BibTeX XML Cite \textit{J. Heras} and \textit{E. Komendantskaya}, Math. Comput. Sci. 8, No. 1, 99--116 (2014; Zbl 1302.68243) Full Text: DOI
Fuchs, Laurent; Théry, Laurent Implementing geometric algebra products with binary trees. (English) Zbl 1311.68147 Adv. Appl. Clifford Algebr. 24, No. 2, 589-611 (2014). MSC: 68T15 11E88 15A66 PDF BibTeX XML Cite \textit{L. Fuchs} and \textit{L. Théry}, Adv. Appl. Clifford Algebr. 24, No. 2, 589--611 (2014; Zbl 1311.68147) Full Text: DOI
Dehlinger, Christophe; Dufourd, Jean-François Formal specification and proofs for the topology and classification of combinatorial surfaces. (English) Zbl 1296.65034 Comput. Geom. 47, No. 9, 869-890 (2014). MSC: 65D18 PDF BibTeX XML Cite \textit{C. Dehlinger} and \textit{J.-F. Dufourd}, Comput. Geom. 47, No. 9, 869--890 (2014; Zbl 1296.65034) Full Text: DOI
Pąk, Karol Automated improving of proof legibility in the Mizar system. (English) Zbl 1304.68160 Watt, Stephen M. (ed.) et al., Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7–11, 2014. Proceedings. Berlin: Springer (ISBN 978-3-319-08433-6/pbk). Lecture Notes in Computer Science 8543. Lecture Notes in Artificial Intelligence, 373-387 (2014). MSC: 68T15 68T30 PDF BibTeX XML Cite \textit{K. Pąk}, Lect. Notes Comput. Sci. 8543, 373--387 (2014; Zbl 1304.68160) Full Text: DOI
Gransden, Thomas; Walkinshaw, Neil; Raman, Rajeev Mining state-based models from proof corpora. (English) Zbl 1304.68155 Watt, Stephen M. (ed.) et al., Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7–11, 2014. Proceedings. Berlin: Springer (ISBN 978-3-319-08433-6/pbk). Lecture Notes in Computer Science 8543. Lecture Notes in Artificial Intelligence, 282-297 (2014). MSC: 68T15 PDF BibTeX XML Cite \textit{T. Gransden} et al., Lect. Notes Comput. Sci. 8543, 282--297 (2014; Zbl 1304.68155) Full Text: DOI
Alama, Jesse; Kahle, Reinhard Checking proofs. (English) Zbl 1330.00021 Aberdein, Andrew (ed.) et al., The argument of mathematics. Dordrecht: Springer (ISBN 978-94-007-6533-7/hbk; 978-94-007-6534-4/ebook). Logic, Epistemology, and the Unity of Science 30, 147-170 (2013). Reviewer: Manfred Kerber (Birmingham) MSC: 00A30 00A35 03-03 01A60 01A61 03B35 68T15 PDF BibTeX XML Cite \textit{J. Alama} and \textit{R. Kahle}, Log. Epistemol. Unity Sci. 30, 147--170 (2013; Zbl 1330.00021) Full Text: DOI
McEvoy, Mark Experimental mathematics, computers and the a priori. (English) Zbl 1284.00051 Synthese 190, No. 3, 397-412 (2013). MSC: 00A35 00A30 62B15 68T15 PDF BibTeX XML Cite \textit{M. McEvoy}, Synthese 190, No. 3, 397--412 (2013; Zbl 1284.00051) Full Text: DOI
Wirth, Claus-Peter Herbrand’s fundamental theorem in the eyes of Jean van Heijenoort. (English) Zbl 1267.03054 Log. Univers. 6, No. 3-4, 485-520 (2012). Reviewer: Reinhard Kahle (Lisboa) MSC: 03F07 01A60 03-03 PDF BibTeX XML Cite \textit{C.-P. Wirth}, Log. Univers. 6, No. 3--4, 485--520 (2012; Zbl 1267.03054) Full Text: DOI
Melquiond, Guillaume Floating-point arithmetic in the Coq system. (English) Zbl 1257.68131 Inf. Comput. 216, 14-23 (2012). Reviewer: Manfred Kerber (Birmingham) MSC: 68T15 PDF BibTeX XML Cite \textit{G. Melquiond}, Inf. Comput. 216, 14--23 (2012; Zbl 1257.68131) Full Text: DOI
Brun, Christophe; Dufourd, Jean-François; Magaud, Nicolas Designing and proving correct a convex hull algorithm with hypermaps in Coq. (English) Zbl 1247.65021 Comput. Geom. 45, No. 8, 436-457 (2012). MSC: 65D18 65Y15 PDF BibTeX XML Cite \textit{C. Brun} et al., Comput. Geom. 45, No. 8, 436--457 (2012; Zbl 1247.65021) Full Text: DOI
McConnell, R. M.; Mehlhorn, K.; Näher, S.; Schweitzer, P. Certifying algorithms. (English) Zbl 1298.68289 Comput. Sci. Rev. 5, No. 2, 119-161 (2011). MSC: 68W01 68-02 PDF BibTeX XML Cite \textit{R. M. McConnell} et al., Comput. Sci. Rev. 5, No. 2, 119--161 (2011; Zbl 1298.68289) Full Text: DOI
Ciolli, Gianni; Gentili, Graziano; Maggesi, Marco A certified proof of the Cartan fixed point theorems. (English) Zbl 1250.68233 J. Autom. Reasoning 47, No. 3, 319-336 (2011). Reviewer: Manfred Kerber (Birmingham) MSC: 68T15 32A99 30C80 PDF BibTeX XML Cite \textit{G. Ciolli} et al., J. Autom. Reasoning 47, No. 3, 319--336 (2011; Zbl 1250.68233) Full Text: DOI
Bundy, Alan Automated theorem provers: a practical tool for the working mathematician? (English) Zbl 1237.68177 Ann. Math. Artif. Intell. 61, No. 1, 3-14 (2011). Reviewer: G. E. Mints (Stanford) MSC: 68T15 PDF BibTeX XML Cite \textit{A. Bundy}, Ann. Math. Artif. Intell. 61, No. 1, 3--14 (2011; Zbl 1237.68177) Full Text: DOI
Solovyev, Alexey; Hales, Thomas C. Efficient formal verification of bounds of linear programs. (English) Zbl 1335.68238 Davenport, James H. (ed.) et al., Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18–23, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22672-4/pbk). Lecture Notes in Computer Science 6824. Lecture Notes in Artificial Intelligence, 123-132 (2011). MSC: 68T15 65K05 90C05 PDF BibTeX XML Cite \textit{A. Solovyev} and \textit{T. C. Hales}, Lect. Notes Comput. Sci. 6824, 123--132 (2011; Zbl 1335.68238) Full Text: DOI
Heras, Jónathan; Poza, María; Dénès, Maxime; Rideau, Laurence Incidence simplicial matrices formalized in Coq/SSReflect. (English) Zbl 1335.68229 Davenport, James H. (ed.) et al., Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18–23, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22672-4/pbk). Lecture Notes in Computer Science 6824. Lecture Notes in Artificial Intelligence, 30-44 (2011). MSC: 68T15 55-04 55U10 PDF BibTeX XML Cite \textit{J. Heras} et al., Lect. Notes Comput. Sci. 6824, 30--44 (2011; Zbl 1335.68229) Full Text: DOI
Domínguez, César; Rubio, Julio Effective homology of bicomplexes, formalized in Coq. (English) Zbl 1207.68211 Theor. Comput. Sci. 412, No. 11, 962-970 (2011). MSC: 68Q65 55U15 68T15 68W30 PDF BibTeX XML Cite \textit{C. Domínguez} and \textit{J. Rubio}, Theor. Comput. Sci. 412, No. 11, 962--970 (2011; Zbl 1207.68211) Full Text: DOI
Barthe, Gilles; Grégoire, Benjamin; Lakhnech, Yassine; Zanella Béguelin, Santiago Beyond provable security verifiable IND-CCA security of OAEP. (English) Zbl 1284.94052 Kiayias, Aggelos (ed.), Topics in cryptology – CT-RSA 2011. The cryptographers’ track at the RSA conference 2011, San Francisco, CA, USA, February 14–18, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-19073-5/pbk). Lecture Notes in Computer Science 6558, 180-196 (2011). MSC: 94A60 PDF BibTeX XML Cite \textit{G. Barthe} et al., Lect. Notes Comput. Sci. 6558, 180--196 (2011; Zbl 1284.94052) Full Text: DOI
Steinberger, John P. An unavoidable set of \(D\)-reducible configurations. (English) Zbl 1221.05165 Trans. Am. Math. Soc. 362, No. 12, 6633-6661 (2010). MSC: 05C15 PDF BibTeX XML Cite \textit{J. P. Steinberger}, Trans. Am. Math. Soc. 362, No. 12, 6633--6661 (2010; Zbl 1221.05165) Full Text: DOI arXiv
Wood, David R. Contractibility and the Hadwiger conjecture. (English) Zbl 1215.05177 Eur. J. Comb. 31, No. 8, 2102-2109 (2010). MSC: 05C83 PDF BibTeX XML Cite \textit{D. R. Wood}, Eur. J. Comb. 31, No. 8, 2102--2109 (2010; Zbl 1215.05177) Full Text: DOI arXiv
Nipkow, Tobias Linear quantifier elimination. (English) Zbl 1207.68339 J. Autom. Reasoning 45, No. 2, 189-212 (2010). MSC: 68T15 03C10 PDF BibTeX XML Cite \textit{T. Nipkow}, J. Autom. Reasoning 45, No. 2, 189--212 (2010; Zbl 1207.68339) Full Text: DOI
Hales, Thomas C.; Harrison, John; McLaughlin, Sean; Nipkow, Tobias; Obua, Steven; Zumkeller, Roland A revision of the proof of the Kepler conjecture. (English) Zbl 1195.52004 Discrete Comput. Geom. 44, No. 1, 1-34 (2010). Reviewer: Rolf Schneider (Freiburg i. Br.) MSC: 52C17 PDF BibTeX XML Cite \textit{T. C. Hales} et al., Discrete Comput. Geom. 44, No. 1, 1--34 (2010; Zbl 1195.52004) Full Text: DOI arXiv
Obua, Steven; Nipkow, Tobias Flyspeck II: The basic linear programs. (English) Zbl 1184.68465 Ann. Math. Artif. Intell. 56, No. 3-4, 245-272 (2009). MSC: 68T15 03B35 90C05 PDF BibTeX XML Cite \textit{S. Obua} and \textit{T. Nipkow}, Ann. Math. Artif. Intell. 56, No. 3--4, 245--272 (2009; Zbl 1184.68465) Full Text: DOI
Dufourd, Jean-François An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps. (English) Zbl 1187.68525 J. Autom. Reasoning 43, No. 1, 19-51 (2009). MSC: 68T15 03B35 PDF BibTeX XML Cite \textit{J.-F. Dufourd}, J. Autom. Reasoning 43, No. 1, 19--51 (2009; Zbl 1187.68525) Full Text: DOI
Biha, Sidi Ould Finite groups representation theory with Coq. (English) Zbl 1247.68231 Carette, Jacques (ed.) et al., Intelligent computer mathematics. 16th symposium, Calculemus 2009, 8th international conference, MKM 2009, held as part of CICM 2009, Grand Bend, Canada, July 6–12, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-02613-3/pbk). Lecture Notes in Computer Science 5625. Lecture Notes in Artificial Intelligence, 438-452 (2009). MSC: 68T15 20C40 PDF BibTeX XML Cite \textit{S. O. Biha}, Lect. Notes Comput. Sci. 5625, 438--452 (2009; Zbl 1247.68231) Full Text: DOI
Calude, Cristian S.; Müller, Christine Formal proof: reconciling correctness and understanding. (English) Zbl 1247.03017 Carette, Jacques (ed.) et al., Intelligent computer mathematics. 16th symposium, Calculemus 2009, 8th international conference, MKM 2009, held as part of CICM 2009, Grand Bend, Canada, July 6–12, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-02613-3/pbk). Lecture Notes in Computer Science 5625. Lecture Notes in Artificial Intelligence, 217-232 (2009). MSC: 03B35 68T15 PDF BibTeX XML Cite \textit{C. S. Calude} and \textit{C. Müller}, Lect. Notes Comput. Sci. 5625, 217--232 (2009; Zbl 1247.03017) Full Text: DOI
Mulhern, Anne; Fischer, Charles; Liblit, Ben Tool support for proof engineering. (English) Zbl 1278.68275 Autexier, Serge (ed.) et al., Proceedings of the 7th workshop on user interfaces for theorem provers (UITP 2006), Seattle, WA, USA, August 21, 2006. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 174, No. 2, 75-86 (2007). MSC: 68T15 PDF BibTeX XML Cite \textit{A. Mulhern} et al., Electron. Notes Theor. Comput. Sci. 174, No. 2, 75--86 (2007; Zbl 1278.68275) Full Text: DOI