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...

Full description

Bibliographic Details
Main Author: Brigitte Pientka
Other Authors: The Pennsylvania State University CiteSeerX Archives
Format: Text
Language:English
Published: 2014
Subjects:
Beluga
Beluga*
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
id ftciteseerx:oai:CiteSeerX.psu:10.1.1.673.6490
record_format openpolar
spelling ftciteseerx:oai:CiteSeerX.psu:10.1.1.673.6490 2023-05-15T15:41:48+02:00 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 Brigitte Pientka The Pennsylvania State University CiteSeerX Archives 2014 application/pdf http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.673.6490 http://www.cs.mcgill.ca/%7Ebpientka/papers/orbi-survey-nov2015.pdf en eng http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.673.6490 http://www.cs.mcgill.ca/%7Ebpientka/papers/orbi-survey-nov2015.pdf Metadata may be used without restrictions as long as the oai identifier remains attached to it. http://www.cs.mcgill.ca/%7Ebpientka/papers/orbi-survey-nov2015.pdf text 2014 ftciteseerx 2016-01-08T17:29:37Z 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. Text Beluga Beluga* Unknown
institution Open Polar
collection Unknown
op_collection_id ftciteseerx
language English
description 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.
author2 The Pennsylvania State University CiteSeerX Archives
format Text
author Brigitte Pientka
spellingShingle Brigitte Pientka
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
author_facet Brigitte Pientka
author_sort Brigitte Pientka
title 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
title_short 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
title_full 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
title_fullStr 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
title_full_unstemmed 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
title_sort 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
publishDate 2014
url http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.673.6490
http://www.cs.mcgill.ca/%7Ebpientka/papers/orbi-survey-nov2015.pdf
genre Beluga
Beluga*
genre_facet Beluga
Beluga*
op_source http://www.cs.mcgill.ca/%7Ebpientka/papers/orbi-survey-nov2015.pdf
op_relation http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.673.6490
http://www.cs.mcgill.ca/%7Ebpientka/papers/orbi-survey-nov2015.pdf
op_rights Metadata may be used without restrictions as long as the oai identifier remains attached to it.
_version_ 1766374689790230528

Similar Items