MICS
2010
13 years 10 months ago
2010
Abstract. There is something of a discontinuity at the heart of popular tactical theorem provers. Low-level, fully-checked mechanical proofs are large trees consisting of primitive...