Annotated reasoning

Authors
Citation
D. Hutter, Annotated reasoning, ANN MATH A, 29(1-4), 2000, pp. 183-222
Citations number
31
Categorie Soggetti
Engineering Mathematics
Journal title
ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE
ISSN journal
10122443 → ACNP
Volume
29
Issue
1-4
Year of publication
2000
Pages
183 - 222
Database
ISI
SICI code
1012-2443(2000)29:1-4<183:AR>2.0.ZU;2-5
Abstract
The application of deduction in various domains resulted in a variety of di fferent techniques to guide the proof search. Many of these techniques inco rporate additional knowledge to restrict or select possible proof steps. As a consequence, usually the underlying calculus has to he modified to keep track of this information during the proof search. In this paper we present a general framework fur maintaining additional strategic knowledge within a proof. We introduce a formal notion of annotations attached to the consti tuents of formulas and illustrate how a generic method of inheriting these annotations can br instantiated for various purposes.