My main interest is applying formal logic to helping people reason. I'm into formalization of arguments, intelligence analysis and general cognitive aids (e.g. memory aids); but I'm also into structuring text, representing arguments diagrammatically, "theory engineering": the dynamic non-monotonic process of formalizing knowledge; argumentation-based tutoring (where the system teaches subject X by actually having knowledge of X in the form of formal theories) and cognitive tutors (i.e. systems that have a model of the learner). I am also interested in Computational Philosophy of Science.
== How Lisp is good for me ==
* functions as 1st class objects saves me from writing for-loops, by using mapcar.
* data is executable: I use eval in my backward-chaining theorem-provers, in order to check that the steps actually follow. The function calls are inference rules of the logic.
* no types to get in the way
== Projects ==
SOLVER - Equational Solver (in alpha) For my EBE project, I have written an equation solver in Lisp. It's currently hackish, and I want to make it neater by defining the set of "valid moves" and extend it to incorporate proof-planning.
ARGAME - Argumentation Games (in passive development) is an implementation of the standard Lorenzen argumentation game (the existence of a winning strategy corresponds to intuitionistic validity). A variation on the rules will implement classical FOL.