School of Computing

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},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014