Search Swinburne Research Bank
Please use this identifier to cite or link to this item: http://hdl.handle.net/1959.3/62484
 Download PDF (Accepted manuscript) (Adobe Acrobat PDF, -1 bytes) |
- Title
- A task-oriented agent-based mechanism for mathematical assistant systems
- Author(s)
- Vo, Quoc Bao
- Abstract
- We present an agent-based mechanism that acts as a mediator module between theorem proving systems and mathematical knowledge bases containing information that is necessary for the constructions of proofs. Unlike the more popular user-oriented mediators who work as information agents to provide the so-called value-added services to the collected data before presenting it to users or user applications, our (multi-)agents are more task-oriented. That is, our agents work in tandem with the user or user application on the tasks the user is trying to solve. This approach is particularly suitable to mathematical knowledge retrieval in theorem proving as (i) checking for applicable axioms/definitions/ theorems from the knowledge base can be done independently from the proof search process concurrently carried out by the prover, and (ii) the prover and the mediator operate on two different search spaces and the search outcome brought about by the mediator can be of great benefit to the prover, e.g. to avoid the prover from exploring many unnecessary or irrelevant proof steps, to keep the prover's search space more manageable and the constructed proof more comprehensible.
- Publication type
- Journal article
- Source
- Web Intelligence and Agent Systems, Vol. 2, no. 1 (Mar 2004), pp. 71-86
- Publication year
- 2004
- Keyword(s)
- Agent-based mechanism; Algebra; Computer programming; Data acquisition; Decision making; Digital libraries; Information agents; Information technology; Internet; MathAS; Mathematical assistant systems; Problem solving; Theorem proving; Value-added services
- Publisher
- IOS Press
- ISSN
- 1570-1263
- Publisher URL
- http://iospress.metapress.com/content/u3t58jr8fhrnyq67/
- Copyright
- Copyright © 2004 IOS Press and the author. The accepted manuscript is reproduced in accordance with the copyright policy of the publisher.
- Full text
- Peer reviewed
