Logic and Programming

Code:

CC216

Acronym:

CC216

Keywords
Classification	Keyword
OFICIAL	Computer Science

Instance: 2012/2013 - 2S

Active?	Yes
Responsible unit:	Department of Computer Science
Course/CS Responsible:	Bachelor in Geology

Cycles of Study/Courses

Acronym	No. of Students	Study Plan	Curricular Years	Credits UCN	Credits ECTS	Contact hours	Total Time
L:AST	0	Plano de Estudos a partir de 2008	3	-	7,5	-
L:B	0	Plano de estudos a partir de 2008	3	-	7,5	-
L:CC	53	Plano de estudos de 2008 até 2013/14	2	-	7,5	-
L:F	1	Plano de estudos a partir de 2008	3	-	7,5	-
L:G	0	P.E - estudantes com 1ª matricula anterior a 09/10	3	-	7,5	-
		P.E - estudantes com 1ª matricula em 09/10	3	-	7,5	-
L:M	3	Plano de estudos a partir de 2009	3	-	7,5	-
L:Q	0	Plano de estudos Oficial	3	-	7,5	-
MI:ERS	99	Plano de Estudos a partir de 2007	2	-	7,5	-

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

Melvin Fitting; First Order Logic and Automated Theorem Proving
C.J. Hogger; Essentials of logic programming. ISBN: 0-19-853832-4

Complementary Bibliography

Barwise Jon; Language, proof, and logic. ISBN: 1-57586-374-X

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 without final exam

Assessment Components

Description	Type	Time (hours)	Weight (%)	End date
Attendance (estimated)	Participação presencial	85,00
Test	Teste	1,50	50,00	2013-04-11
Test	Teste	1,50	50,00	2013-06-14
	Total:	-	100,00

Amount of time allocated to each course unit

Description	Type	Time (hours)	End date
Study	Estudo autónomo	85	2013-06-14
	Total:	85,00

Calculation formula of final grade

 The final grade is the average of the test grades.