Poll, Erik and Thompson, Simon (1998) Adding the axioms to Axiom: Towards a system of automated reasoning in Aldor. Technical report. Kent University
| Postscript | ||
|
Download (176Kb)
|
![[img]](http://kar.kent.ac.uk/style/images/fileicons/application_postscript.png)
|
|
|
Download (216Kb)
|
![[img]](http://kar.kent.ac.uk/style/images/fileicons/application_pdf.png)
|
|
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.
| Item Type: | Monograph (Technical report) |
|---|---|
| Additional information: | Presented at the workshop Calculemus and Types, Eindhoven, Netherlands, July 1998. http://www.win.tue.nl/math/dw/pp/calc/ |
| Uncontrolled keywords: | Axiom Aldor reasoning dependent type category combination |
| Subjects: | Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, |
| Divisions: | Faculties > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group |
| Depositing User: | Mark Wheadon |
| Date Deposited: | 22 Aug 2009 13:57 |
| Last Modified: | 06 Sep 2011 04:01 |
| Resource URI: | http://kar.kent.ac.uk/id/eprint/21662 (The current URI for this page, for reference purposes) |
- Depositors only (login required):
