A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover.

K. Rustan M. Leino, Madan Musuvathi, Xinming Ou

Browse the full TACAS paper archive.