Meta-extract: Using Existing Facts in Meta-reasoning

Meta-extract: Using Existing Facts in Meta-reasoning

ACL2 has long supported user-defined simplifiers, so-called metafunctions and clause processors, which are installed when corresponding rules of class :meta or :clause-processor are proved. Historically, such simplifiers could access the logical world at execution time and could call certain built-...

Full description

Bibliographic Details
Main Authors: Matt Kaufmann, Sol Swords
Format: Article
Language:English
Published: Open Publishing Association 2017-05-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1705.01227v1
id doaj-32c2e9e0d12242f29818c3c707422bf3
record_format Article
spelling doaj-32c2e9e0d12242f29818c3c707422bf32020-11-25T02:32:45ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802017-05-01249Proc. ACL2Workshop 2017476010.4204/EPTCS.249.4:1Meta-extract: Using Existing Facts in Meta-reasoningMatt KaufmannSol SwordsACL2 has long supported user-defined simplifiers, so-called metafunctions and clause processors, which are installed when corresponding rules of class :meta or :clause-processor are proved. Historically, such simplifiers could access the logical world at execution time and could call certain built-in proof tools, but one could not assume the soundness of the proof tools or the truth of any facts extracted from the world or context when proving a simplifier correct. Starting with ACL2 Version 6.0, released in December 2012, an additional capability was added which allows the correctness proofs of simplifiers to assume the correctness of some such proof tools and extracted facts. In this paper we explain this capability and give examples that demonstrate its utility.http://arxiv.org/pdf/1705.01227v1
collection DOAJ
language English
format Article
sources DOAJ
author Matt Kaufmann
Sol Swords
spellingShingle Matt Kaufmann
Sol Swords
Meta-extract: Using Existing Facts in Meta-reasoning
Electronic Proceedings in Theoretical Computer Science
author_facet Matt Kaufmann
Sol Swords
author_sort Matt Kaufmann
title Meta-extract: Using Existing Facts in Meta-reasoning
title_short Meta-extract: Using Existing Facts in Meta-reasoning
title_full Meta-extract: Using Existing Facts in Meta-reasoning
title_fullStr Meta-extract: Using Existing Facts in Meta-reasoning
title_full_unstemmed Meta-extract: Using Existing Facts in Meta-reasoning
title_sort meta-extract: using existing facts in meta-reasoning
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2017-05-01
description ACL2 has long supported user-defined simplifiers, so-called metafunctions and clause processors, which are installed when corresponding rules of class :meta or :clause-processor are proved. Historically, such simplifiers could access the logical world at execution time and could call certain built-in proof tools, but one could not assume the soundness of the proof tools or the truth of any facts extracted from the world or context when proving a simplifier correct. Starting with ACL2 Version 6.0, released in December 2012, an additional capability was added which allows the correctness proofs of simplifiers to assume the correctness of some such proof tools and extracted facts. In this paper we explain this capability and give examples that demonstrate its utility.
url http://arxiv.org/pdf/1705.01227v1
work_keys_str_mv AT mattkaufmann metaextractusingexistingfactsinmetareasoning
AT solswords metaextractusingexistingfactsinmetareasoning
_version_ 1724817985651081216

Similar Items