Fundations of Logic and Model Theory, 7.5 Credits

Contents

The course is divided into two modules:

• Module 1. Theory 4.5 hp
• Module 2. Proficiency training 3.0 hp

The course covers predicate logic, first order logic, temporal logic, and model theory. Central concepts are syntax, semantics, proof systems, soundness, completeness, satisfiability, unification and resolution.

Knowledge of formal logical systems is necessary to understand the basic principles of many areas of Computer Science, e.g., databases, scientific computing, and machine learning. Module 1 creates this familiarity by teaching logical concepts and methods from a computer-science perspective. Particular emphasis is placed on (i) the difference between logically true statements and and formal proofs, i.e., the definition of logical truth on the one hand, and the development of formal systems for deriving the truth value of  a statement on the other; (ii) algorithmic aspects of proof system, focusing on resolution; and (iii) logical models for logical systems and their usefulness for verification. 

Module 2 provides logical proficiency training through mandatory assignments. The module illustrates theory taught in model 1, e.g., through assignments in logical programming, and gives the student the opportunity to apply definitions, notations, and formal systems in a practical setting.

Expected learning outcomes

After having completed the course, the student is expected to be able to: 
Knowledge and understanding

• Explain the difference and interaction between syntax and semantics (FSR 1)
• Explain basic concepts, definitions and notations in predicate, first order, and temporal logic (FSR 2)
• Exhibit a rudimentary understanding of proof systems in predicate logic (FSR 3)
• Describe the properties of soundness and completeness in the context of proof systems (FSR 4)
• Define and use Horn clauses (FSR 5)
• Have a good understanding of resolution, including the translation of formula to conjunctive normal form, the application of the deduction rule Resolution, apply substitutions and unification, compute the most general unifier, and conduct resolution proofs.  (FSR 6)
• Discuss satisfiability, soundness, and completeness in predicate and first-order logic (FSR 7)
• Define what is meant by a model for the various logical systems presented in the course (FSR 8)

Skills and abilities

• Analyse and compare the descriptive power of the logical systems presented in the course (FSR 9)
• Show a basic understanding for how models can be used in formal verification (FSR 10)
• Use basic concepts, definitions and notations in predicate, first order, and temporal logic (FSR 11)
• Use deduction rules and axiom schemas (FSR 12)

Required Knowledge

To be admitted you must have at least 7.5 credits in discrete mathematics (e.g Introduction to Discrete Mathematics, 5MA143) and at least 7.5 credits in programming methodology (e.g 5DV157, 5DV158, 5DV176 eller 5DV177) or equivalent.

Form of instruction

The course consists of lectures, quizzes, programming assignments, and exercises in small groups. In addition to scheduled activities the course also requires individual work with the material.

Examination modes

Examination of the theoretical module (FSR 1-12) is done through a written examination. The grade on this module is one of the grades Fail (U), Pass (3) or Pass with Merit (4), or Pass with Distinction (5).

The examination of the practical module (FSR 1-12) is done through completing a series of assignments individually according to instructions provided during the course. The number of assignments vary accoring to their level of difficulty but is never more than 5. The grade on the practical module is one of the grades Fail (U) or Pass (G).

On the whole course, one of the grades Fail (U), Pass (3) or Pass with Merit (4), or Pass with Distinction (5) is given. At least the grade Pass must be achieved on each part in order to get a grade for the whole course. The grade given on the course is the same as the one set on module 1.

For all students who do not pass the regular examination there is another opportunity to do the examination.
 
A student who has passed an examination may not be re-examined. A student who has taken two tests for a course or segment of a course, without passing, has the right to have another examiner appointed, unless there exist special reasons (Higher Education Ordinance Chapter 6, section 22). Requests for new examiners are made to the head of the Department of Computing Science.

Examination based on this syllabus is guaranteed for two years after the first registration on the course. This applies even if the course is closed down and this syllabus ceased to be valid.

Deviations from the examination forms mentioned in this syllabus can be made for a student who has a decision on pedagogical support due to disability. Individual adaptation of the examination forms should be considered based on the student's needs. The examination form is adapted within the framework of the expected learning outcomes of the course syllabus. At the request of the student, the course responsible teacher, in consultation with the examiner, must promptly decide on the adapted examination form. The decision must then be communicated to the student.

Transfer of credits

Students have the right to be tried on prior education or equivalent knowledge and skills acquired in the profession can be credited for the same education at Umeå University. Application for credit is submitted to the Student Services / Degree. For more information on credit transfer available at Umeå University's student web, www.student.umu.se, and the Higher Education Ordinance (Chapter 6). A refusal of crediting can be appealed (Higher Education chapter 12) to the University Appeals Board. This applies to the whole as part of the application for credit transfer is rejected.