Presenting Sets of Problem Solutions Concisely

摘要

Improvements in formal reasoning systems enable these systems to produce large sets of solutions that may grow rather complex. However, automatically generated presentations of these data lack a sufficient degree of conciseness. In order to improve the presentation of problem solutions that can be casted in terms of sets of ground atoms, we adapt linguistic aggregation techniques to specificities of formal problems. We define novel constructs that can express sets of propositions with highly regular alternations on predicate argument values concisely, including special forms of disjunctions and versions for formulas. We demonstrate applications to model generation and to categorization proofs. The presentations obtained highlight commonalities among and differences across solution parts in a much better way than previous approaches do, thereby supporting the inspection of properties holding across several solutions, and the discovery of flaws in problem specifications.