- Tobias Schmidt-Samoa
- An Even Closer Integration of Linear Arithmetic into
Inductive Theorem Proving
- Proc. 12th Symposium on the
Integration of Symbolic Computation and Mechanized Reasoning
Electronic Notes in Theoretical Computer Sci. 2006, 151, pp. 3-20,
- Copyright Owner
- 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
First, to provide detailed proof objects for proof checking and
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
- . Mbytes
- . Mbytes
- The fonts of the following pdf version differ from the original,
some originally identical fonts are different in this version,
but the whole file can be searched!
- .2 Mbytes