Module api

source code

Interfaces for theorem provers and model builders.

Prover is a standard interface for a theorem prover which tries to prove a goal from a list of assumptions.

ModelBuilder is a standard interface for a model builder. Given just a set of assumptions. the model builder tries to build a model for the assumptions. Given a set of assumptions and a goal G, the model builder tries to find a counter-model, in the sense of a model that will satisfy the assumptions plus the negation of G.