### Abstract

Consider the problem of determining whether a quantifierfree formula φ is satisfiable in some first-order theory T. Shostak’s algorithm decides this problem for a certain class of theories with both interpreted and uninterpreted function symbols. We present two new algorithms based on Shostak’s method. The first is a simple subset of Shostak’s algorithm for the same class of theories but without uninterpreted function symbols. This simplified algorithm is easy to understand and prove correct, providing insight into how and why Shostak’s algorithm works. The simplified algorithm is then used as the foundation for a generalization of Shostak’s method based on a variation of the Nelson- Oppen method for combining theories.

Original language | English (US) |
---|---|

Title of host publication | Frontiers of Combining Systems - 4th International Workshop, FroCoS 2002, Proceedings |

Publisher | Springer Verlag |

Pages | 132-146 |

Number of pages | 15 |

Volume | 2309 |

ISBN (Print) | 3540433813, 9783540433811 |

State | Published - 2002 |

Event | 4th International Workshop on Frontiers of Combining Systems, FroCoS 2002 - Santa Margherita Ligure, Italy Duration: Apr 8 2002 → Apr 10 2002 |

### Publication series

Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|

Volume | 2309 |

ISSN (Print) | 03029743 |

ISSN (Electronic) | 16113349 |

### Other

Other | 4th International Workshop on Frontiers of Combining Systems, FroCoS 2002 |
---|---|

Country | Italy |

City | Santa Margherita Ligure |

Period | 4/8/02 → 4/10/02 |

### Fingerprint

### ASJC Scopus subject areas

- Computer Science(all)
- Theoretical Computer Science

### Cite this

*Frontiers of Combining Systems - 4th International Workshop, FroCoS 2002, Proceedings*(Vol. 2309, pp. 132-146). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2309). Springer Verlag.

**A generalization of shostak’s method for combining decision procedures.** / Barrett, Clark W.; Dill, David L.; Stump, Aaron.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

*Frontiers of Combining Systems - 4th International Workshop, FroCoS 2002, Proceedings.*vol. 2309, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2309, Springer Verlag, pp. 132-146, 4th International Workshop on Frontiers of Combining Systems, FroCoS 2002, Santa Margherita Ligure, Italy, 4/8/02.

}

TY - GEN

T1 - A generalization of shostak’s method for combining decision procedures

AU - Barrett, Clark W.

AU - Dill, David L.

AU - Stump, Aaron

PY - 2002

Y1 - 2002

N2 - Consider the problem of determining whether a quantifierfree formula φ is satisfiable in some first-order theory T. Shostak’s algorithm decides this problem for a certain class of theories with both interpreted and uninterpreted function symbols. We present two new algorithms based on Shostak’s method. The first is a simple subset of Shostak’s algorithm for the same class of theories but without uninterpreted function symbols. This simplified algorithm is easy to understand and prove correct, providing insight into how and why Shostak’s algorithm works. The simplified algorithm is then used as the foundation for a generalization of Shostak’s method based on a variation of the Nelson- Oppen method for combining theories.

AB - Consider the problem of determining whether a quantifierfree formula φ is satisfiable in some first-order theory T. Shostak’s algorithm decides this problem for a certain class of theories with both interpreted and uninterpreted function symbols. We present two new algorithms based on Shostak’s method. The first is a simple subset of Shostak’s algorithm for the same class of theories but without uninterpreted function symbols. This simplified algorithm is easy to understand and prove correct, providing insight into how and why Shostak’s algorithm works. The simplified algorithm is then used as the foundation for a generalization of Shostak’s method based on a variation of the Nelson- Oppen method for combining theories.

UR - http://www.scopus.com/inward/record.url?scp=84947902670&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84947902670&partnerID=8YFLogxK

M3 - Conference contribution

SN - 3540433813

SN - 9783540433811

VL - 2309

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 132

EP - 146

BT - Frontiers of Combining Systems - 4th International Workshop, FroCoS 2002, Proceedings

PB - Springer Verlag

ER -