Guaranteed Proofs Using Interval Arithmetic

	This Article
	Subscribers, please Login Purchase article: $19 PDF IEEE Xplore Subscribers RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Marc Daumas Articles by Guillaume Melquiond Articles by César Muñoz

17th IEEE Symposium on Computer Arithmetic (ARITH'05)

Cape Cod, Massachusetts, USA

June 27-June 29

ISBN: 0-7695-2366-8

	ASCII Text	x
	Marc Daumas, Guillaume Melquiond, César Muñoz, "Guaranteed Proofs Using Interval Arithmetic," Computer Arithmetic, IEEE Symposium on, pp. 188-195, 17th IEEE Symposium on Computer Arithmetic (ARITH'05), 2005.

	BibTex	x
	@article{ 10.1109/ARITH.2005.25, author = {Marc Daumas and Guillaume Melquiond and César Muñoz}, title = {Guaranteed Proofs Using Interval Arithmetic}, journal ={Computer Arithmetic, IEEE Symposium on}, volume = {0}, year = {2005}, issn = {1063-6889}, pages = {188-195}, doi = {http://doi.ieeecomputersociety.org/10.1109/ARITH.2005.25}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Computer Arithmetic, IEEE Symposium on TI - Guaranteed Proofs Using Interval Arithmetic SN - 1063-6889 SP188 EP195 A1 - Marc Daumas, A1 - Guillaume Melquiond, A1 - César Muñoz, PY - 2005 KW - null VL - 0 JA - Computer Arithmetic, IEEE Symposium on ER -

Marc Daumas, CNRS-ENS Lyon-INRIA

Guillaume Melquiond, CNRS-ENS Lyon-INRIA

César Muñoz, National Institute of Aerospace

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ARITH.2005.25

This paper presents a set of tools for mechanical reasoning of numerical bounds using interval arithmetic. The tools implement two techniques for reducing decorrelation: interval splitting and Taylor?s series expansions. Although the tools are designed for the proof assistant system PVS, expertise on PVS is not required. The ultimate goal of the tools is to provide guaranteed proofs of numerical properties with a minimal human-theorem prover interaction.

Citation:

Marc Daumas, Guillaume Melquiond, César Muñoz, "Guaranteed Proofs Using Interval Arithmetic," arith, pp.188-195, 17th IEEE Symposium on Computer Arithmetic (ARITH'05), 2005

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.