Advanced Topics in Logic
Keywords |
Classification |
Keyword |
OFICIAL |
Computer Science |
Instance: 2017/2018 - 2S
Cycles of Study/Courses
Teaching language
Suitable for English-speaking students
Objectives
Application of advanced topics of logic to the resolution of problems in diferent areas of computer science.
Learning outcomes and competences
Students are expected to:
- understand the importance of the application of logic and formal systems in problem solving;
- be able to model real world problems in diferent systems of logic and solve them using SAT and SMT solvers;
- be able to relate proof theory with programming languages, with a special focus on functional and logic programming.
Working method
Presencial
Pre-requirements (prior knowledge) and co-requirements (common knowledge)
Basic knowledge of logic, similar to standard courses in a bachelour degree.
Program
- Intuitionistic Logic: propositional logic; natural deduction; connections between classical and intuitionistic logic; type theory; proof terms; proofs as programs (Curry-Howard isomorphism); reductions as rules of computation; functional programming; first-order intuitionistic logic; natural numbers; inductive definitions.
- SAT solvers: propositional logic; decision problems SAT and VAL; normal forms; equisatisfiability; Tseitin's encoding; SAT solving algorithms (basic concepts); DPLL framework and its optimisations; modeling concrete problems in propositional logic and solving using a SAT solver.
- SMT solver: classical first order logic (FOL); decision problems SAT and VAL; normal forms (Herbrandization and Skolemization); FOL with equality; many-sorted FOL. First order theories: basic concepts and decidability issues; several theories (equality, integers, linear arithmetic, reals, arrays); combining theories; satisfiability modulo theories; SMT solvers; SMT-LIB; applications.
Mandatory literature
Kroening Daniel;
Decision procedures. ISBN: 9783540741046
Goubault-Larrecq Jean;
Proof theory and automated deduction. ISBN: 978-0-7923-4593-0
Complementary Bibliography
Morten Heine Sørensen and Pawel Urzyczyn; Lectures on the Curry-Howard Isomorphism, Elsevier Science, 2006. ISBN: 978-0444520777
Huth Michael 1962-;
Logic in Computer Science. ISBN: 0-521-54310-X
Teaching methods and learning activities
Lectures and case studies.
Evaluation Type
Distributed evaluation with final exam
Assessment Components
designation |
Weight (%) |
Exame |
50,00 |
Teste |
50,00 |
Total: |
100,00 |
Amount of time allocated to each course unit
designation |
Time (hours) |
Estudo autónomo |
50,00 |
Frequência das aulas |
50,00 |
Total: |
100,00 |
Calculation formula of final grade
The final grade is the arithmetic mean of the classifications obtained in a first test, to be in the middle of the semester, and in a second test, in the normal examination period.