Code: | CC2003 | Acronym: | CC2003 | Level: | 200 |
Keywords | |
---|---|
Classification | Keyword |
OFICIAL | Computer Science |
Active? | Yes |
Responsible unit: | Department of Computer Science |
Course/CS Responsible: | Bachelor in Computer Science |
Acronym | No. of Students | Study Plan | Curricular Years | Credits UCN | Credits ECTS | Contact hours | Total Time |
---|---|---|---|---|---|---|---|
L:B | 1 | Official Study Plan | 3 | - | 6 | 56 | 162 |
L:CC | 87 | Plano de estudos a partir de 2014 | 2 | - | 6 | 56 | 162 |
L:F | 0 | Official Study Plan | 2 | - | 6 | 56 | 162 |
3 | |||||||
L:G | 0 | study plan from 2017/18 | 2 | - | 6 | 56 | 162 |
3 | |||||||
L:M | 9 | Official Study Plan | 2 | - | 6 | 56 | 162 |
3 | |||||||
L:Q | 0 | study plan from 2016/17 | 3 | - | 6 | 56 | 162 |
MI:ERS | 89 | Plano Oficial desde ano letivo 2014 | 2 | - | 6 | 56 | 162 |
To know the main topics of propositional logic and first order logic, with a special focus on automated therem proving.
To know the main topics of propositional logic and first order logic, with a special focus on automated therem proving.
Discrete Structures
Proposicional logic: syntax and semantics; satisfazibility, validity. normal forms; SAT solvers; deduction systems; soundness and completeness of deduction systems; decidability. Fist-order logic: syntax and semantics;models; validity; normal forms; deduction systems; soundness and completeness; decidable fragments; first-order theories.
Automated theorem proving: Horn clauses; unification; resolution.
The teaching methods are based on expository lecturing and exercises complemented with programming coursework that enables the student practice the methods studied in the course.
designation | Weight (%) |
---|---|
Teste | 100,00 |
Total: | 100,00 |
designation | Time (hours) |
---|---|
Estudo autónomo | 110,00 |
Frequência das aulas | 52,00 |
Total: | 162,00 |
The final grade (FT - firts test, ST - second test)
F = FT*(0.5) + ST*(0.5)
FT,ST >= 6 e F >= 9.5