A higher level artificial intelligence should be able to express knowledge and reason about it, e.g. draw conclusions from facts or from assumptions. This can be achieved by using some kind of language. Formal (or symbolic) languages have been constructed partly for the sake of turning the “art of making conclusions”, and related problems, into a mathematically precise activity, and partly to facilitate the automation of reasoning. The formal languages of propositional logic and first-order logic are the cornerstones of the formal approaches to knowledge representation and deduction, and the multitude of other formal logical languages that exist are modifications or extensions of these. This course is an introduction to the key notions and results of propositional and first-order logic.
Course type:
- AS track: introductory
- AI track: elective
- Joint curriculum: introductory
Time: Given yearly, Spring
Teachers: Vera Koponen (UU)
Examiner: Marina Axelson-Fisk (CTH)
Introductory course giving the background in logic needed to take the WASP courses “Artificial Intelligence and Machine Learning” and “Graphical Models, Bayesian Learning and Statistical Relational Learning”.
After completing the course, students should be able to
- Formulate statements in a natural language (e.g. English) by a syntactically correct formula in propositional logic or in first-order logic, depending on what is appropriate in the context.
- Determine the truth value of a formula with respect to a truth value assignment if the formula is from propositional logic, or with respect to a structure if the formula is from first-order logic.
- Determine if a formula is satisfiable, valid or a logical consequence of a set of other formulas.
- Determine if two formulas are logically equivalent.
- Construct a (disjunctive, conjunctive or prenex) normal form which is equivalent to a given formula.
- Motivate some standard formal proof rules and construct formal proofs.
- Use the notions of logical consequence and/or formal proof together with the soundness and/or completeness theorems to determine the correctness of a claim that a statement follows from some given assumptions.
- Describe and apply some results from the course about algorithmic aspects about the problem of determining satisfiability, validity, logical consequence etc in propositional and first-order logic.
We study the two formal (logical) languages called propositional logic and first-order logic, which have a central role in modern logic and its applications.
Syntax and semantics of the formal language of propositional logic. Logical consequence and equivalence in propositional logic. Functional completeness. Disjunctive and conjunctive normal forms. Proof rules and formal proofs in propositional logic. Soundness and completeness of propositional logic.
Syntax of the formal language of first-order logic. First-order structures and the semantics of first-order logic. Logical consequence and equivalence in first-order logic. Prenex normal forms. Proof rules and formal proofs of first-order logic. Soundness and completeness of first-order logic. Computational aspects of propositional logic and first-order logic.
Valentin Goranko, Logic as a Tool: A Guide to Formal Logical Reasoning, John Wiley & Sons Ltd, 2016.
Home work assignments.
A re-examination is prepared about 6 months after the course covering completion of missing parts.
Syllabus (Kursplan)
Course page
If you are not a student at KTH you must login via https://canvas.kth.se/login/canvas