CS 486: Applied Logic
 Spring 2001

Project

The Project is due at the final exam, which is
Friday, May 18, from 12:00-2:30 pm in Hollister 372.
Here is a list of possible projects that were mentioned in lectures.
1. Historical studies:
 
  • Read about the origins of first-order logic in From Frege to G�del and relate to our account in class.
    		•
     
  • Read about the controversy over the law of excluded middle. There is good material on the Web.
    		•
    2. Develop first-order logic as a Hilbert system. See books such as A. Church, Introduction to Mathematical Logic, Vol I. Compare to tableau.
    3. Develop propositional logic from the start using refinement logic by rewriting Smullyan, p. 15-17.
    4. Write up a complete account of our treatment of order and algebraic structures in first-order logic.
    5. Give a proof that first-order monadic predicate logic is decidable.
    6. Prove Church's theorem that validity in first-order logic is not decidable by formalizing Turing machines or a simple programming language.
    7. Using refinement logic with primitive recursive functions over Z (lambda-PRL), prove some interesting program correct. Read the article Proofs as Program, by Bates and Constable (see Nuprl Web page).
    8. Interactions with the PRL research group. Various researchers are willing to talk with you about specific projects:
     
  • Reflection in first-order logic, a topic that leads to Tarski's theorem about the undefinability of truth. Contact Eli Barzilay (eli@cs.cornell.edu).
    		•
     
  • The towers of Hanoi problem stated and solved as a theorem. Contact Dr. Stuart Allen (sfa@cs.cornell.edu).
    		•
     
  • Reading and explaining a formal theory of lists from the Nuprl 5 library. Contact Tina Nolte (tan4@cornell.edu).
    		•
     
  • Learning to operate JProver, a fully automatic first-order theorem prover. Contact Dr. Kreitz.
    		•
    9. Reading interesting papers about logic and reporting on them. Here are some examples that I have copies of:
     
  • Assigning Meaning to Proofs, R. Constable.
    		•
     
  • Implementing Metamathematics, R. Constable, Douglas Howe.
    		•
     
  • A Basis for a Mathematical Theory of Computation, John McCarthy.
    		•

    HOME


    Webms: Juanita Heyerman, Department of Computer Science, Cornell University, Ithaca, NY. Mail to: juanita@cs.cornell.edu