Background

• Previous work in area focused on generation from low-level proofs

  • lots of unnecessary and obvious information gets included
  • ordering proof steps is a significant problem
  • tactic-style proofs generated as an intermediate representation

• Template based generation from tactic proofs is unsatisfactory

Previous slide

Next slide

Back to first slide

View graphic version