Quality Metric for Proofs

Our Interests

• Ranking proofs (can be used for evaluation of solvers)
• Improving proofs
• Selecting proofs for different uses
• Displaying proofs to different users

Our Needs

• Ways of accepting something as a proof
• Quantitative metrics for ranking proofs
• Ways to partially order proofs by quality

Questions that Arise

• What constitutes an acceptable solution from a logic solver?
  • What does NOT constitute an acceptable solution/output?
• What features of solutions should be used to assess their quality?
  • What features should NOT be used?
  • What features are developer-specific, what features are user-specific, and what features are globally important?
• What mechanisms (should) exist by which existing solutions can be postprocessed to improve their quality?
• Is a common verification/validation process possible/desirable for a broad range of logics and their solvers' solutions?
• Provide some examples from current solvers' solutions that illustrate good and bad solutions, wrt points previously addressed.