Meta-level reasoning was added to the Boyer-Moore theorem prover by 1979. We have recently re-implemented and, we think, slightly improved our approach to meta-theoretic reasoning in the Acl2 theorem prover. However, there is lots of room for much more substantial improvement. Our talk will consist of 3 parts: review, recent results, and general remarks.
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
Strategic Construction of Fitch-Style Proofs.Frederic D. Portoraro - 1998 - Studia Logica 60 (1):45-66.
The Addition of Bounded Quantification and Partial Functions to a Computational Logic and its Theorem Prover.Robert Boyer - manuscript
The Classification of Small Weakly Minimal Sets. II.Steven Buechler - 1988 - Journal of Symbolic Logic 53 (2):625-635.
One Theorem of Zil'ber's on Strongly Minimal Sets.Steven Buechler - 1985 - Journal of Symbolic Logic 50 (4):1054-1061.
The Classification of Small Weakly Minimal Sets. III: Modules.Steven Buechler - 1988 - Journal of Symbolic Logic 53 (3):975-979.
The Geometry of Weakly Minimal Types.Steven Buechler - 1985 - Journal of Symbolic Logic 50 (4):1044-1053.
Sorry, there are not enough data points to plot this chart.
Added to index2009-01-28
Recent downloads (6 months)0
How can I increase my downloads?
There are no threads in this forum
Nothing in this forum yet.