We describe the integration of permutation group algorithms with proof planning. We consider eight basic questions arising in computational permutation group theory, for which our code provides both answers and a set of certificates enabling a user, or an intelligent software system, to provide a full proof of correctness of the answer. To guarantee correctness we use proof planning techniques, which construct proofs in a human-oriented reasoning style. This gives the human mathematician the necessary insight into the computed solution, as well as making it feasible to check the solution for relatively large groups.
|Name||Lecture Notes in Computer Science|
|Conference||conference; 19th International Conference on Automated Deduction; 2003-07-28; 2003-08-02|
|Period||28/07/03 → 2/08/03|
|Other||19th International Conference on Automated Deduction|