Course on Application of Logic in Intelligent Systems

-> Home page -> Teaching activities flag

Basic information on the course:

Academic year 2024/2025

Basic study literature for the course, complementing lectures:
Propositional logic
Propositional logic extensions
Predicate logic
Horn logic

Additional material to the course

Lecture presentations (in Slovak)

go Introduction (symbolic AI, ancient logic and reasoning)
go Propositional logic basics (syntax, semantics, equivalence, entailment, grounding)
go Representation of sentences in propositional logic
go Sentences in Conjunctive Normal Form (transformations, simplification)
go Inference in propositional logic (basic inference types)
go Resolution principle for propositional logic
go Conflict-driven clause learning (CDCL) model search for propositional logic
go Problem modelling in propositional logic
go Introduction into SMT (Satisfiability Modulo Theories)
go Late checking for SMT satisfiability and model search
go Early checking for SMT satisfiability and model search
go Predicate logic basics (the 0-th and 1-st order predicate calculus - syntax and interpretation)
go Resolution principle for predicate logic
go Horn logic (forward and backward chaining of rules)
go Production systems (Three little pigs simulation, 99 bottles song)
go Prolog programming language (Island of liars and honest people, 99 bottles song)

Internet materials/demos

Code experiments

Software online tools
Software download
Code snippets

Students' projects (2018)

Sudoku

Final exam topics

  • Symbolic AI and logic reasoning
    1. Rational agent
    2. Symbolic artificial intelligence
    3. Sylogisms (ancient India and Greece)
  • Propositional logic
    1. Foundations of propositional logic
      • Syntax (symbols, operators)
      • Logical values and interpretation (rules, truth tables)
      • Operator characteristics (precedence, commutativity, associativity, idempotence, truth/falsity preservation)
      • Possible worlds (un/satisfiability, validity)
      • Equivalence of logical sentences (transformation rules, minimal operator set)
    2. Grounding of logical sentences (granularity, natural sentence encoding)
    3. Logical sentence representations
      • Basic representations
      • Focus on visualisation
      • Focus on syntactic simplicity
    4. Creation of CNF
      • Naive transformation to CNF
      • Tseitin transformation
      • Plaisted-Greenbaum encoding
      • Transformation to kCNF
    5. Logical entailment and resolution
    6. Simplification of CNF
      • Symbol elimination (from sentence, from clause)
      • Clause elimination
      • Blocked clause elimination
  • Inference in propositional logic
    1. Inference main tasks (deduction, validity, satisfiability)
    2. Characteristics of inference procedures
    3. Inference vs representation (BDD, DNF, CNF - in/direct approach)
      • Inference using truth tables
      • Enumeration of possible worlds algorithm
    4. Resolution based inference
      • Resolution and contradiction detection
      • Resolution algorithm structure
      • Special cases treatment (pure literal, tautology, multipresence, clause subsumption)
      • Derivation graph
      • Useless resolvencies and clause selection strategies
    5. Tablo calculus
      • Tablo algorithm
      • Decomposition rules
      • Rule selections
      • Tablo calculus vs DNF/CNF
    6. Search methods
      • DPLL algorithm
      • Propagations (unit propagation, pure literal propagation)
      • Implication and conflict graphs
      • Conflict analysis (cuts)
        • Conflict clause selection
        • Conflict-driven backjumping
      • Selection heuristics (DLIS, DLCS, MOM, VSIDS)
  • Modelling in propositional logic
    1. Satisfiability based procedure
    2. Modelling algorithm
    3. Binary variables (design and encoding)
    4. Constraints design (minimal set)
    5. Cardinality constraints
      • Constraint types and replacements
      • Binomial encoding
      • Binary encoding
      • Sequence counnter encoding
    6. Symmetry and its breaking
    7. Domain variables encoding
      • Direct encoding
      • Logarithmic encoding
      • Sequential encoding
      • Hierarchical encoding
      • Constraint encoding
    8. Pseudo Boolean constraint encoding
  • Satisfiability modulo theories
    1. Atoms as symbols with inner structure
    2. Syntax of sentences with modulo theories
    3. Satisfiability and T-satisfiability
    4. Selected modulo theories
      • Difference logic
      • Linear arithmetics
    5. Search for model
      • Early checking
      • Late checking
    6. T-satisfiability
      • Fourier-Motzikin variable elimination
        • Constraint types
        • FM Algorithm
        • Algorithm complexity
      • One phase simplex method
        • Basic principle
        • Constraints transformation
        • Usage of simplex method
    7. Direct encoding
      • Direct encoding algoorithm for difference logic
      • Determining values of variables
      • Direct encoding for linear arithmetics
      • Reduction of number of generated constraints
  • Predicate logic
    1. Zero order predicate calculus
      • Syntax
      • Predicates, constants and functions
      • Interpretation
        • Interpretation of constants
        • Interpretation of function/predicate symbols
        • Interpretation of logical sentences
        • Possible worlds and models
    2. First order predicate calculus
      • Syntax with variables
      • Quantifiers
        • Universal and existential quantifiers and their duality
        • Negation of quantifiers
        • Characteristics of quantifiers (commutativity, distributivity)
      • Bounded and free variables
      • Interpretation of variables
      • Transformation of sentences into CNF
      • Inference in predicate logic
        • Refutation proof using resolution
          • Unification of terms (unifiers, term substitution)
          • Unification algorithm
          • Generalised resolution
            • Variable colisions
            • Derivation graph
          • Paramodulation
          • Answering questions
        • Tablo calculus
          • Rules for quantifier elimination
          • Infinite branch developing
  • Horn predicate logic
    1. Horn clauses (rules, facts, goals)
    2. Forward chaining of rules
      • Forward chaining of rules vs resolution
      • Hyperresolution
      • Forward chaining algorithm
    3. Backward chaining of rules
      • Backward chaining of rules vs resolution
      • Input resolution strategy
      • Backward chaining algorithm
    4. Clips programming language
      • ordering hyperresolutions (rule priority)
      • ordering unifiers
      • production system activity algorithm
        • activation of rules
        • rule firing
        • Rete network for pattern matching
    5. Prolog programming language
      • A bit of history, Prolog and KKUI
      • Interaction with Prolog
      • Syntax (constants, variables, structures)
      • Database (facts, rules)
      • Unification of terms
      • Computation as database search
      • Block model

Additional reading
aima Artificial Intelligence: A Modern Approach - the fourth edition of a now classic AI textbook (used in more than 1000 universities)
dp Decision Procedures: An Algorithmic Point of View - decision procedures for selected SMT

Copyright © MM
Last updated 11.12.2025