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. Momigliano
Secondo
;
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.
Logical frameworks; Higher-order abstract syntax; Proof assistants; Benchmarks; Context reasoning
Settore INF/01 - Informatica
dic-2015
Article (author)
File in questo prodotto:
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/287686
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 25
  • ???jsp.display-item.citation.isi??? 12
social impact