The Interface is the Message

---

Authors

Harald Rueß and Natarajan Shankar

Abstract

A decision procedure for the satisfiability (validity) problem is a total predicate on a class of formulas that determines whether a given formula is satisfiable. It might seem that a simple binary interface for a decision procedure as a function that takes a formula and returns $\mathit{Yes}$ or $\mathit{No}$ according to whether the formula is satisfiable, would be adequate. On the contrary, we have observed that decision procedures need rich interfaces in order to be deployed most effectively. Decision procedures are frequently used in an online manner so that atomic formulas are added to a context incrementally, and claims are tested against the context. The application programmer interface (API) should include operations for asserting and retracting information, testing claims, and for creating, deleting, and browsing contexts. The decision procedures might need to exchange information with other inference procedures such as a rewriter, typechecker, or an external constraint solver. We discuss the basic issues in the design of modular interfaces for decision procedures that allow a rich range of interactions with other decision procedures and external applications. Our experience includes the integration of ground decision procedures, BDD packages, model checkers, and rewriters into PVS, and with the integration of ground decision procedures with SAT solving. The discussion here is mostly centered around the design of the API for ICS.

gzipped postscript

BibTeX Entry

@inproceedings{RuessShankar:QPQ03,
  TITLE = {The Interface is the Message}
  AUTHOR = {Harald Rue{\ss} and Natarajan Shankar},
  BOOKTITLE = {Proceedings of the First QPQ Workshop on Deductive Software Components},
  YEAR = {2003},
  MONTH = {July}, 
  ADDRESS = {Miami, Floria},
  URL = {http://www.qpq.org} 
}

---

Harald Ruess: ruess@csl.sri.com