Infopaket

Logic and automated deduction

Обов’язкова дисципліна для ОП

Second

2021/2022

3 Semester

5

Full-time form

1. 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. 2. 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.

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. As a result of studying the discipline the student must: to know the basic concepts and methods of mathematical logic, the hierarchy of logics, logical calculus, methods and tools of proving theorems, methods of describing subject areas, software systems and systems of Artificial Intelligence; to be able to formalize the properties of subject areas, software systems, and systems of Artificial Intelligence using the apparatus of logic, to use the apparatus of logic to solve problems of artificial intelligence.

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.

Lectures, independent work, Test, current evaluation, exam.

1. Test 1: LO 1.1, LO 2.1, LO3.1 - 20 балів/12 балів. 2. Test 2: LO1.2, LO2.2, LO3.1 - 20 балів/12 балів. 2. Test 3: LO1.2, LO2.2, LO3.1 - 15 балів/9 балів. 3. Current evaluation: LO3.1, LO4.1, LO4.2 - 5 points / 3 points. An applicant may not be admitted to the final assessment if during the semester he: 1) has not reached the minimum threshold level (60%) of the assessment of those learning outcomes that cannot be assessed during the final control; 2) scored the number of points, which is insufficient to obtain a positive assessment, even if he achieves the maximum possible result in the final control. The recommended minimum is 36 points.

Ukrainian