Beagle as a HOL4 external ATP method
| Autor: | Cezary Kaliszyk, Thibault Gauthier, Chantal Keller, Michael Norrish |
|---|---|
| Přispěvatelé: | Leopold Franzens Universität Innsbruck - University of Innsbruck, Programming securely with cryptography (PROSECCO), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Microsoft Research - Inria Joint Centre (MSR - INRIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Microsoft Research Laboratory Cambridge-Microsoft Corporation [Redmond, Wash.], NICTA Canberra labs, National ICT Australia [Sydney] (NICTA), University of Innsbruck, Keller, Chantal |
| Rok vydání: | 2018 |
| Předmět: |
Engineering
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO] Programming language business.industry [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] HOL 020207 software engineering 0102 computer and information sciences 02 engineering and technology Translation (geometry) computer.software_genre 01 natural sciences Beagle 010201 computation theory & mathematics 0202 electrical engineering electronic engineering information engineering business Algorithm computer TRACE (psycholinguistics) |
| Zdroj: | PAAR-Fourth Workshop on Practical Aspects of Automated Reasoning PAAR-Fourth Workshop on Practical Aspects of Automated Reasoning, Jul 2014, Vienne, Austria |
| ISSN: | 2398-7340 |
| DOI: | 10.29007/8xbv |
| Popis: | This paper presents BEAGLE TAC, a HOL4 tactic for using Beagle as an external ATP fordischarging HOL4 goals. We implement a translation of the higher-order goals to the TFAformat of TPTP and add trace output to Beagle to reconstruct the intermediate steps derivedby the ATP in HOL4. Our translation combines the characteristics of existing successfultranslations from HOL to FOL and SMT-LIB, however we needed to adapt certain stagesof the translation in order to benefit form the expressivity of the TFA format and the powerof Beagle. In our initial experiments, we demonstrate that our system can prove, withoutany arithmetic lemmas, 81% of the goals solved by Metis. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|