Course: Automated theorem proving

« Back
Course title Automated theorem proving
Course code KMA/XDV
Organizational form of instruction no contact
Level of course Doctoral
Year of study not specified
Semester Winter and summer
Number of ECTS credits 30
Language of instruction Czech
Status of course Compulsory-optional
Form of instruction Face-to-face
Work placements This is not an internship
Recommended optional programme components None
Lecturer(s)
  • Pech Pavel, prof. RNDr. CSc.
Course content
Working with DGS, verification in DGS, classical proof, examples. Basic notions of the theory of automated theorem proving, proving, deriving, discovering new statements. Conditions of degeneracy and their searching, examples.

Learning activities and teaching methods
Monologic (reading, lecture, briefing), Dialogic (discussion, interview, brainstorming), Monitoring
Learning outcomes
The subject deals with the automated theorem proving. This theory is based on the elimination of variables from a system of algebraic equations using the Gröbner basis of an ideal. Using this method various theorems will be proved in the seminar (for example Simson-Wallace theorem, Heron's formula, Brahmagupta's theorem for cyclic quadrilateral, Ceva's and Menelaus' theorem, theorem about transversals of polygons etc.). Mathematical statements are deduced and proved using the computer. This method is compared with the classical method of proving. All illustrated with a range of examples. Language of the course is Czech or English.
A graduate will acquire competencies to execute automated proving of selected theorems.
Prerequisites
It is necessary to understand basic notions of given theory, knowledge of definitions, theorems and basic proofs. The ability to solve typical problems of the theory. The written part of the exam is oriented on verification, whether a student is able so solve individual tasks, which come out of the given theory. The target of the oral exam is a verification of students understanding of the theory and his/her ability to apply it.

Assessment methods and criteria
Oral examination, Written examination

Seminar work
Recommended literature
  • COX, D., LITTLE, J., O´SHEA, D. Ideals, Varieties and Algorithms. Springer Verlag, 1979..
  • PECH, P. Klasické versus počítačové metody při řešení úloh z geometrie. Č. Budějovice: JU, PF, 2005..
  • PECH, P. Selected topics in geometry with classical vs. computer proving. New Jersey London Singapore: World Scientific Publishing, 2007..


Study plans that include the course
Faculty Study plan (Version) Category of Branch/Specialization Recommended year of study Recommended semester
Faculty: Faculty of Education Study plan (Version): Theory of Mathematics Education (2) Category: Pedagogy, teacher training and social care - Recommended year of study:-, Recommended semester: -
Faculty: Faculty of Education Study plan (Version): Theory of Mathematics Education (2) Category: Pedagogy, teacher training and social care - Recommended year of study:-, Recommended semester: -