Sciweavers

CADE
2004
Springer

The ICS Decision Procedures for Embedded Deduction

14 years 3 months ago
The ICS Decision Procedures for Embedded Deduction
contexts such as construction of abstractions, speed may be favored over completeness, so that undecidable theories (e.g., nonlinear integer arithmetic) and those whose decision problems are often considered infeasible in practice (e.g., real closed fields) should not be ruled out completely. Most problems that arise in practice involve combinations of theories: the question whether f(cons(4?car(x)-2?f(cdr(x)), y)) = f(cons(6?cdr(x), y)) follows from 2 ? car(x) - 3 ? cdr(x) = f(cdr(x)), for example, requires simultaneously the theories of uninterpreted functions, linear arithmetic, and lists. The ground (i.e., quantifier-free) fragment of many combinations is decidable when the fully quantified combination is not, and practical experience indicates that automation of the ground case is adequate for most applications. Practical experience also suggests several other desiderata for an effective e service. Some applications (e.g., construction of abstractions) invoke their deductive servi...
Leonardo Mendonça de Moura, Sam Owre, Haral
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2004
Where CADE
Authors Leonardo Mendonça de Moura, Sam Owre, Harald Rueß, John M. Rushby, Natarajan Shankar
Comments (0)