Artificial intelligence in theorem proving

General data

Course ID:	1000-2M19SID
Erasmus code / ISCED:	11.3 Kod klasyfikacyjny przedmiotu składa się z trzech do pięciu cyfr, przy czym trzy pierwsze oznaczają klasyfikację dziedziny wg. Listy kodów dziedzin obowiązującej w programie Socrates/Erasmus, czwarta (dotąd na ogół 0) – ewentualne uszczegółowienie informacji o dyscyplinie, piąta – stopień zaawansowania przedmiotu ustalony na podstawie roku studiów, dla którego przedmiot jest przeznaczony. / (0612) Database and network design and administration The ISCED (International Standard Classification of Education) code has been designed by UNESCO.
Course title:	Artificial intelligence in theorem proving
Name in Polish:	Sztuczna inteligencja w dowodzeniu twierdzeń
Organizational unit:	Faculty of Mathematics, Informatics, and Mechanics
Course groups:	(in Polish) Przedmioty obieralne na studiach drugiego stopnia na kierunku bioinformatyka Elective courses for Computer Science
ECTS credit allocation (and other scores):	(not available) Basic information on ECTS credits allocation principles: the annual hourly workload of the student’s work required to achieve the expected learning outcomes for a given stage is 1500-1800h, corresponding to 60 ECTS; the student’s weekly hourly workload is 45 h; 1 ECTS point corresponds to 25-30 hours of student work needed to achieve the assumed learning outcomes; weekly student workload necessary to achieve the assumed learning outcomes allows to obtain 1.5 ECTS; work required to pass the course, which has been assigned 3 ECTS, constitutes 10% of the semester student load. view allocation of credits
Language:	English
Type of course:	elective monographs
Short description:	Automated reasoning systems are becoming an important tool for mathematicians and computer scientists. Machine learning is becoming a more and more used method to strengthen reasoning systems. The goal of this course is to learn the artificial intelligence methods used in theorem proving.
Full description:	1. Artificial intelligence problems in interactive theorem provers 2. Selection of relevant premises using classical machine learning methods 3. Deep neural networks in theorem proving 4. Calculi used in automated reasoning and their practical properties 5. Proof state evaluation in various calculi 6. Internal proof guidance 7. Reinforcement learning in theorem proving 8. Proof features based on semantic properties and logical models 9. Generative methods in theorem proving
Bibliography:	A. Alemi et al. DeepMath - Deep Sequence Models for Premise Selection J. Harrison: Handbook of Practical Logic and Automated Reasoning D. Selsam et al.: NeuroSAT - Learning a SAT Solver from Single-Bit Supervision K. Krstovski, D. Blei: Equation Embeddings
Learning outcomes:	Knowledge: 1. Artificial intelligence problems in theorem proving 2. Classical machine learning methods in automated reasoning 3. Knowledge of the basic automated theorem proving calculi 4. Characterization of interactive and automated proofs Skills: The student is able to propose and apply appropriate artificial intelligence methods to a theorem proving problem. Competences: The student understands the need to adapt existing artificial intelligence methods to the specifics of theorem proving and is able to perform such adaptations.
Assessment methods and assessment criteria:	Egzamin pisemny

This course is not currently offered.

Course descriptions are protected by copyright.
Copyright by University of Warsaw.