Search Swinburne Research Bank
Please use this identifier to cite or link to this item: http://hdl.handle.net/1959.3/81316
- Assertion application in theorem proving and proof planning
- Vo, Quoc Bao; Benzmuller, Christoph; Autexier, Serge
- Our work addresses assertion retrieval and application in theorem proving systems or proof planning systems for classical firstorder logic. We propose a distributed mediator M between a mathematical knowledge base KB and a theorem proving system TP which is independent of the particular proof and knowledge representation formats of TP and KB and which applies generalized resolution in order to analyze the logical consequences of arbitrary assertions for a proof context at hand. We discuss the connection to proof planning and motivate an application in a project aiming at a tutorial dialogue system for mathematics.
- Publication type
- Conference paper
- Paper presented at the 10th Workshop on Automated Reasoning (ARW 2003), Liverpool, United Kingdom, 15-16 April 2003, pp. 7-8
- Publication year
- Assertion application; Assertion retrieval; Firstorder logic; Proof planning; Systems; Theorem proving
- Computer Science Department, University of Liverpool
- Publisher URL
- Copyright © 2003.