 Authors
 Tobias SchmidtSamoa
 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. 320,
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 userdefined 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



 Format
 all.ps.gz
 Size
 . Mbytes

 Format
 .dvi.gz
 Size
 . 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!
 Format
 .pdf
 Size
 .2 Mbytes