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 SimsonWallace 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..
