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

• Type: Conference
• Year: 2004
• Where: CADE
• Authors: Leonardo Mendonça de Moura, Sam Owre, Harald Rueß, John M. Rushby, Natarajan Shankar
• Keywords: Automated Reasoning, CADE 2004, Generation This Work, Nsf Grants Ccr-itr-0326540, Rich Application Programming