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 faithful inclusion mapping, we define annotated reasoning theories using the notion of erasing 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.
Composing and Controlling Search in Reasoning Theories Using Mappings
Giunchiglia, Fausto;
2000-01-01
Abstract
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 faithful inclusion mapping, we define annotated reasoning theories using the notion of erasing 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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione
