A variety of logical frameworks supports the use of higher order abstract syntax in representing formal systems. Although these systems seem superficially the same, they differ in a variety of ways, for example, how they handle a context of assumptions and which theorems about a given formal system can be concisely expressed and proved. Our contributions in this paper are two-fold: (1) We develop a common infrastructure and language for describing benchmarks for systems supporting reasoning with binders, and (2) we present several concrete benchmarks, which highlight a variety of different aspects of reasoning within a context of assumptions. Our work provides the background for the qualitative comparison of different systems that we have completed in a separate paper. It also allows us to outline future fundamental research questions regarding the design and implementation of meta-reasoning systems.
Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions / A. Felty, A. Momigliano, B. Pientka. - In: MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE. - ISSN 0960-1295. - (2017). [Epub ahead of print] [10.1017/S0960129517000093]
Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions
A. MomiglianoSecondo
;
2017
Abstract
A variety of logical frameworks supports the use of higher order abstract syntax in representing formal systems. Although these systems seem superficially the same, they differ in a variety of ways, for example, how they handle a context of assumptions and which theorems about a given formal system can be concisely expressed and proved. Our contributions in this paper are two-fold: (1) We develop a common infrastructure and language for describing benchmarks for systems supporting reasoning with binders, and (2) we present several concrete benchmarks, which highlight a variety of different aspects of reasoning within a context of assumptions. Our work provides the background for the qualitative comparison of different systems that we have completed in a separate paper. It also allows us to outline future fundamental research questions regarding the design and implementation of meta-reasoning systems.File | Dimensione | Formato | |
---|---|---|---|
all.pdf
accesso aperto
Descrizione: Articolo principale
Tipologia:
Pre-print (manoscritto inviato all'editore)
Dimensione
423.47 kB
Formato
Adobe PDF
|
423.47 kB | Adobe PDF | Visualizza/Apri |
benchmarks-for-reasoning-with-syntax-trees-containing-binders-and-contexts-of-assumptions.pdf
accesso riservato
Tipologia:
Publisher's version/PDF
Dimensione
380.24 kB
Formato
Adobe PDF
|
380.24 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.