Next: About this document
CS 486 Applied Logic Possible Projects
Spring 19977
-
set theory-compare development with Suppes.
- Prove IVT in
-theory-compare to formal topology.
- Develop further our first-order theory of prop calculus-prove Eval theorem, define tautologies, represent Tableau proof as formula.
- Nuprl development
- an algorithm like max-seg-sum
- develop a CS280 theorem
- exercises in Caldwell theory of prop calculus
- Nuprl-Light practice
- Boolean rings as a theory with rewrites
- logic of subtyping
- Typed Logic with Subtyping-basic theorems in Smullyan style
- Nuprl formal hypertext
- explain Caldwell library
- explain Achilles library
- explain Cantor theorem
- Prolog-relate Prolog to Nuprl
follow my hints
- How humans understand arguments (``deformalizing'')
- Role of Natural Language (NL) syntax in immediate inference
- Read Prawitz on Natural Deduction (ND) related to Tableau
- Read Constable/O'Donnell on Block ND, relate to Tableau
- Read Kozen on
-calculus
- Read Kozen BKR algorithm