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.
|Titolo:||The next 700 challenge problems for reasoning with higher-order abstract syntax representations : part 2: a survey|
MOMIGLIANO, ALBERTO (Secondo)
|Parole Chiave:||Logical frameworks; Higher-order abstract syntax; Proof assistants; Benchmarks; Context reasoning|
|Settore Scientifico Disciplinare:||Settore INF/01 - Informatica|
|Data di pubblicazione:||dic-2015|
|Digital Object Identifier (DOI):||10.1007/s10817-015-9327-3|
|Appare nelle tipologie:||01 - Articolo su periodico|