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)

Abstract

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: Faculties > Sciences > School of Computing
Depositing User: Mark Wheadon
Date Deposited: 30 Aug 2009 17:11 UTC
Last Modified: 31 May 2019 08:32 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/22041 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year