A generalization of shostak’s method for combining decision procedures

Clark W. Barrett, David L. Dill, Aaron Stump

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 languageEnglish (US)
Title of host publicationFrontiers of Combining Systems - 4th International Workshop, FroCoS 2002, Proceedings
PublisherSpringer Verlag
Pages132-146
Number of pages15
Volume2309
ISBN (Print)3540433813, 9783540433811
StatePublished - 2002
Event4th International Workshop on Frontiers of Combining Systems, FroCoS 2002 - Santa Margherita Ligure, Italy
Duration: Apr 8 2002Apr 10 2002

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2309
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other4th International Workshop on Frontiers of Combining Systems, FroCoS 2002
CountryItaly
CitySanta Margherita Ligure
Period4/8/024/10/02

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Fingerprint Dive into the research topics of 'A generalization of shostak’s method for combining decision procedures'. Together they form a unique fingerprint.

Cite this