* König lemma * syntax and semantics of propositional logic, * logical connectives, * truth tables, * adequate set of truth connectives, axioms and inference rules, normal forms in propositional logic, clausal form, terms, atoms and formulas, Herbrand theorem, * prenex form, * Skolemization, interpretation.

* Resolution in propositional logic, refinements of the resolution, resolution in predicate logic, substitution, unification, * linear resolution, * LI-resolution, * Horn clauses, * LD-resolution, * SLD-resolution, * soundness and completeness.

Logic program, * SLD-trees, Prolog - syntax and semantics, * incompleteness, simple Prolog programs, meta-interpreters.

Signed formula, atomic tableau, tableau proofs in propositional logic, \alpha-, \beta-rules, tableau proofs in predicate logic, \gamma-, \delta- rules, finite tableau, reduced entry, contradictory path, finished tableau, tableau proof, tableau refutation, complete systematic tableau, soundness and completeness.

basic task, example setting, generic algorithm, generalization and specialization, specialization operators, general-to-specific ILP, bias, Aleph system, assumption-based reasoning, assumption, assumption-based learning, WiM system.

refinement operator, global and local completeness, ideal refinement operator, non-existence for reduced Horn clauses.

data mining task, frequent Datalog query, maximal frequent patterns, RAP algorithm

extensional and intensional representation, Datalog, evaluation of Datalog queries

Modal logic, modal tableau, non-monotonic inference,