The module connects the library with Prover9 and Mace4: Prover9 searches for proofs in first order logic with equality, and Mace4 searches for finite models and counter-models.
The functions build the input file for both programs and read their answers back. Mace4 models are returned as
L_Structure Int, so they can be shown and checked with the rest of the library (e.g. ffolValuation).
Running the programs is up to the application (a server, a WebAssembly build, a local installation...).
It builds the input file from a list of assumptions and a list of goals. Prover9 tries to prove the goals from the assumptions; Mace4 searches for a model of the assumptions that falsifies the goals (a counter-model). With no goals, Mace4 simply searches for models of the assumptions.
p9m4Problem { assumptions = [ ffolRead "!A[X](P(X) -> Q(X))", ffolRead "P(a)" ], goals = [ ffolRead "Q(a)" ] }
|> .input
== "formulas(assumptions).\n(all X (P(X) -> Q(X))).\nP(a).\nend_of_list.\n\nformulas(goals).\nQ(a).\nend_of_list.\n"It reads the result of a Prover9 run: Just True if a proof was found, Just False if the search ended without
one (SEARCH FAILED, which does not mean that the goal is false), and Nothing if the output says neither (e.g. it
was stopped by a time limit).
It extracts the models of a Mace4 output (the interpretation(...) blocks in its standard format) as structures
for the symbols of the problem. Note that Mace4 only searches domains of size 2 or more. The elements of the universe are 0, 1, ..., n-1. Mace4 leaves out the symbols that
its simplifications made irrelevant; they get an arbitrary interpretation (constant 0, empty relations), which does
not change the truth of the problem's formulas.
mace4Models problem mace4Output
|> List.map (ffolValuation (ffolRead "Q(a)"))
== [ Just False ]
An input file for Prover9 and Mace4.
symbolsmaps the names used in the file back to the identifiers of the original formulas.