An Approach to Assertion Application via Generalized Resolution (bibtex)
by Bao Quoc Vo, Christoph Benzmüller, Serge Autexier
Abstract:
In this paper we address assertion retrieval and application in theorem proving systems or proof planning systems for classical first-order logic. Due to Huang the notion of assertion comprises mathematical knowledge from a mathematical knowledge base KB such as definitions, theorems, and axioms. the prover during proof construction. We propose a distributed mediator module between KB and a theorem proving system S which is independent of the particular proof representation format of S and which applies generalized resolution in order to analyze the logical consequences of arbitrary assertions for a proof context at hand. Our approach is applicable without any extension also to the assumptions that are dynamically created during a proof search process. It therefore realizes a crucial first step towards full automation of assertion level reasoning. We discuss the benefits and connection of our approach to proof planning and motivate an application in a project aiming at a tutorial dialogue system for mathematics.
Reference:
An Approach to Assertion Application via Generalized Resolution (Bao Quoc Vo, Christoph Benzmüller, Serge Autexier), SEKI Publications (ISSN 1437-4447), number SR-03-01, 2003. (Url (preprint): http://christoph-benzmueller.de/papers/R20.pdf)
Bibtex Entry:
@techreport{R20,
  Abstract =	 {In this paper we address assertion retrieval and
                  application in theorem proving systems or proof
                  planning systems for classical first-order
                  logic. Due to Huang the notion of assertion
                  comprises mathematical knowledge from a mathematical
                  knowledge base KB such as definitions, theorems, and
                  axioms.  the prover during proof construction. We
                  propose a distributed mediator module between KB and
                  a theorem proving system S which is independent of
                  the particular proof representation format of S and
                  which applies generalized resolution in order to
                  analyze the logical consequences of arbitrary
                  assertions for a proof context at hand. Our approach
                  is applicable without any extension also to the
                  assumptions that are dynamically created during a
                  proof search process. It therefore realizes a
                  crucial first step towards full automation of
                  assertion level reasoning. We discuss the benefits
                  and connection of our approach to proof planning and
                  motivate an application in a project aiming at a
                  tutorial dialogue system for mathematics.},
  Author =	 {Bao Quoc Vo and Christoph Benzm{\"u}ller and Serge
                  Autexier},
  Institution =	 {Saarland University, SEKI Publications (ISSN
                  1437-4447)},
  Number =	 {SR-03-01},
  Publisher =	 {SEKI Publications (ISSN 1437-4447)},
  Title =	 {An Approach to Assertion Application via Generalized
                  Resolution},
  Type =	 {SEKI Report},
  Note =	 {Url (preprint):
                  \url{http://christoph-benzmueller.de/papers/R20.pdf}},
  Year =	 2003,
}
Powered by bibtexbrowser