Meta-extract: Using Existing Facts in Meta-reasoning
The work
| Authors | Matt Kaufmann; Sol Swords |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2017 |
| Citekey | kaufmann2017metaextract |
Where it appeared
| Published in | Proceedings of the 14th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2017) |
|---|---|
| Series | Electronic Proceedings in Theoretical Computer Science |
| Volume | 249 |
| Pages | 47--60 |
Identifiers
| arXiv | 1705.01227 from its landing_page_url |
|---|---|
| DOI | 10.4204/eptcs.249.4 |
Access
| Landing page | https://arxiv.org/abs/1705.01227 |
|---|
Related
| Distinct from | peng2018smtlink |
|---|
From bibtex.
Abstract
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.
A copy is held
pdf, 143.5 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-09-17 21:44 UTC |
| Approved by | a person 2026-10-05 21:25 UTC |
Filed under
Cite it as
@inproceedings{kaufmann2017metaextract,
title = {Meta-extract: Using Existing Facts in Meta-reasoning},
author = {Matt Kaufmann and Sol Swords},
year = {2017},
booktitle = {Proceedings of the 14th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2017)},
series = {Electronic Proceedings in Theoretical Computer Science},
volume = {249},
pages = {47--60},
doi = {10.4204/eptcs.249.4},
}
This record lives at https://refs.drheap.org/kaufmann2017metaextract/ and will keep doing so.