In this course are introduced the concepts of symbolic computation and demonstration of theorems in Algebra, using the GAP programming language and the automatic theorem prover PROVER9.
At the end of the course the student should be able to solve small problems appropriate to symbolic computation and automatic demonstration of theorems, namely proving theorems or finding counterexamples using automatic theorems provers; to know some of the most common functions of GAP, as well as its programming language.
a. GAP and its main functions o(lists, routines to extract sublists, arithmetic, matrices, transformations, groupings);
b. PROVER 9
c. Underlying algebraic background
- GAP Manuals: http://www.gap-system.org/Doc/manuals.html
- Prover9 Manual: http://www.cs.unm.edu/~mccune/mace4/manual-examples.html
Evaluation is made on individual basis and it involves the coexistence of two modes: continuous assessment (60%) and
final evaluation (40%). Further information is detailed in the Learning Agreement of the course unit.
