Hybrid: A Definitional Two-Level Approach to Reasoning with Higher-Order Abstract Syntax
| Autor: | Felty, Amy, Momigliano, Alberto |
|---|---|
| Rok vydání: | 2008 |
| Předmět: | |
| Druh dokumentu: | Working Paper |
| Popis: | Combining higher-order abstract syntax and (co)induction in a logical framework is well known to be problematic. Previous work described the implementation of a tool called Hybrid, within Isabelle HOL, which aims to address many of these difficulties. It allows object logics to be represented using higher-order abstract syntax, and reasoned about using tactical theorem proving and principles of (co)induction. In this paper we describe how to use it in a multi-level reasoning fashion, similar in spirit to other meta-logics such as Twelf. By explicitly referencing provability in a middle layer called a specification logic, we solve the problem of reasoning by (co)induction in the presence of non-stratifiable hypothetical judgments, which allow very elegant and succinct specifications of object logic inference rules. Comment: 58 pages, with 12 figures. To appear in the Journal of Automated Reasoning, accepted April 2010. For associated code, see http://hybrid.dsi.unimi.it/jar/index.html |
| Databáze: | arXiv |
| Externí odkaz: |
|