AutomatedProverAPIExplanation

The MOBIUS Automated Prover API provides a generic programming interface to automated theorem provers. The initial version of this API was designed by MOBIUS partners working in tandem with leaders in the SMT-LIB community. The intention is to have some future variant of this API be the standard API for all automated theorem provers, at least within the SMT-LIB community.

The API was developed by performing an analysis of the core operations provides by all major automated provers: prover initialization and shutdown, hinting to a prover about resource utilization bounds (primarily, time and space), declaration of new theories (via axiomatic definitions), making and retracting assumptions (as part of, e.g., a background predicate of a theory), and checking the validity of formulae.

The initial version of this API was designed with a formal specification written in JML, and example implementations were provided in Java, C, and OCaml. Communication with theorem provers is supported via pipes/sockets, native methods, and an XML-RPC-based messaging interface. This API is now used by ESC/Java2 and the CVC3 prover, and interfaces with the Z3 and Simplify theorem provers as well (BT07).

Version: 1 Time: Fri Mar 28 17:36:00 2008 Author: dcochran (dcochran) IP: 193.1.132.32