Compositional logics

Course: Artificial Intelligence

Structural unit: Faculty of Computer Science and Cybernetics

Title
Compositional logics
Code
ОК.09
Module type
Обов’язкова дисципліна для ОП
Educational cycle
Second
Year of study when the component is delivered
2023/2024
Semester/trimester when the component is delivered
2 Semester
Number of ECTS credits allocated
4
Learning outcomes
PLO16. To know and be able to apply logical formalisms.
Form of study
Distance form
Prerequisites and co-requisites
To know basic concepts of mathematical logic: languages of propositional logic and first order logic, their possibilities for the description of subject areas; have a modern understanding of the basic methods of theorem proving and means of inference. To be able to describe in formal languages statements regarding certain subject areas; to derive in propositional and first-order calculus of Hilbert type and sequential type.
Course content
Discipline aim. The purpose of the discipline is to broaden knowledge of logic, including the study of proof assistant systems, program-oriented formal logical methods; obtaining knowledge, skills and abilities related to the application of the mathematical logic in programming. The learning course is devoted to the problems of formalisms of mathematical logic application in the theorem provers. It studies the application of mathematical logic in programming under conditions of uncertain and unclear information, basic methods of finding proofs and means of logical inference, means of formalizing subject areas in conditions of uncertain and unclear information, truthness and validity of formulas, construction of inference in logical calculus.
Recommended or required reading and other learning resources/tools
1. Nikitchenko M.S., Shkilnyak S.S. Matematychna lohika ta teoriya alhorytmiv. – Kyiv., 2008. 2. Nikitchenko M.S., Shkilnyak S.S. Prykladna lohika. – Kyiv, 2013. 3. Belnap N., Steel T. The logic of questions and answers. – New Haven and London: Yale Univ. Press, 1976. 4. Handbook of Logic in Computer Science. Edited by S. Abramsky, Dov M. Gabbay and T. S. E. Maibaum. – Oxford Univ. Press. – Vol. 1–5, 1993–2000. 5. Hoare C.A.R., Jifeng He. Unifying Theories of Programming. – London: Prentice Hall Europe, 1998. 6. Schneider K.: Verification of Reactive Systems. Formal Methods and Algorithms. – Berlin-Heidelberg: Springer-Verlag, 2004. 7. Clarke E.M., Grumberg O., Peled D.: Model Checking. MIT Press (1999). 8. Kröger F., Merz S. Temporal logic and state systems. – Berlin-Heidelberg: Springer-Verlag, 2008.
Planned learning activities and teaching methods
Lectures, individual work.
Assessment methods and criteria
Semester assessment: 1. Test 1: LO 1.1, LO 1.2, LO 2.1 – 20 points / 12 points 2. Test 2: LO 1.3, LO 2.1 – 20 points / 12 points 3. Course paper: LO 3.1, LO 4.1 – 15 points / 9 points 4. Current evaluation: LO 3.1, LO 4.1 – 5 points / 3 points Final assessment: - maximum number of points that can be obtained by the student: 40 points; - learning outcomes that are evaluated: LO 1.1 – LO 1.3, LO 2.1 - form of holding: written work.
Language of instruction
Ukrainian, English

Lecturers

This discipline is taught by the following teachers

Andrii V. Kryvolap
Theory and Technology of Programming
Faculty of Computer Science and Cybernetics

Departments

The following departments are involved in teaching the above discipline

Theory and Technology of Programming
Faculty of Computer Science and Cybernetics