Foundations of Automated Reasoning

Dates: 10-14 January 2028 Venue: Ashoka University 

This international workshop is a joint collaboration of Ashoka University and International Centre for Theoretical Sciences, Bengaluru.
 
 

About the Workshop

Automated Reasoning is an area of computer science concerned with understanding and formalizing reasoning processes in a way that enables the construction of software systems capable of reasoning completely, or nearly completely, automatically. It lies at the intersection of computational logic, theoretical computer science, and artificial intelligence, and plays a central role in the development of reliable and trustworthy computing systems. The field encompasses a broad range of foundations, techniques, and applications, including:
● Satisfiability (SAT) and Satisifiability Modulo Theory (SMT) Solving: Design and implementation of efficient decision procedures for determining the satisfiability of complex logical formulas across multiple theories.
● Verification and Synthesis: Formal verification of software systems and cryptographic protocols, and automated synthesis of programs from logical specifications.
● First-Order Logic Provers: Fully automated proof discovery using resolution based reasoning, without human intervention.
● Proof Assistants: Principles and theoretical foundations of interactive theorem proving, including type theory, proof automation, and trusted proof checking.

Topics to be Covered

1. Propositional & First-Order Logic: Resolution and unification algorithms.
2. Satisfiability (SAT) and SMT: The DPLL algorithm, CDCL, and Theories (Arithmetic,
Arrays, Bit-vectors) + Nelson Oppen Theory Combination
3. Type Theory: Automatic Type Inference + Interactive Theorem Proving
4. Applications: Verification of security protocols, program synthesis.