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: Thursdays 11 am - 12 pm or by appointment (email communication is preferred). Office is at Joshi 465

Grading assistant: Aaron Eberhart (email: aaron.eberhart [AT] gmail.com). Help desk: Wednesdays, 11-12am in Russ 417.

Schedule: Tuesdays, Thursdays 3:30 pm - 4:50 pm in Russ 355.

Exam Schedule: There will be three exams on Saturdays: October 1, November 5, and December 10. All exams will start at 9:30 am and 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 (8/30, 9/1): Datalog - Introduction, Syntax, Semantics
  • Homework 1, due on Tuesday, 09/06/2016, 3:30pm.
• Week 2 (9/6, 9/8): Datalog - Semantics
  • Homework 2, due on Tuesday, 09/13/2016, 3:30pm.
• ​Week 3 (9/13, 9/15): Datalog - Fixed-point Semantics
  • Homework 3, due on Thursday, 09/22/2016, 3:30pm.
• Week 4 (9/20, 9/22): Datalog - Fixed-point Semantics
• Week 5 (9/27):  Propositional Logic - Syntax, Semantics
• In-term Exam 1 (Saturday, 10/1, starting at 9:30 am in Russ 144)
• Week 6 (10/4, 10/6): Propositional Logic - Semantics, Expressing Datalog in Propositional Logic
  • Homework 4, due on Tuesday, 10/11/2016, 3:30pm
• Week 7 (10/11, 10/13): Propositional Logic - Equivalences, Normal Forms, Tableaux Algorithm
• Week 8: (10/18, 10/20): Propositional Logic - Tableaux Algorithm
  • ​Homework 5, due on Tuesday, 10/25/2016, 3:30pm
• Week 9 (10/25, 10/27): Propositional Logic - Tableaux Algorithm, Theoretical Aspects (time-permitting)
• Week 10 (11/1): First-order Predicate Logic - Syntax
• In-term Exam 2 (Saturday, 11/5, starting at 9:30 am in Russ 144)
• Week 11 (11/8, 11/10): First-order Predicate Logic - Syntax, Semantics
  • ​Homework 6, due on Thursday, 11/17/2016, 3:30pm
• Week 12 (11/15, 11/17): First-order Predicate Logic - Equivalence, Normal forms
• Week 13 (11/22):  First-order Predicate Logic - Equivalence, Normal forms, (Note: there's no class on 11/24 due to Thanksgiving holiday).
• Week 14 (11/29, 12/1): First-order Predicate Logic - Tableaux Algorithm
  • Additional exercises for exam preparation. Not for submission.
• Week 15 (12/6): First-order Predicate Logic - Tableaux Algorithm, Theoretical Aspects (time-permitting)
• Final Exam (Saturday, 12/10, starting at 9:30 am in Russ 144)

Course evaluation:

• (Almost) weekly homework exercises, counted towards 10% of final course grade.
• In-term exam 1, counted towards 30% of final grade.
  Date: Saturday, 10/1/2016 (starting at 9:30am, duration 90 minutes)
• In-term exam 2, counted towards 30% of final grade.
  Date: Saturday, 11/5/2016 (starting at 9:30am, duration 90 minutes)
• Final exam, counted towards 30% of final grade.
  Date: Saturday, 12/10/2016 (starting at 9:30am, duration 90-120 minutes)
  • Grading will follow a standard scale (100 >= A >= 90, 90 > B >= 80, 80 > C >= 65, 65 > D >= 55, 55 > F >= 0). The instructor reserves the right to curve the scale.

Notes on course evaluation:

• Attendance during exams are required (including for those who registered in the online section). Exceptions can only be made in documented cases of emergencies.
• On homework exercises:
  • Exercise sets are posted (almost) weekly.
  • Most exercises are graded and worth 4 points each.
  • A vsmall number of homework exercises are optional, and will be marked as so in the exercise sheets. These ones are not graded, but are still useful for you to dig deeper to the course materials.
  • 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 (preferred); or
    • Put in CS 2210 mailbox in the department office (ask the front desk); or
    • If you registered for the distance learning section, upload a PDF of your solution to the appropriate Dropbox folder in Pilot. It is your responsibility to ensure that your solution is readable by the grader. Please do not upload a file in format other formats (jpeg, doc, etc.)
  • 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.
  • It is allowed to discuss how to solve the exercises with your friends. However, each person writes the solutions entirely by him/herself.
  • 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.