Senior Research Scientist, CSLI, Stanford University
Cordura Hall, Stanford University, Stanford, CA, 94305-4101, USA
PH: +1 650 723 9030 FAX: +1 650 725 2166
University of Lancaster, UK -- Joint degree in Computing and Mathematics with a heavy emphasis in logic (in the Philosophy department.)
Keith Devlin taught me the meaning of the funny upside-down A's and backward E's that we logicians are so fond of. I remember a lecture by Kit Dodson when he explained homology groups in thirty seconds with the aid of a plastic chair --- something that another professor had tried for almost an entire term to do without success (I'm guessing that it was the chair, but I may be wrong.) Bob Hale introduced me to Beth semantic tableaux and Peter Mott to sequent calculus, natural deduction (and sign language.) John Self supervised my undergraduate thesis on comparing reasoning programs. I wrote propositional provers based on semantic tableaux, resolution and natural deduction. In PASCAL yet! Because I elected to parse standard notation instead of using something sensible like reverse Polish, I think I learned more about parsing than about theorem proving.
The fact thay I remember their names and perhaps even some of the material they taught me is testament to the influence that they had on me (although in the case of Keith Devlin, working in the same building helps the memory.)
University of Edinburgh, UK -- Ph.D. in Artificial Intelligence.
I was a member of the Alan Bundy's Mathematical Reasoning Group, which at that time had been in existence only seven years or so.
Alan has built and maintained the MRG for thirty years, and they have collectively produced a significant body of research. My part was the technique of Gazing, described on my research page, and cited on my publications page. This work had its genesis in two ideas of Alan's on research, which are worthy of emulation in other research groups.
The Mathematical Reasoning Group maintains a collection of notes called "blue book notes" -- yes they are stored in blue ring binders (or they used to be at least). Members of the group are encouraged to write up "half-baked" ideas and put them in the folder, others may later pick them up and cook them. Without the blue book, and a note of Alan's from it, I wouldn't have found my project. There's a link to the blue book notes on the current Mathematical Reasoning Group web page, but access requires a password.
The other of Alan's innovations was the idea of "rationally reconstructing" published research. Much Artificial Intelligence research involves the writing of programs, and then writing up the results of running those programs. Often the write-up is, um, sub-optimal, and it is difficult to see how the claimed results could be obtained from the description. Alan suggested that I rationally reconstruct Woody Bledsoe's UT theorem prover, and this proved to be the genesis of my program Gazer.
I was a contemporary at Edinburgh with among others: Lincoln Wallen (also a schoolmate), Bernard Silver, Richard O'Keefe, Leon Sterling, Jane Hesketh, Stephen Owen, Robert Dale, Mary-Angela Papalaskari, Dave Robertson, Paul Brna, Helen Pain, Mark Drummond, Andy Golding, all of whom contributed to my experience at Edinburgh in ways too numerous, and diverse, to list.
Woody Bledsoe employed me as a post doc (despite my not having officially graduated from Edinburgh). His kindness gave me additional time to complete my dissertation, and to interact with his research group, and the other automated researchers at UT Austin. These included Don Simon, Larry Hines, Ernie Cohen, Tie-Cheng Wang, and Matt Kaufmann. These people collectively taught me how to get by in Texas, which was no mean feat.
Woody Bledsoe introduced me to some folk at the Microelectronics and Computer Consortium (MCC) in Austin where he was the drector of the AI lab. Chief among was Hassan Ait-Kaci, who was investigating the class of what you might call mixed-paradigm programming languages.
Hassan hired me to work on his LIFE programming language. I was responsible for Still LIFE the first interpreter for the language, which subsequently extended into the Wild LIFE compiler. The general theme of the lab was the design of multi-paradigm programming languages. Other languages from our lab included LOGIN (logic and inheritance (object-oriented) programming), LeFun (logic and functional programming) and FOOL (functional and object-oriented programming). LIFE is the three way combination of the paradigms.
The group at MCC included Pat Lincoln and Roger Nasr. I also met Raymonde Guindon through Pat.
The LIFE project at MCC came to an end in 1988, or thereabouts. I decamped to Duke University, where I had a visiting position for one year. Don Loveland and Gopalan Nadathur were supportive in making this happen. I spent the year revisiting my dissertation work (for by now I had graduated, finally).
It was here that I developed my first courses, an undergraduate course in AI and a graduate course in automated reasoning. I discovered that I love to teach. I thank all of the students on whom I practiced the art that year.
One thing was noteworthy about the AI course, and that was that the course was offered at a number of institutions (perhaps four) across North Carolina by the magic of microwave links (I think.) The classroom that I was in had cameras on me, my slides, and the local students. The student desks have voice operated microphones, and a camera automatically panned to the student who was speaking. These pictures were broadcast to the remote sites. Similarly, a split screen displaying the remote students (so to speak) was visible to me and to the local students. I recall few technical problems, and an interesting experience in distance education.
So I applied for this job in Los Angeles. I don't recall who, but someone told me about Trusted Information Systems, who at that time had an office in Santa Monica. I went for an interview, got a job, but for other reasons decided to move to Philadelphia. Then the plot thickened. TIS also had an office just outside Baltimore, Maryland, and Steve Crocker, the head of the Santa Monica office who offered me the position, was about to move to that office. So I said, how bad can the commute be? and signed up for the East Coast office.
I spent more time than was healthy thinking about forty lines of assembly code (a procedure called cb_get_block, I'm still not sure I understand why) from one of the original ARPAnet imps. The project was to specify formally the assumptions under which the code would work, and hence know the conditions under which the imp might crash. Examining the assembly code from this perspective was more more interesting than you might think.
I spent the bulk of my time, however, learning how to use the HOL automated reasoning system. After running through some basic set theory, we set about using the system to verify liveness and progress properties of some computer communication protocols.
After a short while, I realised that I prefer academia -- teaching in particular -- to the commercial sector and decided to look for something closer to home. The answer to the commute question, by the way was 128 miles, 2.5 hours each way. Not an insignificant factor in the decision to move on.
Swarthmore College is a small liberal arts college in suburban Philadelphia. At the time Computer Science was a program, staffed by a full time director Charles Kelemen. Charles was due for a sabbatical, and so he hired me for two years to serve as acting director in the second year. I ended up being there for four years in total.
The students at Swarthmore set about teaching me how to teach. I think that they eventually succeeded, but they made me work hard. Among the students I remember Luke Hankins, Guy Haskins, AC Capehart, Josh Smith, Marc Rieffel and Geoff Noer (my memory had help here from the SCCS alumni page.)
In addition to teaching I returned to my research program in automated reasoning, mostly in collaboration with Sidney Bailin. We did our work on Grover, funded by the NSF, while I was at Swarthmore. I was able to hire some talented students, and dubbed the group Swarthmore College Automated Natural Deduction Laboratory (SCANDAL!). Andrew Merrill, Sam Ehrlichman and Alex Rothenberg, David Sobel were among the people who worked there with me.
An anecdote to illustrate why you should never ask my advice on business matters: The world-wide web was just about getting started around the end of my time at Swarthmore. I asked Dan Kohn what he was going to do after graduation. He told me that he and a group of students (including Guy Haskin and Eiji Hirai) were starting a company to sell things on the web. I demonstrated my business savvy by asking who would want to use the Internet to buy stuff?. Netmarket became the first company to perform a secure retail transaction on the Internet.
In 1994 John Etchemendy was kind enough to arrange for one month's funding for a new arrival in the Bay Area to write a grant proposal in hopes that we could arrange a collaboration that would allow me to stay at Stanford for a while. The proposal was not successful, indeed, I am not sure that it was ever submitted. However, after (at the time of writing) more than ten years I am still a CSLI as a research scientist.
I am now the project manager for the Openproof project at CSLI. We primarily produce educational software packages for teaching undergraduate logic. I've written more Java code and shell scripts than is good for a person, the end result being desktop applications Fitch, Boole, Tarski's World, and the Internet-based grading service Submit and The Grade Grinder, all available as part of the Language, Proof and Logic package. My collaborators on this project are currently John Etchemendy, Albert Liu, Nik Swoboda and Andrei Aron. The list of past members of the project is long, and I won't repeat it here.
I occasionally get to teach logic to undergraduates too. I've taught Stanford's courses Philosophy 57, Philosophy 159 and Philosophy 160a.
On occasion, I review books for CSLI Publications. I was the general chair for the Diagrams 2006 conference held at Stanford in June 2006.