Interactive (Non)Theorem (Dis)Proving

PhD Thesis Proposal, Harsh Raju Chamarthi, 2015. [PDF]

Abstract

We present a framework for interactively disproving non-theorems. Our method can be used to add automated disproving and counterexample generation capabilities to existing interactive theorem provers. This capability increases the utility and effectiveness of theorem provers because it provides automated support for what users spend most of their time doing: debugging flawed models, invariants, interfaces and conjectures. We present various disproving techniques and discuss an implementation and evaluation of the framework using ACL2s, the ACL2 Sedan.

Committee

Committee Composition Justification

Karl Lieberherr is an expert on SAT and CSP. Olin Shivers is an expert on Static Analysis. Matt Kaufmann is an expert on interactive theorem proving and logic. He is an author of ACL2, a widely-used interactive theorem prover, for which he won the ACM Software System award. -- Pete