Advanced Logic and Applications

Code:

CC4086

Acronym:

CC4086

Level:

400

Keywords
Classification	Keyword
OFICIAL	Computer Science

Instance: 2022/2023 - 2S

Active?	Yes
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	8	Study plan since 2014/2015	1	-	6	42	162

Teaching language

Suitable for English-speaking students

Objectives

The automation of testing systems is a tool with increasing value in the software industry. In this course the theoretical foundations are discussed as well as the tools that help in the automatic deduction processes.

Learning outcomes and competences

Application of advanced topics of logic in solving problems in various areas of computer science. The student is expected to:
- understand the importance of using logic and formal systems in solving concrete problems;
- be able to relate proof theory with programming in different paradigms (with an emphasis on the functional and logical).
- be able to use an automated theorem prover;
- understand the algorithmic interpretation of intuitionistic logic and the principles of extracting programs from proofs.

Working method

Presencial

Program

- Constructive logic and type theory: lambda calculus; simple type systems; intuitionistic logic; Martin-Löf type theory; propositions as types (the Curry-Howard isomorphism); reductions as computation rules; extracting programs from proofs, logic tools, proof assistant systems (examples: Coq, Hol, Isabelle).
- Semantics of possible worlds, Kripke models.
- Equational logic: terms; unification, rewriting.
- Logic of predicates and proofs: the completeness theorem, algorithms for finding proofs (tableaux and resolution).
- Dependent types. Existential quantification. Correspondence with first-order logic. Type driven programming. Functional programming with dependent types (examples: Idris, Agda).
- Decidable and undecidable problems: complete and decidable theories; elimination of quantifiers; Gödel's incompleteness theorem.

Mandatory literature

Jean Goubault-Larrecq; Proof theory and automated deduction. ISBN: 978-0-7923-4593-0
Yves Bertot; Interactive theorem proving and program development. ISBN: 9783540208549 hbk

Complementary Bibliography

Morten Heine Sørensen and Pawel Urzyczyn; Lectures on the Curry-Howard Isomorphism, Elsevier Science, 2006. ISBN: SBN: 978-0444520777
Michael Huth; Logic in Computer Science. ISBN: 0-521-54310-X

Teaching methods and learning activities

Theoretical-practical classes with exposition of subjects and problem solving.

Evaluation Type

Distributed evaluation without final exam

Assessment Components

designation	Weight (%)
Teste	100,00
Total:	100,00

Amount of time allocated to each course unit

designation	Time (hours)
Estudo autónomo	120,00
Frequência das aulas	42,00
Total:	162,00

Eligibility for exams

No frequency criteria.

Calculation formula of final grade

First test (50% of the final mark).
Second test (50% of the final mark).
If FT is the mark obtained in the first test and ST the mark obtained in second test, then the final mark is given by:
F = FT*(0.5) + ST*(0.5)
FT,ST >= 6 and F >= 9.5
To get approval in the distributed evaluation, students must obtain a minimum of 6 points (in a total of 20) in each test and a minimum of 9.5 as final mark.
The students not obtaining approval, can take a resit exam, with a weight of 100% of the final mark.

Additionally there could be lab projects proposed in each module, with the weight of these projects in the final mark to be determined by the teacher.

Special assessment (TE, DA, ...)

Students whose enrollment type does not require class attendance must take the two prescribed tests.

Observations

The resit exam scope comprises the entire syllabus.
This exam can be used to improve the final mark.