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

### 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.

### 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
}