Every Computer Scientist should have at least a basic knowledge about the foundations of logic which is important for formal understanding of many important areas in computer science. Virtually all areas in computer science require various degree of formal treatment based on logic. This includes computability and complexity theory, formal semantics of programming language, design and implementation of digital circuitry for microprocessors, database query languages and engine, specification and verification of software, knowledge representation for artificial intelligence, robotics and web information systems, and many other application areas. Understanding about the foundations of logic will crucially help you in gaining better understanding of those areas you will certainly encounter in the future.

This course is intended to provide an introductory-level, but detailed, treatment of the foundations of logic which covers Datalog, propositional logic, and first-order predicate logic as the most fundamental logical formalism. Throughout the course, there will be two important aspects which will be discussed thoroughly, namely modeling of knowledge and computation through reasoning. Modeling of knowledge is related to how logic as a language is syntactically formed and how it is semantically interpreted to represent knowledge. Meanwhile, the reasoning is related to how we can computationally infer further knowledge from existing one by operating on the syntactic level while making sure that the given semantics is adhered to.

Instructor: Dr. Adila A. Krisnadhi (email: krisnadhi.2 [AT] wright.edu)

Instructor's office hours: Wednesdays 11 am - 12 pm or by appointment (email communication is preferred). Office is at Joshi 465

Schedule: Mondays, Wednesdays, Fridays 12:20 - 1:15 pm in Russ 355.

Exam Schedule: There will be three exams: February 11 (Saturday), March 25 (Saturday), and April 26 (Wednesday), 2017. The first and second exams will start at 10:00 am, while the third/final exam will start at 12:30pm. All exams will be held on Russ 355. Attendance is strictly required.

Course materials:

• Lecture manuscript (may be updated throughout the semester, see latest version date on the first page of the manuscript).
• Uwe Schöning, Logic for Computer Scientists, Birkhäuser, 2008 - Section 1.1, 1.2, 1.4, 2.1, 2.2, and 2.3.
• Mordechai Ben-Ari, Mathematical Logic for Computer Science, 2nd Ed., Springer, 2001 - Section 2.6 and 5.5.

Slides and lecture manuscript will be posted here as they become available. However, relevant for the exams is the material presented in class. If you miss a class, it's your responsibility to get all missing information, e.g. from classmates.

Course outline:

• Week 1 (1/9, 1/11, 1/13): No class on the first week (Instructor is away)
• Week 2 (1/18, 1/20): Datalog - Introduction, Syntax, Semantics - Note: No class on 1/16 (MLK Day Holiday)
  • Exercise Sheet 1 (due date: 1/27/2017, before class).
• ​​Week 3 (1/23, 1/25, 1/27): Datalog - Semantics, Fixed-point Semantics
• Week 4 (1/30, 2/1, 2/3): Datalog - Fixed-point Semantics
  • Exercise Sheet 2 (due date: 2/6/2017, before class).
• Week 5 (2/6, 2/8, 2/10):  Propositional Logic - Syntax, Semantics
• Exam 1 (Saturday, 2/11, starting at 10:00 am in Russ 355)
• Week 6 (2/13, 2/15, 2/17): Propositional Logic - Semantics, Expressing Datalog in Propositional Logic
• Week 7 (2/20, 2/22, 2/24): Propositional Logic - Equivalences, Normal Forms, Tableaux Algorithm
• Spring Break (2/27 - 3/4) - NO CLASS
• Week 8: (3/6, 3/8, 3/10): Propositional Logic - Tableaux Algorithm
  • Exercise Sheet 3 (due date: 3/13/2017, before class).
• Week 9 (3/13, 3/15, 3/17): Propositional Logic - Tableaux Algorithm
• Week 10 (3/20, 3/22, 3/24): First-order Predicate Logic - Syntax
• Exam 2 (Saturday, 3/25, starting at 10:00 am in Russ 355)
• Week 11 (3/27, 3/29, 3/31): First-order Predicate Logic - Semantics
• Week 12 (4/3, 4/5, 4/7): First-order Predicate Logic - Equivalence, Normal forms
  • Exercise Sheet 4 (due date: 4/14/2017, before class)
• Week 13 (4/10, 4/12, 4/14):  First-order Predicate Logic - Tableaux Algorithm
• Week 14 (4/17, 4/19): First-order Predicate Logic - Tableaux Algorithm
  • There will be no class on Friday, 4/22.
• Exam 3 (Wednesday, 4/26, starting at 12:30pm in Russ 355)

Course evaluation:

• Homework Group Exercises, counted toward 4% of final grade.
  • Exercises are done by a group of exactly two students. Everyone must find a partner!
  • You are free to choose your partner for doing the exercise sets, but once you choose a partner, you are not allowed to change to a different partner.
• Exam 1, counted toward 32% of final grade.
  Date: Saturday, 2/11/2017 (starting at 10:00am, duration 90 minutes)
• Exam 2, counted toward 32% of final grade.
  Date: Saturday, 3/25/2017 (starting at 10:00am, duration 90 minutes)
• Exam 3, counted toward 32% of final grade.
  Date: Wednesday, 4/26/2017 (starting at 12:30pm, duration 90-120 minutes)
• Grading will be based on the following cutoff scores: 100 >= A >= 90, 90 > B >= 80, 80 > C >= 65, 65 > D >= 55, 55 > F >= 0. The instructor reserves the right to adjust the cutoff scores.
• Attendance during exams are required. Exceptions can only be made in documented cases of emergencies.

Notes on homework exercises:

• Exercise sets are posted (roughly) weekly. You should complete each exercise set in a group of two. 
• Deadline of each exercise set is usually one week after it is posted. Due dates will be given in the exercise set and in the course website.
• Explain and justify the solution of each exercise you submit whenever appropriate.
• Submit solutions either in handwriting or typed.  Handwriting must be easily readable. If you type your solution, do not use MS Word since its math formatting is difficult to read. Use LaTeX instead.
• Submission methods: Hand it in to me directly before the class on the due date.
• Late submissions will not be graded -- so please avoid submitting late.
• Staple multiple pages so they don't get lost in stack (no paper clips or other methods). Put your name on each sheet you submit. Remove fuzzy margins.
• If we spot two identical or nearly identical write-ups, or two versions, one of which looks like a copy of the other, both parties will receive 0 points.
• Homework exercises are the tough part of the class. If you stay on top of them, exams should be relatively easy.