OMRS (Open Mechanized Reasoning System(s)) is a framework and an architecture for the specification of theorem provers. In previous papers we have identified two major architectural principles underlying the design of theorem provers, namely: (a) they are often built by composing (integrating) multiple simpler systems (e.g., a rewriter and a decision procedure for linear arithmetic), and (b) search strategies can be very naturally implemented by annotating assertions with 'control' annotations. In this paper we formalize these ideas by means of mappings, and show how they can be used in the specification of the NQTHM waterfall
Composing and Controlling Search in Reasoning Theories using Mappings
Giunchiglia, Fausto;
2000-01-01
Abstract
OMRS (Open Mechanized Reasoning System(s)) is a framework and an architecture for the specification of theorem provers. In previous papers we have identified two major architectural principles underlying the design of theorem provers, namely: (a) they are often built by composing (integrating) multiple simpler systems (e.g., a rewriter and a decision procedure for linear arithmetic), and (b) search strategies can be very naturally implemented by annotating assertions with 'control' annotations. In this paper we formalize these ideas by means of mappings, and show how they can be used in the specification of the NQTHM waterfallFile in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
