Journal of Automated Reasoning manuscript No. (will be inserted by the editor) The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations Part 2—A Survey
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 sys-tems, Twelf, Beluga, Abella and Hybrid, using several benchmarks...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Text |
| Language: | English |
| Published: |
2014
|
| Subjects: | |
| Online Access: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.673.6490 http://www.cs.mcgill.ca/%7Ebpientka/papers/orbi-survey-nov2015.pdf |
| Summary: | 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 sys-tems, 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 trans-lating between them. |
|---|