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: 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: Jonathan Carpenter (email: carpenter.102 [AT] wright.edu -- help desk hours: Wednesdays, 10:30 - 11:30 am, in Russ 417.).
Schedule: Tuesdays, Thursdays 9:30 am - 10:50 am in Russ 355
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/12, 1/14): Datalog - Introduction, Syntax, Semantics
- Slide 0: Class Organization (updated with new exam schedule).
- Exercise Sheet 1 - due date: 1/19 - 9:30 am
- Week 2 (1/19, 1/21): Datalog - Semantics
- Exercise Sheet 2 - due date: 1/26 - 9:30 am
- Week 3 (1/26, 1/28): Datalog - Fixed-point Semantics
- Exercise Sheet 3 - due date: 2/9 - 9:30 am (Note: exercise 25 and 26 are optional - they will not be graded, though you will find them instructive if you attempt to do them).
- Week 4 (2/2, 2/4): Datalog - Fixed-point Semantics
- Week 5 (2/9, 2/11): Propositional Logic - Syntax, Semantics, In-term Exam 1 (Thursday, 2/11, starting at 9:20 am)
- Week 6 (2/16, 2/18): Propositional Logic - Semantics, Expressing Datalog in Propositional Logic
- Exercise Sheet 4 - due date 2/23 - 9:30 am
- Week 7 (2/23, 2/25): Propositional Logic - Equivalences, Normal Forms, Tableaux Algorithm
- Exercise Sheet 5 - due date 3/15 - 9:30 am
- Week 8: Spring break!
- Week 9 (3/8, 3/10): Propositional Logic - Tableaux Algorithm
- Week 10 (3/15, 3/17): Propositional Logic - Tableaux Algorithm, Theoretical Aspects (time-permitting)
- Week 11 (3/22, 3/24): First-order Predicate Logic - Syntax, In-term Exam 2 (Thursday, 3/24, starting at 9:20 am)
- Week 12 (3/29, 3/31): First-order Predicate Logic - Syntax, Semantics
- Week 13 (4/5, 4/7): First-order Predicate Logic - Syntax, Semantics
- Exercise Sheet 6 - due date 4/14 - 9:30 am
- Exercise Sheet 6 solutions
- Week 14 (4/12, 4/14): First-order Predicate Logic - Equivalence, Normal forms, Tableaux Algorithm
- Week 15 (4/19, 4/21): First-order Predicate Logic - Tableaux Algorithm, Theoretical Aspects (time-permitting)
- Final Exam (Tuesday, 4/26, starting at 8:00 am)
Course evaluation:
- (Almost) weekly homework exercises, counted towards 10% of final course grade.
- In-term exam 1, counted towards 30% of final grade.
Date: Thursday, 2/11/2016 (starting at 9:20am, duration 90 minutes) -- note: we start a bit earlier than the usual class time! - In-term exam 2, counted towards 30% of final grade.
Date: Thursday, 3/24/2016 (starting at 9:20am, duration 90 minutes) -- note: we start a bit earlier than the usual class time! - Final exam, counted towards 30% of final grade.
Date: Tuesday, 4/26/2016 (starting at 8:00am, duration 90-120 minutes) -- note: we use final exam schedule from the WSU registrar. - 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. Exceptions can only be made in documented cases of emergencies.
- On homework exercises:
- Exercise sets are posted weekly.
- Most exercises are graded and worth 4 points each.
- A very small 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 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).
- Late submissions are not guaranteed to 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.
