Hint Orchestration Using ACL2's Simplifier
This paper describes a strategy for providing hints during an ACL2 proof, implemented in a utility called use-termhint. An extra literal is added to the goal clause and simplified along with the rest of the goal until it is stable under simplification, after which the simplified literal is examined...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2018-10-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1810.04318v1 |