Over the past three decades, a variety of meta-reasoning systems which support reasoning about higher-order abstract specifications have been designed and developed. In this paper, we survey and compare four meta-reasoning systems, Twelf, Beluga, Abella and Hybrid, using several benchmarks from the open repository ORBI that describes challenge problems for reasoning with higher-order abstract syntax representations. In particular, we investigate how these systems mechanize and support reasoning using a context of assumptions. This highlights commonalities and differences in these systems and is a first step towards translating between them.
The next 700 challenge problems for reasoning with higher-order abstract syntax representations : part 2: a survey / A.P. Felty, A. Momigliano, B. Pientka. - In: JOURNAL OF AUTOMATED REASONING. - ISSN 0168-7433. - 55:4(2015 Dec), pp. 307-372.
The next 700 challenge problems for reasoning with higher-order abstract syntax representations : part 2: a survey
A. MomiglianoSecondo
;
2015
Abstract
Over the past three decades, a variety of meta-reasoning systems which support reasoning about higher-order abstract specifications have been designed and developed. In this paper, we survey and compare four meta-reasoning systems, Twelf, Beluga, Abella and Hybrid, using several benchmarks from the open repository ORBI that describes challenge problems for reasoning with higher-order abstract syntax representations. In particular, we investigate how these systems mechanize and support reasoning using a context of assumptions. This highlights commonalities and differences in these systems and is a first step towards translating between them.File | Dimensione | Formato | |
---|---|---|---|
companion-jar.pdf
accesso aperto
Tipologia:
Pre-print (manoscritto inviato all'editore)
Dimensione
533.83 kB
Formato
Adobe PDF
|
533.83 kB | Adobe PDF | Visualizza/Apri |
art%3A10.1007%2Fs10817-015-9327-3.pdf
accesso riservato
Tipologia:
Publisher's version/PDF
Dimensione
10.54 MB
Formato
Adobe PDF
|
10.54 MB | 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.