Fundamentals of Knowledge Representation
- The aim of this advanced course is to introduce the students to the most successful logic based concepts, tools and techniques used today in CS and IT, which are behind a major breakthrough in the theoretical and practical applications in knowledge representation systems.
- Learning syntax and semantics of predicate logic with ensuring its orientation to the actual needs of computer science and information technology.
- Understanding how predicate logic detects difference between finite and infinite.
- Understanding why predicate logic cannot detect difference between enumerable and nonenumerable.
- Prove or disprove predicate formulas by means of the unfolded tree analysis.
- Prove soundness and completeness for some finite systems of inference rules.
- Simulate computations within predicate logic.
- Being familiar with decidable procedures for propositional logic.
- Being familiar with decidable procedures for pure monadic predicate logic.
- Specify programs formally using Hoare triples.
- Run symbolic execution rules for loop-free programs manually.
- Use symbolic execution rules to prove loop-free programs semi-automatically.
- Understanding the definition of loop invariants.
- Write loop invariants for simple arithmetic programs.
- Prove simple arithmetic programs using loop invariants.
- Understanding symbolic execution for loops.
- Understanding an algorithm for inferring loop invariants automatically.
- Apply the algorithm for simple arithmetic programs.
- Understanding SAT solvers.
- Understanding the DPLL algorithm.
- Apply Conflict-Driven Clause Learning as an efficient tool for SAT solving in practice.
- Formal systems. Syntax and semantics
- Predicate logic as a specification language for AI and CSDiscuss several subtle examples of encoding problems into predicate logic. Discuss the importance of distinguishing syntax and semantics. Formally describe the syntax of predicate logic. Formally define the domain of interpretation of predicate logic (universe and interpretation of symbols). Informally describe the semantics of predicate logic formulas, including connectives and quantifiers.
- Models. Semantics of predicate logic. Finite and infinite modelsRecap on the formal syntax of predicate logic. Bound and free variables. Formal semantics of predicate logic.Validity, satisifiability, etc. Brief introduction to reasoning about predicate logic formulas.
- Automatized provers for predicate logic: Soundness and completenessThe unfolded tree analysis in predicate logic. A finite system of inference rules. Soundness and completeness. Bound and free variables.
- Predicate logic: Undecidability. Decidable fragmentsSimulation Turing/Minsky machines within predicate logic. Decidable procedures for propositional logic. Decidable procedures for pure monadic predicate logic.
- Hoare triples as a language to specify the dynamic behaviour of programs/plans in AI and CS.Introduction to Hoare logic as the foundation of many successful techniques for formal verification of software. Provide intuition about program correctness through examples of program specifications in Hoare logic. Formally define the syntax and semantics of Hoare triples. Distinguish between the notion of partial and total correctness. The importance of auxiliary variables. Use Hoare Triples.
- Hoare logic. Inference rules. Soundness and Completeness. Automatized Inference of Loop Invariants.Formally define inference rules of Hoare logic for reasoning about partial program correctness. Explain the connection between forwards and backwards axiom for assignment and weakest preconditions for assignment. Explain how reasoning about predicate logic formulas is used for verifying programs using Hoare Logic. Apply the Hoare Logic inference rules to prove (or disprove) correctness of loop free programs. Use loop invariants to prove correctness of programs with loops. Discuss the difference between inference rules for partial and total correctness. Discuss extensions of Hoare Logic to support other programming language features, such as pointers. Classic (single-path) symbolic execution. Recap: Syntax and semantics of while programs. Proving Hoare triples of programs using forward symbolic execution. Understand an algorithm for generating loop invariants automatically.
- SAT Solvers. Symbolic model checking. Horn clauses and functional dependencies in relational databases. The DPLL algorithm and its improvementsWhat is SAT. Polynomial-time algorithms in the case of Horn clauses and functional dependencies in relational databases. Normal forms for general case. Tseitin transformation. Understand the DPLL algorithm: unit propagation, pure literal elimination. Conflict-Driven Clause Learning as an efficient tool for solving the Boolean satisfiability problem in practice.
- Van Harmelen, F., Lifschitz, V., Porter, B. (ed.). Handbook of knowledge representation. – Elsevier, 2008. – Vol. 1. – 1034 pp.
- Boolos, G. S., Burgess, J. P., Jeffrey, R. C. Computability and logic. – Cambridge university press, 2002. – 364 pp.
- Nipkow, T., Grumberg, O., Hauptmann, B. (ed.). Software Safety and Security: Tools for Analysis and Verification. – IOS Press, 2012. – 400 pp.