Adding the axioms to Axiom: Towards a system of automated reasoning in Aldor
Erik Poll, Simon Thompson · Kent Academic Repository (University of Kent) · 1998
A number of combinations of theorem proving and computer algebra systems have been proposed; in this paper we describe another, namely a way to incorporate a logic in the computer algebra system Axiom. We examine the type system of Aldor -- the Axiom Library Compiler -- and show that with some modifications we can use the dependent types of the system to model a logic, under the Curry-Howard isomorphism. We give a number of example applications of the logic we construct. 1 Introduction Symbolic mathematical -- or computer algebra -- systems, such as Axiom [JS92], Maple and Mathematica, are in everyday use by scientists, engineers and indeed mathematicians, because they provide a user with techniques of, say, integration which far exceed those of the person themselves, and make routine many calculations which would have been impossible some years ago. These systems are, moreover, taught as standard tools within many university undergraduate programmes and are used in support of both ac...