Abstraction Based Theorem Proving: An example from the theory of Reals

Ashish Tiwari

To be presented at PDPAR 2003, Miami, FL Jul 29 2003. Colocated with CADE 2003 .
Proceedings will be published as an INRIA technical report.


This paper presents a sound, but incomplete, logical decision procedure for the quantifier-free theory of reals. It is obtained using a combination of superposition and ordered chaining calculi. The emphasis is on termination and efficiency, rather than completeness. The procedure is used at the core of an hybrid abstraction tool for creating finite state sound abstractions of hybrid systems.

Download document in postscript format


On page9: the second inference rule in the Heuristics section is missing a side condition (R \cup S) \models \mu \geq 0. The corrected version of the paper is available on this web page. Click here for a new version with revised inference rules.


Slides of the presentation at PDPAR (CADE 2003) are available here in postscript format.

BibTeX Entry

	TITLE = "Abstraction Based Theorem Proving: {A}n example from the theory of Reals",
	AUTHOR = {Tiwari, A.},
	BOOKTITLE = {Proceedings of the CADE-19 WOrkshop on Pragmatics of Decision Procedures in Automated Deduction, PDPAR 2003},
	EDITOR = "Tinelli, C. and Ranise, S.",
	PAGES = {40--52},
	YEAR = 2003

Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page