Publications

Under review

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

Complete

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

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

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

Education

Dissertation

Publications

Under review

Complete

Employment

Professional Service

Refereeing and Reviewing

Thesis Committees

Program Committees

Professional Memberships

Awards and Scholarships