Interface for doing prover queries
Author: rgrig, based on work of mjm, further revised by David Cok
This package is responsible for building prover queries and for querying the prover(s). As a small bonus, there is runtime check that the queries are well-sorted (or typed, whatever you prefer, but I shall use `sorted' to not confuse it with Java types).
The clients of this package should get a Prover instance, build queries using the Builder provided by the Prover, and use the Prover to ask if queries are theorems or not.
(NOTE: A formula is a term whose sort is BOOL.)
There are three types of terms. The most general is term_id(a1, ..., an), that is, it has an identifier, gets applied to a number (possibly 0) of arguments and returns a value. It's sort is t1 x ... x tn -> t. A constant is just the case n=0. Before using a term it has to be registered, that is, you have to tell the builder that term_id: t1 x ... x tn -> t is going to be used. Surely, having to register the constants "1", "2", "41" individually would be unpleasant. That's why the second type of term is a facility that makes it easy to use such constants. Informally, you register const_int : JavaInteger -> ProverInt. Finally, for associative-commutative operators it is convenient to allow a variable number of arguments. That is the third type of term.
The Prover interface is also small. One can push/pop assumptions, make queries, and optionally inquire about details of the query answer. (The simple answer is a boolean, or an exception.)