Home » forums » LtU Forum

Course in mathematical logic with applications to computer science

I am a mathematics professor *. I was approached recently by one of our talented computer-science undergraduates at the university where I work, who is in her senior year and interested in taking a reading course in the applications of mathematical logic to computer science.

This undergraduate recently completed a summer project with the author of Twelf, formalising the ‘simplification’ SASyLF, and I get the impression that her interest is much more in the sorts of logic that arise in computer-assisted (mathematical) theorem proving than in the logic of programming per se—that is, I think that she's not particularly interested in temporal logic and other such proving-programs-correct stuff. She specifically mentioned wanting to understand the SLDNF logic behind Prolog, and I feel qualified to start there, but don't really know where to go next. I guess that I want to dig deeper into HM type inference (although she's already studied TAPL on her own, I believe), the calculus of inductive constructions, and that sort of thing—but these are mostly just (to me) buzzwords that I've picked up, and I'd like to put together some sort of coherent reading course. Suggestions?

* To clarify, I'm mentioning this not to brag, but rather to give an idea of what a stretch this course will be for me. (I'm a representation theorist, not a logician.) Thus, don't hesitate to give references to things that “everybody knows”—almost assuredly, I don't!

By L Spice at 2009-10-14 22:40 | LtU Forum | previous forum topic | next forum topic | other blogs | 6794 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Proof theory?

It sounds like your undergraduate may be more interested in proof theory, rather than type theory. (The two are of course closely related via Curry-Howard correspondence, but are distinct disciplines.) I'm not at all an expert, but I have found Troelstra & Schwichtenberg, Basic Proof Theory, to be a useful introduction and survey of the field - assuming that this is the field that is of interest. It has a chapter on SLD-resolution.

By DavidA at Thu, 2009-10-15 09:06 | login or register to post comments

Gallier's out of print book

Gallier's out of print book "Logic for Computer Science: Foundations of Automatic Theorem Proving" is available from his website. In particular, it has a chapter devoted to SLD-resolution and Prolog (and also covers a lot more).

By dpmulligan at Thu, 2009-10-15 09:55 | login or register to post comments

Love free books

I'm always happy when I can find a good reference without requiring students (who aren't so lucky as we are about getting desk copies) to purchase something expensive. Thanks a lot for the link!

By L Spice at Fri, 2009-10-16 15:49 | login or register to post comments

great suggestion

Jean Gallier is an excellent writer and its a pity this book is out of print. If you want to learn Mathematical Logic, there is no better book than Ebbinghaus,Flum,Thomas, reads like formal poetry and it has a chapter devoted to Logic programming.

By harshrc at Sat, 2009-10-17 23:01 | login or register to post comments

Paulson's Logic and Proof

Larry Paulson's lecture notes, Logic and Proof, should be entirely relevant as a starting point for your wonderful-sounding student.

Uniform Proofs as a Foundation for Logic Programming is an important paper for higher-order extensions to LF, and will need some backup from proof theory; some pages from Proofs & Types would fit the bill.

The risk with reading courses is that you can cover much interesting material without mastering it. Your student sounds like she knows lots, what's maybe worth spending time on, is where her knowledge is patchy. The nice thing about starting with lecture notes is that they come with exercises to get some kind of fix on this.

By Charles Stewart at Thu, 2009-10-15 13:47 | login or register to post comments

Great pointers

Thanks very much (to you and to everyone) for your great pointers. You say, and I 100% agree,

Your student sounds like she knows lots, what's maybe worth spending time on, is where her knowledge is patchy.

My worry is less about the patchiness of her knowledge, and more about the patchiness of mine! As I mentioned, I'm a mathematician, not a computer scientist (or even a logician), and most of what I know about CS I've picked up just from reading boards such as this one and programming in Haskell. Thus, I'm looking for something that will provide enough guidance that even an inexperienced guide such as I can use it successfully. The lecture notes look promising in that respect.

(The uniform-proofs paper has Frank Pfenning as one of its coauthors, too, so I imagine that it's right up her alley. :-) )

By L Spice at Fri, 2009-10-16 15:48 | login or register to post comments

Computational Modelling

Computational Modelling of Mathematical Reasoning by Alan Bundy here

By Marlene Miller at Sat, 2009-10-17 04:44 | login or register to post comments

Lemma the Ultimate

I'm very new to these subjects myself, but I've recently started a blog documenting my exploration of them. I try to link to relevant resources when possible.

Could have some helpful links:
http://lemmatheultimate.com

By larrytheliquid at Mon, 2009-10-19 07:01 | login or register to post comments