COM S 671: Introduction to Automated Reasoning

Cross-Listing: Not cross-listed.

Topics in modern logic needed to understand and use automated reasoning systems such as HOL, Nuprl, and PVS. Special emphasis on type theory and logic and on tactic-oriented theorem proving.

Offered: Fall only

Prerequisites: (COM S 611 and graduate standing) or permission of instructor.

Grade options: Letter or S/U

Credit hours: 4

Recent offerings:

• http://www.cs.cornell.edu/courses/cs671/2004sp
• http://www.cs.cornell.edu/courses/cs671/2003sp
• http://www.cs.cornell.edu/courses/cs671/2002sp
  • Bob Constable