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

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.

Abstract

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

Errata

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

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

postscript format.

BibTeX Entry


@inproceedings{Tiwari03:PDPAR,
	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.",
	PUBLISHER = {INRIA, Nancy},
	PAGES = {40--52},
	YEAR = 2003
}