Jesse Alama

I am a post-doctoral researcher in the project A Logical Framework for Dialogue Games based at the Theory and Logic Group at the Technical University of Vienna in Austria. Previously I was a postdoc in the DiFoS (Dialogical Foundations of Semantics) project based at the CENTRIA (Center for Artificial Intelligence) at the New University of Lisbon. 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), automated theorem proving, 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 mathematical argumentation. I'm eager to apply techniques from interactive and automated theorem proving to problems in the foundations and philosophy of mathematics, and to make progress in mathematics with the help of computers.

(For more details, consult my CV.)

Upcoming

• With my colleagues Reinhard Kahle, Gregory Wheeler, and Alexei Angelides, I'm a co-organizer for a workshop The Notion of Proof, to be held June 10 and 11 in Porto, Portugal, at a special joint meeting of the American Mathematical Society, the European Mathematical Society, and the Sociedade Portugesa de Matemática (Portuguese Mathematical Society).
• I'm on the program committee for PxTP 2015 (Proof Exchange for Theorem Proving), a workshop to be held on August 2 and 3 as part of the 25th International Conference on Automated Deduction (CADE-25).
• I've been invited to participate in the upcoming seminar at Dagstuhl entitled Information from Deduction: Models and Proofs, to be held from September 13–18, 2015.

See Also

• My publications on MathSciNet.

• GitHub (code)

  If you have any comments, questions, feature requests, or bug reports concerning my code, please do contact me.

• arXiv (preprints)

• Research blog

• TONIGHT: Proponent v. Opponent, a blog devoted to dialogue games and dialogical logic. (Coauthored with Sara Uckelman.)

• Mathoverflow

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).

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).

The Web

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.

Non- and quasi-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, and these days I'm experimenting with Clojure).

Contact

• Theory and Logic Group
  Institut für Computersprachen
  Technical University of Vienna
  Favoritenstraße 9/E1852
  1040 Vienna
  Austria
  alama@logic.at