- Radboud Repository
- →
- Browsing by Author
JavaScript is disabled for your browser. Some features of this site may not work without it.
Browsing by Author "Kaliszyk, C.S."
Now showing items 1-34 of 34
-
A FORMAL PROOF OF THE KEPLER CONJECTURE Hales, T.; Adams, M.; Bauer, G.; Dang, T.D.; Harrison, J.; Hoang, L.T.; Kaliszyk, C. ; Magron, V.; McLaughlin, S.; Nguyen, Tat T.; Nguyen, Q.T.; Nipkow, T.; Obua, S.; Pleso, J.; Rute, J.; Solovyev, A.; Ta, T.H.A.; Tran, N.T.; Trieu, T.D.; Urban, Jos.; Vu, K.Y.; Zumkeller, R. et al.2017, Article / Letter to editor (Forum of Mathematics. Pi, vol. 5, (2017), pp. 1-29, article e2)
sine al.
-
Hammering towards QED Blanchette, J.C.; Kaliszyk, C. ; Paulson, L.C.; Urban, J.2016, Article / Letter to editor (Journal of Formalized Reasoning, vol. 9, iss. 1, (2016), pp. 1-48)
-
A Learning-Based Fact Selector for Isabelle/HOL Blanchette, J.C.; Greenaway, D.; Kaliszyk, C. ; Kühlwein, D.; Urban, J.2016, Article / Letter to editor (Journal of Automated Reasoning, vol. 57, iss. 3, (2016), pp. 219-244)
-
FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover Kaliszyk, C. ; Urban, J.2015, Part of book or chapter of book (Davis, M.; Fehnker, A.; McIver, A. (ed.), Logic for Programming, Artificial Intelligence, and Reasoning : 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings, pp. 88-96) -
Efficient Semantic Features for Automated Reasoning over Large Theories Kaliszyk, C. ; Urban, J.; Vyskocil, J.2015, Article in monograph or in proceedings (Yang, Q. (ed.), IJCAI 2015 : Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, pp. 3084-3090)
-
Formalizing Physics: Automation, Presentation and Foundation Issues Kaliszyk, C. ; Urban, J.; Siddique, U.; Khan-Afshar, S.; Dunchev, C.; Tahar, S.2015, Part of book or chapter of book (Kerber, M.; Carette, J.; Kaliszyk, C. (ed.), Intelligent Computer Mathematics : International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings, pp. 288-295) -
Learning-assisted theorem proving with millions of lemmas Kaliszyk, C. ; Urban, J.2015, Article / Letter to editor (Journal of Symbolic Computation, vol. 69, iss. July-August, (2015), pp. 109-128)
-
HOL(y)Hammer: Online ATP Service for HOL Light Kaliszyk, C. ; Urban, J.2015, Article / Letter to editor (Mathematics in Computer Science, vol. 9, iss. 1, (2015), pp. 5-22)
-
Lemmatization for Stronger Reasoning in Large Theories Kaliszyk, C. ; Urban, J.; Vyskočil, J.2015, Part of book or chapter of book (Lutz, C.; Ranise, S. (ed.), Frontiers of Combining Systems : 10th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21-24, 2015, Proceedings, pp. 341-356)
-
MizAR 40 for Mizar 40 Kaliszyk, C. ; Urban, J.2015, Article / Letter to editor (Journal of Automated Reasoning, vol. 55, iss. 3, (2015), pp. 245-256)
-
Learning to Parse on Aligned Corpora (Rough Diamond) Kaliszyk, C. ; Urban, J.; Vyskočil, J.2015, Part of book or chapter of book (Urban, C.; Zhang, X. (ed.), Interactive Theorem Proving : 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings, pp. 227-233)
-
System Description: E.T. 0.1 Kaliszyk, C. ; Schulz, S.; Urban, J.; Vyskočil, J.2015, Part of book or chapter of book (Felty, A.P.; Middeldorp, A. (ed.), Automated Deduction - CADE-25 : 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, pp. 389-398)
-
Certified Connection Tableaux Proofs for HOL Light and TPTP Kaliszyk, C. ; Urban, J.; Vyskocil, J.2015, Article in monograph or in proceedings (Leroy, X. (ed.), CPP'15 : Proceedings of the 2015 Conference on Certified Programs and Proofs, pp. 59-66)
-
Learning-Assisted Automated Reasoning with Flyspeck Kaliszyk, C. ; Urban, J.2014, Article / Letter to editor (Journal of Automated Reasoning, vol. 53, iss. 2, (2014), pp. 173-213)
-
Erratum to : Learning-Assisted Automated Reasoning with Flyspeck Kaliszyk, C. ; Urban, J.2014, Article / Letter to editor (Journal of Automated Reasoning, vol. 2014, iss. October, (2014), pp. 1)
-
Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems Joosten, S.; Kaliszyk, C. ; Urban, J.2014, Part of book or chapter of book (Verbeek, F. (ed.), ACL2 2014 : Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014, pp. 77-85)
-
Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description Kaliszyk, C. ; Urban, J.; Vyskočil, J.; Geuvers, H.2014, Part of book or chapter of book (Watt, S.; Davenport, J.; Sexton, A. (ed.), Intelligent Computer Mathematics, pp. 435-439)
-
MaSh: Machine Learning for Sledgehammer Kühlwein, D.; Blanchette, J.; Kaliszyk, C. ; Urban, J.2013, Part of book or chapter of book (Blazy, S.; Paulin-Mohring, C.; Pichardie, D. (ed.), Interactive Theorem Proving, pp. 35-50)
-
PRocH: Proof Reconstruction for HOL Light Kaliszyk, C. ; Urban, J.2013, Part of book or chapter of book (Bonacina, M. (ed.), Automated Deduction – CADE-24, pp. 267-274)
-
Automated Reasoning Service for HOL Light Kaliszyk, C. ; Urban, J.2013, Part of book or chapter of book (Carette, J.; Aspinall, D.; Lange, C. (ed.), Intelligent Computer Mathematics, pp. 120-135)
-
Stronger automation for flyspeck by feature weighting and strategy evolution Kaliszyk, C. ; Urban, J.2013, Part of book or chapter of book (Blanchette, J. (ed.), Pxtp 2013. Third international workshop on proof exchange for theorem proving, pp. 87-95)
-
Lemma mining over HOL light Kaliszyk, C. ; Urban, J.2013, Part of book or chapter of book (McMillan, K.; Middeldorp, A.; Voronkov, A. (ed.), Logic for programming, artificial intelligence, and reasoning, pp. 503-517)
-
Formal Mathematics on Display: A Wiki for Flyspeck Tankink, C. ; Kaliszyk, C. ; Urban, J.; Geuvers, H.2013, Part of book or chapter of book (Carette, J. (ed.), Intelligent Computer Mathematics, pp. 152-167)
-
Communicating formal proof : the case of Flyspeck Tankink, C. ; Kaliszyk, C. ; Urban, J.; Geuvers, H.2013, Article in monograph or in proceedings (Blazy, S. (ed.), Interactive Theorem Proving : 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, pp. 451-456)
-
Initial Experiments with External Provers and Premise Selection on HOL Light} Corpora Kaliszyk, C. ; Urban, J.2012, Article in monograph or in proceedings (Fontaine, P. (ed.), PAAR-2012 : Third Workshop on Practical Aspects of Automated Reasoning June 30 & July 1, 2012 A liated with the 6th International Joint Conference on Automated Reasoning (IJCAR 201), Manchester, pp. 72-81)
-
Computing with Classical Real Numbers 2009, Article / Letter to editor (Journal of Formalized Reasoning, vol. 2, iss. 1, (2009), pp. 27-39)
-
Deduction using the ProofWeb system Kaliszyk, C.S. ; Raamsdonk, F. van; Wiedijk, F. ; Wupper, H. ; Hendriks, Maxim; Vrijer, Roel de2008, External research report
-
A Real Semantic Web for Mathematics Deserves a Real Semantics 2008, Article in monograph or in proceedings (Lange, Christoph; Schaffert, Sebastian; Skaf-Molli, Hala (ed.), SemWiki 2008 – The Wiki Way of Semantics : Proceedings of the 3rd Semantic Wiki Workshop (SemWiki 2008) at the 5th European Semantic Web Conference (ESWC 2008), pp. 62-66)
-
Cooperative Repositories for Formal Proofs -- A Wiki-Based Solution 2007, Article in monograph or in proceedings (Kauers, Manuel; Kerber, Manfred; Miner, Robert (ed.), Towards Mechanized Mathematical Assistants, pp. 221-234)
-
Web Interfaces for Proof Assistants 2007, Article / Letter to editor (Electronic Notes in Theoretical Computer Science, vol. 174, iss. 2, (2007), pp. 49-61)
-
Certified Computer Algebra on top of an Interactive Theorem Prover 2007, Article in monograph or in proceedings (M. Kauers, R. Miner; Windsteiger, W. (ed.), Towards Mechanized Mathematical Assistants, Calculemus 2007, Hagenberg, pp. 94-105)
-
Teaching logic using a state-of-the-art proof assistant Kaliszyk, C.S. ; Wiedijk, F. ; Hendriks, M. ; Raamsdonk, F. van2007, Article in monograph or in proceedings (Geuvers, H.; Courtieu, P. (ed.), PATE'07, International Workshop on Proof Assistants and Types in Education, pp. 37-50)
-
Web Interfaces for Proof Assistants 2006, Article in monograph or in proceedings (Autexier, S.; Benzm"uller, C. (ed.), Proceedings of the FLoCs Workshop on User Interfaces for Theorem Provers (UITP-06), Seattle, pp. 53-64)
Now showing items 1-34 of 34
Search Repository
Browse
-
All of Repository
Upload Full Text