Search Swinburne Research Bank
Please use this identifier to cite or link to this item: http://hdl.handle.net/1959.3/81325
|Download PDF (Published version) (Adobe Acrobat PDF, -1 bytes)|
- A task-oriented agent-based mechanism for theorem proving
- Vo, Quoc Bao
- 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
- Conference paper
- Proceedings of the IEEE/WIC International Conference on Intelligent Agent Technology (IAT 2003) / Jiming Liu, Boi Faltings, Matthias Klusch, and Chunnian Liu (eds.), pp. 275-281
- Publication year
- Axiom; Information agent; Knowledge base; Mathematics computing; Mathematical knowledge retrieval; Mediator module; Multi-agent systems; Multiagent systems; Proof search process; Software agents; Task-oriented agent-based mechanism; Theorem proving; User-oriented mediator; Value-added service
- 9780769519319, 0769519318
- Publisher URL
- Copyright © 2003 IEEE. Published version of the paper reproduced here in accordance with the copyright policy of the publisher. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.
- Full text
- Peer reviewed