Computational Logic

Code:

CC2003

Acronym:

CC2003

Level:

200

Keywords
Classification	Keyword
OFICIAL	Computer Science

Instance: 2016/2017 - 1S

Active?	Yes
Web Page:	http://www.dcc.fc.up.pt/~nam/web/Teaching/lc16/index.html
Responsible unit:	Department of Computer Science
Course/CS Responsible:	Bachelor in Computer Science

Cycles of Study/Courses

Acronym	No. of Students	Study Plan	Curricular Years	Credits UCN	Credits ECTS	Contact hours	Total Time
L:B	0	Official Study Plan	3	-	6	56	162
L:CC	63	Plano de estudos a partir de 2014	2	-	6	56	162
L:M	0	Official Study Plan	2	-	6	56	162
			3
L:Q	4	study plan from 2016/17	3	-	6	56	162
MI:ERS	105	Plano Oficial desde ano letivo 2014	2	-	6	56	162

Teaching language

Portuguese

Objectives

 To know the main topics of propositional logic and first order logic, with a special focus on automated therem proving.

Learning outcomes and competences

To know the main topics of propositional logic and first order logic, with a special focus on automated therem proving.

Working method

Presencial

Pre-requirements (prior knowledge) and co-requirements (common knowledge)

Discrete Structures

Program

 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.

Mandatory literature

Huth Michael 1962-; Logic in Computer Science. ISBN: 0-521-54310-X

Complementary Bibliography

Barwise Jon; Language, proof, and logic. ISBN: 1-57586-374-X
C.J. Hogger; Essentials of logic programming. ISBN: 0-19-853832-4
Almeida José Bacelar 070; Rigorous software development. ISBN: 9780857290175

Teaching methods and learning activities

 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.

Evaluation Type

Distributed evaluation with final exam

Assessment Components

designation	Weight (%)
Exame	75,00
Trabalho escrito	25,00
Total:	100,00

Amount of time allocated to each course unit

designation	Time (hours)
Estudo autónomo	84,00
Frequência das aulas	56,00
Total:	140,00

Calculation formula of final grade

 The final grade : Trab: practical

Trab∗4+Exam∗16)≥9.5,Trab∗4≥1,Exam∗16≥6