Interactive non-theorem disproving
Harsh Raju Chamarthi · 2016
We present a framework for interactively disproving non-theorems. It is designed as an extension to existing interactive theorem provers, adding semi-automated support for counterexample generation. The key ingredient of our framework is an enumerative and modifiable characterization of problem constraints. An enumerator provides the initial basis by generating data that conforms to monadic type constraints. A user-defined fixer further modifies input data to satisfy arbitrary constraints. We introduce two classes of user-specifiable rules, called fixer rules and preservation rules, that form the core of interactive non-theorem disproving. Our counterexample search method is based on concrete construction and executability combining property-based testing with proof-based deduction. We present various disproving techniques and discuss an implementation and evaluation of the framework using ACL2s.--Author's abstract