Quality Metric for Proofs
- Ranking proofs (can be used for evaluation of solvers)
- Improving proofs
- Selecting proofs for different uses
- Displaying proofs to different users
- 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.