Turning the Theory into Practice

• Algorithm:

  • Traverse proof from root node to leaves in depth first manner
  • For each node
    • identify the applicable MCC
    • collect relevant mathematical information from formal proof node
    • create relevant sentence

Previous slide

Next slide

Back to first slide

View graphic version