IW Meeting 2009-08-20

From Inference Web

Jump to: navigation, search


  • combine proof
    • multi phases combine
    • mizar proofs



  • It's odd that you have proofs from two versions of EP. It's not wrong, but for clarity we should (by default) use only the latest version's proofs. I.e., here you should not use the 0.999 proofs.
  • we should extract another statistic for each proof - the number of nodes from each contributing ATP system. In this Metis proof that statistic would show 59 from EP and 1 from Metis, which shows the Metis proof has been replaced by EP proof steps.
  • In the table, can you highlight, e.g., use a red font, the % values that are an improvement.

  • Experiment 1. Combine all the human proofs from mizar as one group.
  • Experiment 2 has three parts ...
    • 1. Convert all the +1 versions' proofs and try combining
    • 2. Convert all the +2 versions' proofs and try combining
    • 3. Try combining the +1 and +2 versions' proofs
Personal tools