© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Adding the axioms to Axiom: Towards a system of automated reasoning in Aldor
Erik Poll and Simon Thompson
Technical Report 6-98, Computing Laboratory, University of Kent, May 1998 Presented at the workshop Calculemus and Types, Eindhoven, Netherlands, July 1998. <a href="http://www.win.tue.nl/math/dw/pp/calc/">Workshop website</a>.Abstract
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.
Download publication 176 kbytes (PostScript)Bibtex Record
@techreport{584, author = {Erik Poll and Simon Thompson}, title = {{Adding the axioms to Axiom: Towards a system of automated reasoning in Aldor}}, month = {May}, year = {1998}, pages = {182-196}, keywords = {determinacy analysis, Craig interpolants}, note = {Presented at the workshop Calculemus and Types, Eindhoven, Netherlands, July 1998. Workshop website}, doi = {}, url = {http://www.cs.kent.ac.uk/pubs/1998/584}, institution = {Computing Laboratory, University of Kent}, number = {6-98}, type = {Technical Report}, }