Skip to main content

Integrating Computer Algebra and Reasoning through the Type System of Aldor

Poll, Erik and Thompson, Simon (2000) Integrating Computer Algebra and Reasoning through the Type System of Aldor. In: Kirchner, Hélène and Ringeissen, Christophe, eds. Frontiers of Combining Systems Third International Workshop. Lecture Notes in Computer Science, 1794 . Springer, Berlin, Germany, pp. 136-150. ISBN 978-3-540-67281-4. E-ISBN 978-3-540-46421-1. (doi:10.1007/10720084_10) (KAR id:22041)

Language: English
Download (344kB) Preview
[thumbnail of Integrating_Computer_Algebra_and_Reasoning_through_the_Type_System_of_Aldor.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL:


A number of combinations of reasoning 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 Alder - 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 and explain a prototype implementation of a modified type-checking system written in Haskell.

Item Type: Book section
DOI/Identification number: 10.1007/10720084_10
Uncontrolled keywords: computer algebra, reasoning, Axiom, Aldor
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 75 Electronic computers. Computer science
Q Science > Q Science (General) > Q335 Artificial intelligence
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Wheadon
Date Deposited: 30 Aug 2009 17:11 UTC
Last Modified: 16 Nov 2021 10:00 UTC
Resource URI: (The current URI for this page, for reference purposes)
Thompson, Simon:
  • Depositors only (login required):


Downloads per month over past year