We present a proof-generating decision procedure for the quantifier-free fragment of first-order logic with the relations =, !=, >=, and > and argue that this logic, augmented with a set of theory-specific rewriting rules, is adequate for bi...Expand abstract...
- Publication status:
- Peer review status:
- Peer reviewed
- Accepted Manuscript
- Publication date:
- Local pid:
- Copyright holder:
- Springer-Verlag Berlin Heidelberg
- Copyright date:
- Citation: Kroening, D. & Weissenbacher, G. (2011) An interpolating decision procedure for transitive relations with uninterpreted functions. In: Namjoshi, K., Zeller, A. & Ziv, A. (eds.) Hardware and software: Verification and Testing. 5th International Haifa Verification Conference, HVC 2009, Haifa, Israel, October 19-22, 2009, Revised Selected Papers. Lecture Notes in Computer Science 6405, pp. 150-168.
An interpolating decision procedure for transitive relations with uninterpreted functions
Views & Downloads
If you are the owner of this record, you can report an update to it here: Report update to this record