Logic and automated deduction

Course: Artificial Intelligence

Structural unit: Faculty of Computer Science and Cybernetics

Title
Logic and automated deduction
Code
ННД.18
Module type
Обов’язкова дисципліна для ОП
Educational cycle
Second
Year of study when the component is delivered
2022/2023
Semester/trimester when the component is delivered
3 Semester
Number of ECTS credits allocated
5
Learning outcomes
PLO16. To know and be able to apply logical formalisms.
Form of study
Distance form
Prerequisites and co-requisites
To know: basic methods of mathematical logic, methods of theorem proving in predicate logic, methods of formalization of program systems and systems of Artificial Intelligence. To be able to: prove theorems in predicate logic, develop program systems and systems of Artificial Intelligence based on their formal models and prove properties of such systems.
Course content
Discipline aim. The aim of the discipline is to provide up-to-date knowledge of mathematic logic, methods of automated deduction and their application for solving problems of Artificial Intelligence, to develop ability to formulate scientific problem and working hypotheses on the basis of understanding of existing and creation of new holistic knowledge, as well as professional practice, to develop and implement new competitive ideas in the field of information technology. Synopsis of the course: The discipline "Logic and Automated Thinking" is a part of the educational-scientific program of training specialists at the educational-qualification level "Master" in the field of knowledge 12 "Information Technologies" in the specialty 122 "Computer Science", educational-scientific program "Artificial intelligence". This discipline is mandatory in the specialty 122 "Computer Science", educational-scientific program "Artificial Intelligence". It is taught in the 3rd semester of the 2nd year of master's studies in the amount of 150 hours. (5 ECTS credits) in particular: lectures - 42 hours, consultations - 2 hours, independent work - 106 hours. The course includes 3 parts and 3 tests. The discipline ends with an exam in the 3rd semester.
Recommended or required reading and other learning resources/tools
1. Nikitchenko M.S., Shkilniak S.S. Prykladna logika. – К., 2013. 2. Nikitchenko M.S. Teoria Programuvannia.– К., 2020. 3. Schneider K.: Verification of Reactive Systems. Formal Methods and Algorithms. – Berlin-Heidelberg: Springer-Verlag, 2004. 4. Nielson H.R. Semantics with Applications: A Formal Introduction / H.R. Nielson, F. Nielson // John Wiley & Sons Inc. P. 240., 1992 5. Dijkstra E.W. A Discipline of Programming / E.W. Dijkstra // Prentice-Hall, Englewwod Cliffs, New Jersey, 1976.
Planned learning activities and teaching methods
Lectures, independent work.
Assessment methods and criteria
Semester assessment: 1. Test 1: LO 1.1, LO 2.1, LO3.1 - 20 points / 12 points. 2. Test work 2: LO1.2, LO2.2, LO3.1 - 10 points / 06 points. 3. Test work 3: LO1.2, LO2.2, LO3.1 - 20 points / 12 points. 4. Current evaluation: LO3.1, LO4.1, LO4.2 - 10 points / 06 points. Final assessment: exam. - the maximum number of points that can be obtained: 40 points; - learning outcomes that will be evaluated: LO1.1, LO1.2, LO1.3, LO1.4; - form and types of tasks: written work. The recommended minimum is 24 points.
Language of instruction
Ukrainian, English

Lecturers

This discipline is taught by the following teachers

Mykola S. Nikitchenko
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