[Home] [CV] [Publications]


Minus 1a5aa4f1c08b567c9107cba729de26bc87c17ab2b2f690eb45059193a1d6f587 Composing and Controlling Deduction in Reasoning Theories using Mappings
Coglio, A. and Giunchiglia, F. and Meseguer, J. and Talcott, C. L. - 2000

Reasoning theories can be used to specify heterogeneous reasoning systems. In this paper we present an equational version of reasoning theories, and we study their structuring and composition, and the use of annotated assertions for the control of search, as mappings between reasoning theories. We define composability and composition using the notion of \emphfaithful inclusion mapping, we define \emphannotated reasoning theories using the notion of \empherasing mapping, and we lift composability and composition to consider also annotations. As an example, we give a modular specification of the top-level control (known as waterfall) of NQTHM, the Boyer-Moore theorem prover.