Jesse Alama

[Picture of me]

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


See Also

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.

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.

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.

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:

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