Advanced Topics in Logic

Code:

CC4026

Acronym:

CC4026

Level:

400

Keywords
Classification	Keyword
OFICIAL	Computer Science

Instance: 2017/2018 - 2S

Active?	Yes
Web Page:	http://www.dcc.fc.up.pt/~sandra/Home/TAL1718.html
Responsible unit:	Department of Computer Science
Course/CS Responsible:	Master in Computer Science

Cycles of Study/Courses

Acronym	No. of Students	Study Plan	Curricular Years	Credits UCN	Credits ECTS	Contact hours	Total Time
M:CC	4	Study plan since 2014/2015	1	-	6	42	162
MI:ERS	6	Plano Oficial desde ano letivo 2014	4	-	6	42	162

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.