Logistics:

Credits:	4
Classes:	Tuesdays and Thursdays, 10:10am to 11:40am
Classsroom:	AC-04-LR-007
Teaching Assistant:	Smayan Agarwal

Links:

Course Outline and Lectures

Course Project Guidelines

Resources and Reading Materials

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 four programming problem sets. These are designed to reinforce lecture material and develop practical skills in applying theoretical concepts. They constitute 25% of the grade.
2. Course Project: Students will undertake a project on constraint solving (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. Project topic needs to be approved by the instructor. It carries 25% of the grade.
3. Periodic Assessments: Six, in-class, closed-book, 45 minute quizzes carry the remaining grade.

Policies: Please note the following policies:

• Attendance: Regular attendance is expected, though not mandatory. Please arrive on time; students more than 5 minutes late should not enter, as this disrupts the class.
• Classroom Conduct: Food is not permitted, though beverages (hot or cold) are allowed. Notes should be taken on paper or a tablet/iPad. Laptops and phones are not to be used during class unless prior accommodation has been granted by the Office of Learning Support (ols@ashoka.edu.in).
• Assignments: Timely submission of assignments is required. Late submissions will not be accepted. Exceptions must be approved by the Director of OAA (director.oaa@ashoka.edu.in).
• Academic Integrity: As outlined in Ashoka's Academic Integrity Policy (see MyAshoka → Information and Documents → Office of Academic Affairs), plagiarism and other violations (including but not limited to unauthorized use of AI tools) are serious offenses. Any violation will result in a failing grade (F) for the course. Please review the policy carefully.

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.