COMP 4900A COMPUTER SCIENCE LOGIC (Undergraduate) &
COMP 5900F COMPUTATIONAL LOGIC (Graduate)

Also crosslisted as CGSC 5900F and PHIL 5900C.

This course is cross-listed as an undergraduate and graduate course. Senior undergraduate students have to take it as COMP 4900; graduate students as COMP 5900.

Prerequisites: No prerequisites, but contacting the instructor is advised to check the background.

Credits: 0.5

Lectures: three hours a week.

NOTE: THE AUTOMATICALLY SCHEDULED LECTURE TIMES FOR THIS COURSE ARE NOT VERY APPEALING. WE CAN TRY TO CHANGE THEM AT THE FIRST CLASS. IT SHOULD NOT BE DIFFICULT TO FIND A TIME SLOT IN THE EVENING IF NOTHING ELSE IS POSSIBLE OR AVAILABLE BEFORE THAT. SO, IF YOU ARE INTERESTED, SHOW UP AT THE FIRST LECTURE AND WE'LL TRY TO FIND AN ALTERNATIVE SCHEDULE.

This course introduces students to languages of symbolic logic, their semantics, and their use for logically specifying and modelling computational objects and processes in different areas of computing. Techniques for deductive reasoning from those specifications are covered and applied to problems solving through some existing systems for automated reasoning.

Symbolic logic has become a fundamental discipline in computer science, like mathematical analysis for different areas of physics and engineering. Several areas of computer science and computer engineering use logic both implicitly and explicitly, for specifying and modelling systems and automatically reasoning from those specifications. Examples are databases, knowledge management, artificial intelligence, software engineering, programming languages, distributed systems, theory of computing, security, semantic web, ontological engineering, agent systems, etc.

Logic is at the heart of the theory of computing. The models of computation have all their roots in symbolic logic. Today, logic provides powerful methods to characterize and understand computational complexity classes through what is called descriptive complexity. Important complexity classes are also introduced in terms of zero-knowledge and interactive proof systems, which are logical notions. Through the techniques introduced in finite model theory, an area of logic, it is possible to understand the expressive power of formal languages and their applications in computing.

We will use mostly my lecture notes (slides), and also the following book, as a supplement only, for the less computational parts:
"Language, Proof and Logic", by Barwise and Etchemendy. CSLI Publications, 2002.