ML Anthology

Assertion Application in Theorem Proving and Proof Planning

Quoc Bao Vo, Christoph Benzmüller, Serge Autexier
IJCAI 2003 pp. 1343-
/ijcai/2003/vo2003ijcai-assertion/

Abstract

Our work addresses assertion retrieval and application in theorem proving systems or proof planning systems for classical first-order 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. This paper is a short version of [9]. 1 Proof planning at the assertion level Due to Huang [6], the notion of assertion comprises mathematical knowledge from a mathematical knowledge base KB such as axioms, definitions, and theorems. Huang argues that an assertion-based representation, i.e. assertion level, is just

PDF Semantic Scholar

Cite

Text

Vo et al. "Assertion Application in Theorem Proving and Proof Planning." International Joint Conference on Artificial Intelligence, 2003.

Markdown

[Vo et al. "Assertion Application in Theorem Proving and Proof Planning." International Joint Conference on Artificial Intelligence, 2003.](https://mlanthology.org/ijcai/2003/vo2003ijcai-assertion/)

BibTeX

@inproceedings{vo2003ijcai-assertion,
  title     = {{Assertion Application in Theorem Proving and Proof Planning}},
  author    = {Vo, Quoc Bao and Benzmüller, Christoph and Autexier, Serge},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {2003},
  pages     = {1343-},
  url       = {https://mlanthology.org/ijcai/2003/vo2003ijcai-assertion/}
}