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 |
Subjects: | |
Online Access: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.698.1068 http://www.site.uottawa.ca/%7Eafelty/dist/FMP-Part2.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. |
---|