Doctor of Philosophy |
Bachelor of Arts |
Formal Proofs and Refutations
Grigori Mints, Solomon Feferman, Johan van Benthem, Jeremy Avigad
Axiomatizing Jaskowski's discussive logic D2 (with Hitoshi Omori), Studia Logica
From absolute to affine geometry in terms of point-reflections, midpoints, and collinearity (with Victor Pambuccian), Note di Matematica
Sentence complexity of theorems in Mizar, Journal of Automated Reasoning
Dialogues for proof search, in Christoph Benzmüller and Jens Otten (eds.), ARQNL 2014. Automated Reasoning in Quantified Non-Classical Logics, EasyChair, 2015, pp. 65–70
Automating Leibniz's theory of concepts (with Paul Oppenheimer and Edward N. Zalta) , in Amy P. Felty and Aart Middeldorp (eds.), Automated Deduction - CADE 25, Springer, 2015, pp. 73–97
Without E, in Pavel Arazim and Michal Dancak (eds.), Logica Yearbook 2014, College Publications, 2015, pp. 1–12
The simplest axiom system for plane hyperbolic geometry revisited, again, Studia Logica 102, 2014, pp. 609–615 [MR3202001]
A curious dialogical logic and its composition problem (with Aleks Knoks and Sara L. Uckelman), Journal of Philosophical Logic 43, 2014, pp. 1065–1100
Premise selection for mathematics by corpus analysis and kernel methods (with Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze and Josef Urban), Journal of Automated Reasoning 52, 2014, pp. 191–213
Tarski geometry axioms (with William Richter and Adam Grabowski), Formalized Mathematics 22, 2014, pp. 167–176
Computing with mathematical arguments (with Reinhard Kahle) , in Hanne Andersen et al. (eds.), New Challenges to Philosophy of Science, Springer, 2013, pp. 9–22
Checking proofs (with Reinhard Kahle) , in Andrew Aberdein and Ian Dove (eds.), The Argument of Mathematics, Springer, 2013, pp. 147–170
Eliciting implicit assumptions of Mizar proofs by property omission, Journal of Automated Reasoning 50, 2013, pp. 123–133
Complete independence of an axiom system for central translations, Note di Matematica 33, 2013, pp. 133–142 [MR3178579]
Automated and human proofs in general mathematics: An initial comparison (with Daniel Kühlwein and Josef Urban), in Nikolai Bjørner and Andrei Voronkov (eds.), Logic for Programming, Artificial Intelligence, and Reasoning, Springer, 2012, pp. 37–45
Escape to Mizar from ATPs, in Pascal Fontaine et al. (eds.), PAAR 2012, Easychair, 2012, pp. 3–11
New developments in parsing Mizar (with Czesław Bylinski), in Johan Juering et al. (eds.), Intelligent Computer Mathematics, Springer, 2012, pp. 427–431
Dependencies in formal mathematics: Applications and extraction for Coq and Mizar (with Lionel Mamane and Josef Urban), in Johan Juering et al. (eds.), Intelligent Computer Mathematics, Springer, 2012, pp. 1–16
What is dialogical about dialogical logic? (with Sara L. Uckelman) , in Henrique Jales Ribeiro (ed.), Inside Arguments, Cambridge Scholars Publishing, 2012, pp. 207–222
The λ-calculus in Edward N. Zalta (ed.), The Stanford Encyclopedia of Philosophy, Center for the Study of Language and Information, Stanford University, 2011
Metadata for a wiki of formalized mathematics, in Christoph Lange and Josef Urban (eds.), MathWikis-2011, CEUR-WS, 2011, pp. 2–5
Large formal wikis: Issues and solutions (with Kasper Brink, Lionel Mamane and Josef Urban), in James H. Davenport et al. (eds.), Intelligent Computer Mathematics, Springer, 2011, pp. 133–148
mizar-items: Exploring fine-grained dependencies in the Mizar Mathematical Library, in James H. Davenport et al. (eds.), Intelligent Computer Mathematics, Springer, 2011, pp. 266–267
Licensing the Mizar Mathematical Library (with Michael Kohlhase, Lionel Mamane, Adam Naumowicz, Piotr Rudnicki and Josef Urban), in James H. Davenport et al. (eds.), Intelligent Computer Mathematics, Springer, 2011, pp. 149–163
Dialogue games for classical logic (with Sara L. Uckelman and Aleks Knoks), in Martin Giese and Roman Kuznets (eds.), TABLEAUX 2011: Workshops, Tutorials, and Short Papers, Institut für Informatik und angewandte Mathematik, University of Bern, 2011, pp. 82–86
A wiki for Mizar: Motivation, Considerations, and Initial Prototype (with Josef Urban, Piotr Rudnicki and Herman Guevers), in Serge Autexier et al. (eds.), Intelligent Computer Mathematics, Springer, 2010, pp. 455–469
Exploring Steinitz-Rademacher polyhedra: A challenge for automated reasoning tools, in Geoff Sutcliffe et al. (eds.), Proceedings of the Eighth International Workshop on the Implementation of Logics, 2010, pp. 14–18
Euler's polyhedron formula in Mizar, in Komei Fukada et al. (eds.), Mathematical Software – ICMS 2010, 2010, pp. 144–147
A formal proof of Euler's polyhedron formula, Studies in Logic, Grammar, and Rhetoric 18, 2010, pp. 455–469
Euler's polyhedron formula, Formalized Mathematics 16, 2008, pp. 7–17
The vector space of subsets of a set based on symmetric difference, Formalized Mathematics 16, 2008, pp. 1–5
The rank+nullity theorem, Formalized Mathematics 15, 2007, pp. 137–142
Postdoctoral Researcher
Theory and Logic Group, Vienna University of Technology, Austria
January, 2014 to June, 2015
Postdoctoral Researcher
Center for Artificial Intelligence, New University of Lisbon, Portugal
September, 2009 to September, 2012
Assistant Editor
Stanford Encyclopedia of Philosophy, United States
November, 2007 to present
Research Programmer
Qualitative Reasoning Group, Northwestern University, United States
September, 2001 to August, 2002
Programmer
Cycorp, Inc., United States
June, 2001 to September, 2001
Minds and Machines | Journal of Logic and Computation |
Formalized Mathematics | Logic Journal of the IGPL |
History and Philosophy of Computing | Journal of Philosophical Logic |
Review of Symbolic Logic | The Internet Encyclopedia of Philosophy |
Mathematical Reviews | Handbook of Mathematical Fuzzy Logic |
Fenner Tanswell, Proof and Prejudice: Why Formalisation Doesn't Make You a Formalist
Master of Logic thesis at Institute for Logic, Language and Computation, University of Amsterdam, 2012
Matthew Wampler-Doty, Evidentialist Logic
Master of Logic thesis at Institute for Logic, Language and Computation, University of Amsterdam, 2010
Proof eXchange for Theorem Proving (PxTP 2015) | Conference on Intelligent Computer Mathematics (2014) |
The Notion of Proof Revisited (AMS-EMS-SPM Joint Meeting 2015) | Logic and Games (Vienna Summer of Logic 2014) |
Conference on Intelligent Computer Mathematics (2013) | MathWikis (2011) |
Austrian Mathematical Society | German TeX Users Group |
Association of Mizar Users | Mathematical Association of America |
Association for Automated Reasoning |
Visiting Fellow
Isaac Newton Institute for Mathematical Sciences — Semantics and Syntax: A Legacy of Alan Turing
Cambridge, England
January, 2012 to April, 2012
Cross-CRP Short-Term Visit (Lisbon-Vienna)
European Science Foundation
2011
Centennial Teaching Assistant Award
Stanford University Center for Teaching and Learning
2008
Fulbright Scholar
Rényi Institute of Mathematics, Budapest, Hungary
September, 2002 to September, 2003
Budapest Semesters in Mathematics
St. Olaf College
2001
Scholar of the College
University of Minnesota at Morris
2000