VVZ API is not affiliated with ETH Zurich. Data might be outdated or incorrect. Please view the official ETHZ Vorlesungsverzeichnis for binding information.
Decision Procedures for Logical Theories
Last Updated: 2026-02-05 14:59:54
Abstract
This course dicusses some of the main decidable logics and theories, and derives and analyzes the corresponding decision procedures, both theoretically (complexity analysis) and from an implementation point of view. Included topics are propositional satisfiability, combination methods, quantifier elimination, and model-checking.
Objective
Overview of decidable logics and theories and implementation techniques for building effective decision procedures for such logics.
Content
Decision procedures decide validity or satisfiability of logical formulas of a particular logic or of a particular theory within some logic. Recent successes in verifying substantial parts of hardware and software components have been made possible via implementations of such decision procedures in verification systems such as PVS or HOL. In this course we shall treat some of the main decidable logics and theories and derive and analyze the corresponding decision procedures both theoretically (complexity analysis) and from an implementation point of view. Topics include propositional satisfiability, ground decision procedures for equality and inequality, combination methods, quantifier elimination, and rewriting. The emphasis is on simple and unified theoretical foundations, efficient implementation, and applications.
Resources
Literature
Literature will be announced during the lecture.
General Information
- Language
- English
- Frequency
- Yearly recurring
Examination
- Type
- session examination
- Mode
- oral 15 minutes
Course Components
| Type | Title | Time & Place | Hours |
|---|---|---|---|
| lecture | Decision Procedures for Logical Theories |
|
2 h weekly |
| exercise | Decision Procedures for Logical Theories |
|
1 h weekly |