Symbolic Logic and Applications

This course was taught in Monsoon 2025. For the latest
iteration of the course, please see the teaching page.

René Magritte, La Reproduction Interdite (1937)

Logistics:

Credits: 4
Classes: Tuesdays and Thursdays, 10:10am to 11:40am
Classroom: AC-04-LR-007
Teaching Assistant: Smayan Agarwal (smayan.agarwal_ug25@ashoka.edu.in)

Course Description: Symbolic logic presents an intriguing challenge in computer science: balancing the need to express complex ideas with the ability to solve problems efficiently. This course explores how we can create systems that are powerful enough to describe useful scenarios, yet still allow computers to reason about them effectively. We'll examine various approaches to this balance, learning how theorists and practitioners have developed ways to represent knowledge and automate reasoning. Without requiring any prior background in logic or advanced mathematics, this course offers a gentle yet rigorous introduction to deductive systems, propositional and predicate calculi, and higher-order logic. We will also learn about the applications of these formalisms to constraint solving, program verification, automated reasoning, and interactive theorem proving. The objectives of this course are to:

  1. Develop a foundation in the core concepts and deductive systems of propositional logic, predicate logic, and higher-order logics, including their syntax, semantics, and proof techniques,
  2. Gain knowledge of the practical applications of symbolic logic in a variety of domains, such as constraint solving, program verification, automated reasoning, and interactive theorem proving,
  3. Understand the trade-off between expressiveness and algorithmic tractability in logical formalisms, and the importance of finding reasonable compromises between these conflicting goals,
  4. Understand the fundamental limitations of formal logic, reasoning, and computation, and
  5. Develop hands-on experience working with tools like SAT solvers and interactive theorem provers, bridging the gap between theoretical reasoning and practical considerations.

Prerequisites: First, the course will require a certain amount of maturity at least at the level of [CS-2212] Data Structures and Algorithms. Second, functional knowledge of a programming language (preferably Python or Rust) is required for completing the assignments and projects in this course.

Grading: A serious student of a subject is not an idle spectator to a variety show but learns best by active involvement. This is particularly true of mathematical subjects. This course is structured to incentivise involvement through the following:

  1. Assignments: The course includes three programming problem sets. These are designed to reinforce lecture material and develop practical skills in applying theoretical concepts. They constitute a third of the grade.
  2. Course Project: Students will undertake a project on invariant synthesis (which requires programming). This hands-on experience allows for practical application of course concepts and fosters deeper engagement with the subject matter. The project may be done either alone or in pairs. It carries a third of the grade.
  3. Periodic Assessments: Five, in-class, closed-book, assessments carry the remaining grade.

Policies: Please note the following policies:

Support: Students are encouraged to reach out to University offices such as the Office of Learning Support, Ashoka Center for Well-Being, and Center for Writing and Communication for additional support.