Jesse Alama

I am a post-doctoral researcher in the Dialogical Foundations of Semantics project based at the Center for Artificial Intelligence at the New University of Lisbon in Portugal. I completed my Ph.D. in 2009 under the supervision of Grigori Mints in the Stanford University Department of Philosophy (see my academic heritage). My dissertation, Formal Proofs and Refutations, extends and re-interprets the critical philosophy of mathematics of Imre Lakatos in the light of the results of automated reasoning.

I work in mathematical logic (primarily proof theory) and philosophy of mathematics, with a specialization in formal mathematics, a young interdisciplinary subject devoted to constructing formalizations of mathematical knowledge. Formal mathematics offers a lot of challenging problems for artificial intelligence and, I believe, to our understanding of human mathematical argumentation. I'm eager to apply techniques from interactive and automated theorem proving to problems in the foundations and philospohy of mathematics.

Upcoming Activities

• Until April 15, 2012, I will be a visiting fellow at the Isaac Newton Institute for Mathematical Sciences under the auspices of the Semantics and Syntax: A Legacy of Alan Turing program.

Work in Progress

• “Conditions for the redundancy of the E-rule” (with Sara Uckelman).
• “A note on foundation in Tarski-Grothendieck set theory”.
• “Diamonds in the Lindenbaum-Tarski algebra of PA” (with Reinhard Kahle and Henk Barendregt).
• “Dependencies in formal mathematics” (with Lionel Mamane and Josef Urban). [arXiv preprint]
• “Premise selection for mathematics by corpus analysis and kernel methods” (with Daniel Kühlwein, Evgeni Tsivtsivadze, Josef Urban, and Tom Heskes). [arXiv preprint]

Professional Activity

Invited Contributions

• “Toward a structure theory for Lorenzen dialogue games”, invited extension of a presentation given at Computability in Europe 2010, 30 June–4 July, 2010, Ponta Delgada, Portugal. [preprint]
• “The λ-calculus”, commissioned entry for the Stanford Encyclopedia of Philosophy.
• “Euler's polyhedron formula in MIZAR”, Third International Conference on Mathematical Software (ICMS 2010), Kobe, Japan, September 15, 2010. [slides]

Publications

2011

• “Metadata for a wiki of formalized mathematics” [official version]

  Lange, Christoph and Urban, Josef (eds.), MathWikis-2011—Proceedings of the ITP 2011 Workshop on Mathematical Wikis, Nijmegen, the Netherlands, August 27, 2011, pp. 2–5.

• “Large formal wikis: Issues and solutions” (with Kasper Brink, Lionel Mamane, and Josef Urban). [official version, arXiv version]

  Davenport, James H. and Farmer, William M. and Urban, Josef and Rabe, Florian (eds.), Intelligent Computer Mathematics, 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18–23. Proceedings, Lecture Notes in Computer Science 6824, pp. 133–148.

• “Licensing the MIZAR Mathematical Library” (with Michael Kohlhase, Lionel Mamane, Adam Naumowicz, Piotr Rudnicki, and Josef Urban). [official version, arXiv version]

  Davenport, James H. and Farmer, William M. and Urban, Josef and Rabe, Florian (eds.), Intelligent Computer Mathematics, 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18–23. Proceedings, Lecture Notes in Computer Science 6824, pp. 149–163.

• “mizar-items: Exploring fine-grained dependencies in the MIZAR Mathematical Library” [official version, arXiv version]

  Davenport, James H. and Farmer, William M. and Urban, Josef and Rabe, Florian (eds.), Intelligent Computer Mathematics, 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18–23. Proceedings, Lecture Notes in Computer Science 6824, pp. 266–7.

2010

• “Exploring Steinitz-Rademacher polyhedra: A challenge for automated reasoning tools” [preprint]

  Sutcliffe, G., Ternovska, E. and Schulz, S. (eds.), Proceedings of the 8th International Workshop on the Implementation of Logics (IWIL 2010).

• “Euler's polyhedron formula in MIZAR” [electronic version]

  Fukada, K. et al. (eds.), Mathematical Software - ICMS 2010, Lecture Notes in Computer Science 6327, pp. 144–7.

• “A wiki for MIZAR: Motivation, Considerations, and Initial Prototype” (with Josef Urban, Piotr Rudnicki, and Herman Geuvers) [arXiv preprint]

  Autexier, S. et al., (eds.), Intelligent Computer Mathematics, Lecture Notes in Computer Science 6167, pp. 455–469.

2009

• “A formal proof of Euler's polyhedron formula” [electronic version]

  Studies in Logic, Grammar and Rhetoric 18(31), pp. 9–33.

2008

• “The vector space of subsets of a set based on disjoint union” [article in Formalized Mathematics, MIZAR text]

  Formalized Mathematics 16(1), pp. 1–5.

• “Euler's polyhedron formula” [article in Formalized Mathematics, MIZAR text]

  Formalized Mathematics 16(1), pp. 7–17.

2007

• “The rank+nullity theorem” [article in Formalized Mathematics, MIZAR text]

  Formalized Mathematics 15(3), 2007, pp. 137–142.

Contributed Presentations

2011

• “Checking proofs”, presented at the ESF Workshop Philosophy of Computer Science and Artificial Intelligence, 9 September, 2011, Ponta Delgada, Portugal [slides]
• “Metadata for a wiki of formalized mathematics”, presented at the ITP 2011 Workshop on Mathematical Wikis (MathWikis-2011), 27 August, 2011, Nijmegen, the Netherlands [slides]
• “Generalizing theorems of the MIZAR Mathematical Library by type promotion and property omission”, presented at the 3rd Workshop on Modules and Libraries for Proof Assistants (MLPA-11), 26 August, 2011, Nijmegen, the Netherlands and at the Brouwer Seminar, Foundations Group, Institute for Computing and Information Science, Radboud University Nijmegen, the Netherlands [conference slides, seminar slides]
• “Logical constants: classical, intuitionistic, dialogical?” (with Reinhard Kahle), presented (by Reinhard) at the ESSLLI 2011 Workshop on Logical Constants, 07 August, 2011, Ljubljana, Slovenia. [slides]
• “Fine-grained mathematical justifications”, presented at the Workshop on Logical Modelling: The Interface Between the Formal and the Empirical, affiliated symposium of the 14th Congress in Logic, Methodology and Philosophy of Science, 21 July 2011, Nancy, France [slides]
• “mizar-items: Exploring fine-grained dependencies in the MIZAR Mathematical Library”, presented at the Conferences in Intelligent Computer Mathematics (CICM 2011), 19 July 2011, Bertinoro, Italy. [poster, movie]
• “Dialogue games for classical logic” (with Aleks Knoks and Sara Uckelman), presented (by Aleks Knoks) at Tableaux 2011 [preprint]
• “Lorenzen dialogue games as logical semantics” (joint with Sara L. Uckelman), presented in the Researcher's Seminar of the Theory and Logic Group, Technical University of Vienna, Austria [slides]
• “Proof analysis using fine-grained dependency information in formal mathematics”, presented at the third Mathematical Logic in the Netherlands [slides]
• “Exploring fine-grained mathematical dependencies with MIZAR”, presented in the University of Białystok Mathematics Seminar. [slides]
• “Extending Fermüller-style dialogues to classical logic”, presented at ProDi [slides]
• “Fine-grained mathematical justifications”, presented at LogICCC meets India [slides]
• “A curious dialogical logic and its composition problem”, presented at the 4th Indian Conference on Logic and its Applications [slides]

2010

• “Fine-grained mathematical justifications”, presented at the Brouwer Seminar at Radboud University Nijmegen, the Netherlands. [slides]
• “Some further properties of the dialogical logic N” (joint work with Sara Uckelman), presented at the DIPLEAP workshop. [slides]
  (My presentation was a technical successor to Sara's, who presented immediately before I did and introduced N and the philosophy behind it. Consult her slides for an introduction to mine.)
• “Playing Lorenzen dialogue games on the web” (joint with Sara Uckelman), presented at Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17).
  [slides]
• “Exploring Steinitz-Rademacher polyhedra: a challenge for automated reasoning tools”, presented at the 8th International Workshop on Implementation of Logics (IWIL 2010). [LADR theory description]
  [slides]
• “Euler's polyhedron formula in MIZAR”, Third International Conference on Mathematical Software (ICMS 2010), Kobe, Japan, September 15, 2010.
• “Playing Lorenzen dialogue games on the web”, Mathematical User Interfaces (MathUI 2010), Paris, France, July 10, 2010.
• “A wiki for MIZAR: Motivation, Considerations, and Initial Prototype” Mathematical Knowledge Management (MKM 2010), Paris, France, July 8, 2010.
• “Expressibility of some basic properties of polyhedra in FOL and extensions”, Days in Logic 2010, Porto, Portugal, January 29, 2010.

2009

• “Expressibility of basic properties of combinatorial polyhedra in FOL and extensions”, Computer Science Logic 2009, Coimbra, Portugal, September 10, 2009.

Blogs

• jesse alama's research scribblings: Take a peek at what keeps me busy most days (and nights).
• TONIGHT: Proponent v. Opponent, a blog devoted to dialogue games and dialogical logic. (Coauthored with Sara Uckelman.)

Academic Programming Projects

The lists below are links to my code repositories (all of which are hosted these days on github) that concern my academic interests and activities. If you have any comments, questions, feature requests, or bug reports concerning my code, please do contact me (see my contact information below).

Formal Mathematics

My work on formal mathematics concentrates on the MIZAR system, an interactive proof assistant based on first-order classical logic and set theory. The MIZAR language for writing mathematics, with its emphasis on flexible notation and natural deduction, is, in my view, one of the most attractive formalisms out there today for writing truly formal proofs of mathematical statements. The library of mathematical knowledge that has been formalized in MIZAR—the MIZAR Mathematical Library (MML)—is very large; the MML witnesses the bona fide formalizability of serious mathematics.

To learn more about MIZAR, I can recommend: “Mizar in a nutshell”, by Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz, Journal of Formalized Reasoning 3(2), (2010), pp. 153–245. For a historical overview of this long-standing project to “reconstruct the mathematical vernacular”, see “MIZAR: The first 30 years”, by Roman Mutuszewski and Piotr Rudnicki, Mechanized Mathematics and its Applications 4(1), (2005), pp. 3–24.

Below you can find the code that I hack that's related to MIZAR.

• mizar-items: breaking MIZAR articles into bits.

  Part of this code base is devoted to a web application (based on hunchentoot) that facilitates exploring the MIZAR Mathematical Library, emphasizing the dependence of items upon other items (e.g., the theorems upon the axioms, a formula on the functions, predicates, and constants it contains, an argument by the background knowledge it takes for granted).

• mwiki: a wiki for MIZAR

  I am a contributor to the MathWiki project, based at Radboud University Nijmegen. The aim of the project is to create a wiki for formalized mathematics. The project's main output so far are wikis for MIZAR and for C-CoRN, the Constructive Coq Repository at Nijmegen. Thinking of formal mathematics as material for a wiki raises a number of interesting methodological and technical problems. For an overview of what has been accomplished so far, see “Large formal wikis: Issues and solutions” and “A wiki for MIZAR: Motivation, considerations, and initial prototype”.

• mizarmode: an Emacs mode for working with MIZAR texts

  Working with MIZAR texts in Emacs is the way to go. mizarmode is an extension of the Emacs text editor for submitting texts to the MIZAR verifier, analyzing proofs for spurious parts, inspecting and debugging proofs, generating ATP problems from MIZAR items (see, e.g., a video demo of some recent mizarmode innovations by Josef Urban; there's also a paper), and so forth.

• xsl4mizar: XSL stylesheets for operating on semantic representations of MIZAR texts

  Thanks to the XMLization of MIZAR, is it possible to do all sorts of transformations of MIZAR artifacts. Since the MIZAR language is so rich and flexible (and because the MIZAR tools are non-interactive ‘batch mode’ programs), working directly with .miz source files is essentially out of the question; one needs ‘semantic’ representations of the texts to be able to operate on them robustly.

Automated Reasoning

My work on formal mathematics goes hand-in-hand with my interest in automated deduction, which is devoted to the problem of getting machines to carry out certain reasoning tasks, such as discovering a formal proof of some statement or inventing a counterexample.

• tptp-el: work with TPTP files, theorem provers, and model finders in Emacs.

  tptp-el is an Emacs extension for processing TPTP files. Currently, the tool can pass off TPTP scripts to theorem provers (E, Vampire, Equinox, and Prover9 are currently supported) and model finders (Paradox and Mace4 are currently supported) and do some elementary interpretation of their output (e.g., highlight the assumptions from a TPTP script that were actually used in the solution of the ATP problem that the script represents).

  There's even some AppleScript code for doing TPTP work using the excellent SubEthaEdit.

• polyhedra: exploring polyhedra using automated reasoning tools

  While formalizing a proof of Euler's polyhedron formula during my dissertation research, I became interested in formal theories for reasoning about polyhedra. One angle that I took concerned expressibility is various properties of combinatorial polyhedra. It turns out that many desirable properties of polyhedra that one would like to express, such as connectedness [not being composed of multiple disjoint polyhedra] and satisfying Euler's polyhedron formula [the vertices, edges, and faces satisfy the relation V−E+F = 2] are not, prima facie, expressible. (Though one has to be careful with precisely what language is being used to express the desired properties; work by Bruno Courcelle and Valere Dussaux shows that one can express the genus of a map, in a suitable monadic second-order setting.)

  Another angle is to simply find some formal theories and work with them, their expressive limitations notwithstanding. From Branko Grünbaum's excellent “Are your polyhedra the same as my polyhedra?”, I came across a first-order approach, due to Ernst Steinitz, and started to work with this theory using ATP tools. I was humbled that many quite simple questions turned out to be rather difficult (though, admittedly, my representation of my questions as ATP problems was far from the slickest). See my paper proposing these problems for ATP systems.

Dialogical Logic

Dialogue games are a game-based approach to logic. These games feature a Proponent, who lays down a logical statement as valid, and a Opponent, who contests that formula's validity. The validity of the initially played formula is related to the winnability of the game for P. Initially, dialogue games were tailored to provide a new account of validity for intuitionistic logic, but since their invention in the late 50s, there are now dialogue-based characterizations of validity for other logics, too.

• dialogues: tools for working with Lorenzen dialogue games.

  A major component of this code base is a dynamic website for playing dialogue games (based on the UnCommon Web Common Lisp web framework).

Web Work

Internet technologies, especially those having to do with the World Wide Web, fascinate me. (Note: I'm an enthusiast of Internet technologies, not an expert web designer [to which this boring page obviously testifies] or Internet connoisseur; the technologies themselves fascinate me, even though my usage of them is often scanty.) I like learning about ReST, HTTP, JavaScript/ECMAScript, and the like. I dream of making killer web applications based on things that matter to me, like mathematics, formal proofs, logic, books, TeX, etc. Here are some projects having to do with the Internet:

• hunchentoot-utils: utilities for working with the excellent hunchentoot web server.
• ucw-sandbox: playing around with the UnCommon Web framework.
• texweb: an upload-compile-download web service for TeX and friends based on hunchentoot.

Several of the projects above (dialogues, xsl4mizar, mwiki, mizar-items) are not at heart about the Internet, but involve Internet programming.

Professional Service

• Referee work:
  • Minds and Machines
  • Journal of Universal Computer Science
  • Journal of Logic and Computation
  • Journal of Formalized Mathematics
• Program Committee member:
  • MathWikis-2011
• Language editor for the Central European Journal of Computer Science

Teaching

2011

• Practical Computer Formalization of Mathematics using MIZAR, tutorial given at the 23rd International Conference on Automated Deduction (CADE 23), University of Wrocław, Poland, July 31, 2011.
• Dialogical Logic, winter project short course (joint with Sara L. Uckelman) at the Institute for Logic, Language and Computation, University of Amsterdam.

2010

• Type Theory: New University of Lisbon. (A course in the European Masters Program in Computational Logic.)

Supervision and Academic Service

• Master of Logic thesis committee member for Matthew Wampler-Doty: Evidentialist Logic, Institute for Logic, Language and Computation, University of Amsterdam, 2010.

Non-professional Activities

I maintain several packages for the Fink project, especially packages for automated reasoning and for my favorite text editor Emacs. I enjoy computer programming (I like Lispy-languages the most, especially Common Lisp and Emacs Lisp).

Contact

• Center for Artificial Intelligence
  Faculty of Science and Technology
  New University of Lisbon
  Quinta da Torre
  2829-516 Caparica
  Portugal
  Office: +351-212-948-536 extension 10761
  Fax: +351-212-948-541
  j.alama@fct.unl.pt