Automated Reasoning

---

COURSE:  CIS4930/CAP5632

TIME:  11:00-12:15 MTWRF 103 Love Building

INSTRUCTOR:  Hilbert Levitz
      Office 168 Love Building
      Phone 644-1796
      E-Mail:  levitz@cs.fsu.edu
     Office Hours:  T,R 2:30-3:30 and by appointment.

GRADER:  Sangeetha Murali
      E-Mail: murali@cs.fsu.edu
      Contact Time: After Class
      Office: 106B Carrothers

PRE-REQUISITES:  A course in discrete mathematics.

OBJECTIVES:  To provide the fundamentals in the theory of automated reasoning,  and to bring students to the point where they can deal with automated reasoning programs based on these fundamentals.
 

TEXT:    Chang and Lee, Symbolic logic and Mechanical Theorem Proving, Addison Wesley.
                The retail price of the book is $60. The bookstore will have used copies for $45.
                Used copies can be purchased even more cheaply through Amazon.com

              Other Texts on Automated Reasoning.
 

MANUALS:   OTTER Manual.

                       SWI PROLOG Manual
 

EXAM DATES:

Mid Term Test:     Friday May 26

Final Exam:           Last day of term.  Friday June 16 at regular class meeting time/place.

GRADES:          Midterm       35%
                            Final Exam   45%
                            Problems      20%

TOPICS IN COURSE:

1) Introduction and  Propositional Logic.

   Chapter 1  Sec. 1.1 - 1.2
   Chapter 2  Sec  2.1 - 2.6

2) First Order Logic

   Chapter 3  Sec 3.1-3.4

3) Skolem Standard Forms, Herbrand Universes and Herbrand's Theorem.

     Chapter 4  Sec 4.1-4.3
                     Sec 4.5 (Omit Theorem 4.3)

4) The Davis Putnam Method For Propositional Logic.

   Chapter 4  Sec 4.6
 

5) The Resolution Principle For Propositional Logic.

   Chapter 5  Sec 5.1-5.2
 

4) Prawitz's Unification Algorithm.

   Chapter 5  Sec 5.3-5.4

5) The Resolution Method For Predicate Logic

   Chapter 5  Sec 5.5
   Compleness of Resolution (as per discussion in class)
      Sec 5.7
      Sec 5.8

6) Linear Resolution.

   Chapter 7  Sec 7.1-7.2
 

7) The Logical Basis of PROLOG.

This section is not based on our text. Students must be careful
 to attend lectures, as there is no corresponding reading assignment.

Bare bones instructions for Prolog.
 

8) The Set of Support Strategy.

   Chapter 6  Sec 6.5B

9) The Interactive Theorem Prover OTTER.

OTTER is a software package developed by Argonne National Lab. It is mounted on CS sytems. Students will run selected problems on OTTER.

Bare bones instructions for OTTER.

Students are encouraged to visit the web page of William McCune, the creator of OTTER. There is to be found a discussion
of various problems solved by otter, as well as information about otter itself.

HOME WORK PROBLEMS:   Do not have to be turned in except when explicitly stated so in class. Click here for a list of the problems .

HONOR CODE: As in any class at F.S.U., it is your responsibility to read, understand, and conform to the Student Honor Code as set forth in the University General Bulletin and the Student Handbook. Any violation of these policies, especially involving the giving or receiving of help on any assignment, will result in severe penalties likely including an F in the course and proceedings before the honor court.

ATTENDANCE:  Roll will be taken at each class period.  More than four unexcused absences will lead to a drop in final grade.
 

DISABILITIES: Please advise the instructor of this class at your earliest convenience (minimum of five working days) if you have a disability that will require a reasonable accomodation for any of the activities in the course schedule.