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

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 waterfall
File 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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11582/1536
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact