The first notions of formal logic were invented over 2000 years ago as philosophers attempted to develop systematic approaches for arriving at statements that were true. By the time we approach adulthood, we will have heard many people say (or we will have said ourselves): “that seems logical”, or “you’re being illogical”. By this, we understand that (in the first case) sound reasoning principles have been used, whereas in the latter case someone may be stating a conclusion that cannot be justified by sound reasoning from an initial set of true facts. This “every day” notion of logic that manifests itself in the arguments that we make in natural language is sometimes referred to as informal logic.
In contrast, in this course, we will study concepts related formal logics. In simple terms, a formal logic consists of some syntax for stating claims (properties that are either true or false) about the world (or some other more specialized domain in which we are interested) and rules for deriving claims that are guaranteed true.
Formal logic is deeply tied to computer science, because computers are great at “blindly following rules”, and many of the issues in which we are interested in computer science can be phrased as basic claims and systems of rules. The basic gates and circuits from which computers are built, the behavior of our programs as they execute, the protocols that our computer systems used to communicate, the expert systems that provide automated assistance to doctors, pilots, etc. all can have their behaviors defined or explained using formal logics. This is extremely important because it provides the basis for automated ruled-based reasoning for these systems.
In this course, we will learn the basic elements found in a formal logic including syntax for claims and rules for making deductions. We will also learn how to judge if our rules are suitable in the sense that they only lead us to claims that match the reality of the domain we are reasoning about.
Our focus will be on formal logics for reasoning about program behavior and for programming directly in terms of logic. We will see how tools based on logic are used to reason about safety and security critical software, network security, and security protocols.
The “Logika: Programming Logics” online course-notes are the main course materials. Other references will be provided as the course unfolds.
| Time: | Tuedays (T) & Thursdays (U), 11:05am - 12:20pm |
|---|---|
| Place: | DUE1073 |
3 credits
John Hatcliff, Office: 2160 Engineering Hall, Office Hours: 12:20-1pm Tuesday and Thursday
Final letter grades are assigned based on the following scale: 90% to earn an A, and 80% to earn a B; 70% to earn a C, and 60% to earn a D.
Homeworks are due almost every week and are to be submitted through GitHub. Each student will be given a private repository that can be used to commit homework assignments. Assignments that are late will not be graded (based the git log), unless in case of documented medical or family emergencies.
Exams will be closed-book and closed notes. The final will be comprehensive, but with emphasis on the latter part of the course.
If you think the instructor or the TAs have made an error when grading your test or your homework, you are of course very welcome to ask for clarification. But complaints about judgment calls, like how much credit to give for a partially correct solution, are not encouraged (it is like arguing balls and strikes).
In general, there will be NO make-up exams (and homework)! Special consideration will be given in only exceptional circumstances. Exceptional circumstances are generally limited to:
If you believe you qualify for exceptional treatment, you must notify the instructor prior to the date of the exam or exercise to be missed.
Kansas State University has an Honor System based on personal integrity, which is presumed to be sufficient assurance in academic matters one’s work is performed honestly and without unauthorized assistance. Undergraduate and graduate students, by registration, acknowledge the jurisdiction of the Honor System. The policies and procedures of the Honor System apply to all full and part-time students enrolled in undergraduate and graduate courses on-campus, off-campus, and via distance learning. The honor system website can be reach via the following URL: http://www.ksu.edu/honor.
A component vital to the Honor System is the inclusion of the Honor Pledge which applies to all assignments, examinations, or other course work undertaken by students. The Honor Pledge is implied, whether or not it is stated: “On my honor, as a student, I have neither given nor received unauthorized aid on this academic work.” A grade of XF can result from a breach of academic honesty. The F indicates failure in the course; the X indicates the reason is an Honor Pledge violation.
For a more complete discussion of these issues see the course policies for the College of Engineering at Kansas State University: http://www.cis.ksu.edu/resources/intradept/syllabuspolicies.
All lectures and course materials are copyrighted. During this course students are prohibited from selling notes to or being paid for taking notes by any person or commercial firm without the express written permission of the instructor teaching this course.
The course material, including this syllabus, is adapted from the one taught by David A. Schmidt, Torben Amtoft, and Robby.