Book section icon

Book section

An interpolating decision procedure for transitive relations with uninterpreted functions

Abstract:
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:
Published
Peer review status:
Peer reviewed
Version:
Accepted Manuscript

Actions


Access Document


Files:
Publisher copy:
10.1007/978-3-642-19237-1_15

Authors


More by this author
Institution:
University of Oxford
Oxford college:
Magdalen College
Department:
Mathematical,Physical & Life Sciences Division - Computing Laboratory
More by this author
Institution:
University of Oxford
Oxford college:
Magdalen College
Department:
Mathematical,Physical & Life Sciences Division - Computing Laboratory

Contributors

Role:
Editor
Role:
Editor
Role:
Editor
More from this funder
Funding agency for:
Georg Weissenbacher
Pages:
150-168
Publication date:
2009
DOI:
URN:
uuid:c46c14d2-aa3b-489e-b9a7-64cb9b0fd1d7
Local pid:
ora:4408

Terms of use


Stats


Views & Downloads


If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP