The most effective theorem proving systems (such as PVS, Acl2, and HOL) provide a kind of two-level reasoning, where the knowledge of a given domain is treated by a special purpose reasoner and a generic reasoning module is used for the actual problem specification. To obtain an effective integration between these two levels of reasoning is far from being a trivial task. In this paper, we propose a combination of Window Reasoning and Constraint Contextual Rewriting to achieve an effective integration of such levels. The former supports hierarchical reasoning for arbitrarily complex expressions. The latter provides the necessary theorem proving support for domain specific reasoning. The two levels of reasoning cooperate by building and exploiting a context, i. e. a set of facts which can be assumed true while transforming a given subexpression. We also argue that the proposed combination schema can be useful for building sound simplifiers to be used in computer algebra systems.
Combining generic and domain specific reasoning by using contexts / Ranise, S.. - 2385:(2002), pp. 305-318. (Intervento presentato al convegno Joint Conferences on 6th Artificial Intelligence and Symbolic Computation, AISC 2002 and 10th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2002 tenutosi a fra nel 2002) [10.1007/3-540-45470-5].
Combining generic and domain specific reasoning by using contexts
Ranise S.
2002-01-01
Abstract
The most effective theorem proving systems (such as PVS, Acl2, and HOL) provide a kind of two-level reasoning, where the knowledge of a given domain is treated by a special purpose reasoner and a generic reasoning module is used for the actual problem specification. To obtain an effective integration between these two levels of reasoning is far from being a trivial task. In this paper, we propose a combination of Window Reasoning and Constraint Contextual Rewriting to achieve an effective integration of such levels. The former supports hierarchical reasoning for arbitrarily complex expressions. The latter provides the necessary theorem proving support for domain specific reasoning. The two levels of reasoning cooperate by building and exploiting a context, i. e. a set of facts which can be assumed true while transforming a given subexpression. We also argue that the proposed combination schema can be useful for building sound simplifiers to be used in computer algebra systems.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione