Assertion application in theorem proving and proof planning

Search Swinburne Research Bank

Home

Please use this identifier to cite or link to this item: http://hdl.handle.net/1959.3/81316

Title: Assertion application in theorem proving and proof planning
Author(s): Vo, Quoc Bao; Benzmuller, Christoph; Autexier, Serge
Abstract: 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
Source: Paper presented at the 10th Workshop on Automated Reasoning (ARW 2003), Liverpool, United Kingdom, 15-16 April 2003, pp. 7-8
Publication year: 2003
Keyword(s): Assertion application; Assertion retrieval; Firstorder logic; Proof planning; Systems; Theorem proving
Publisher: Computer Science Department, University of Liverpool
Publisher URL: http://www.csc.liv.ac.uk/~clare/arw03/