Authors
Tobias Schmidt-Samoa
Title
An Even Closer Integration of Linear Arithmetic into Inductive Theorem Proving
In
Proc. 12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (Calculemus 2005), Electronic Notes in Theoretical Computer Sci. 2006, 151, pp. 3-20, Elsevier
Copyright Owner
Elsevier
Abstract
To broaden the scope of decision procedures for linear arithmetic, they have to be integrated into theorem provers. Successful approaches e.g. in NQTHM or ACL2 suggest a close integration scheme which augments the decision procedures with lemmas about user-defined operators. We propose an even closer integration providing feedback about the state of the decision procedure in terms of entailed formulas for three reasons: First, to provide detailed proof objects for proof checking and archiving. Second, to analyze and improve the interaction between the decision procedure and the theorem prover. Third, to investigate whether the communication of the state of a failed proof attempt to the human user with the comprehensible standard GUI mechanisms of the theorem prover can enhance the speculation of auxiliary lemmas.
Full paper