Code

COMP2008

Year

2

Prerequisites

Theory I (1002) and Theory II (1004)

Term

1

Taught By

Juan Navarro Perez (67%)
John Dowell (33%)

Aims

To introduce and familiarise students with logical and mathematical inference and with database theory, the latter having an emphasis on the fundamentals of relational database systems and SQL. Students learn a number of logical inference methods for classical logics.

Learning Outcomes

Students should understand how axiomatic systems can be used for propositional and predicate logic and they should understand the notions of soundness and completeness. They should also understand how propositional and predicate tableaus work. They should have familiarity with other logics, including modal and temporal logics. They should be able to analyse relational databases.

Predicate logic

Syntax - variables and quantifiers. Free and bound variables, and scope of a variable.
Semantics, Validity and satisfiability in a model. Validity and satisfiability in general.
Proof theory - tableau systems and Hilbert systems.
Translating from natural language to predicate logic and vice versa.
Main theorems: soundness and completeness of tableau method, Herbrand models; Godel's incompleteness theorem

Mathematical proofs

Proof by contradiction

Induction and structured induction

Weak and strong induction

Hilbert systems

Axioms and inference rules for propositional logic.

Axioms and inference rules for predicate logic.

Tableau.

Tableau construction for propositional logic and predicate logic.

Soundness and completeness theorems for first order logic.

Tableau for modal logics.

Finite computation methods

Finite state machines
Regular languages
Kleene's theorem
Finite state machines with stacks

Applications of predicate logic

Case studies of using predicate logic in information technology, including relational databases, software engineering, and artificial intelligence

Databases

What is a database and a database system?
Data Models
The Entity-Relationship Model
The Relational Model and SQL
New Technologies

Lecture presentations with associated courseworks.

The course has the following assessment components:

• Written Examination (2.5 hours, 95%)
• Coursework Section (2 pieces, 5%)

To pass this course, students must:

• Obtain an overall pass mark of 40% for all sections combined

The examination rubric is:
Answer all three questions

J. Truss, Discrete mathematics for computer scientists,

Addison-Wesley, 2nd edition, 1999.

W. Hodges, Logic: an introduction to elementary logic,

Penguin, 1977.

Web resources