An interpolating decision procedure for transitive relations with uninterpreted functions
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 bit-level accurate verification. We describe ou...
| Những tác giả chính: | , |
|---|---|
| Tác giả khác: | |
| Định dạng: | Book section |
| Ngôn ngữ: | English |
| Được phát hành: |
2009
|
| Những chủ đề: |
Search Result 1
An Interpolating Decision Procedure for Transitive Relations with Uninterpreted Functions
Được phát hành 2010
Conference item