LogicUS.FOL.TPTP

The module translates formulas to the TPTP syntax (FOF), the input language of most automated theorem provers and model finders for first order logic, such as E, Vampire or the online service SystemOnTPTP. It is meant for problems too big for the didactic algorithms of the library: the problem is sent to an external prover and its answer (an SZS status) is read back.

Problems

type alias TPTPProblem =

{ input : String

, symbols : Dict String Ident

}

A problem in TPTP syntax. input is the text to give to the prover and symbols maps each TPTP symbol back to the identifier of the original formulas (TPTP requires functors in lower case, so P becomes p).

tptpProblem :

{ axioms : SetFOL

, conjecture : Maybe FormulaFOL

}

-> TPTPProblem

It builds a TPTP problem from a set of axioms and, optionally, a conjecture.

With a conjecture, provers try to prove that it follows from the axioms (SZS status Theorem) or find a counter-model (CounterSatisfiable).
Without it, they decide whether the axioms are satisfiable (Satisfiable/Unsatisfiable).

tptpProblem { axioms = [ ffolRead "!A[X](P(X) -> Q(X))", ffolRead "P(a)" ], conjecture = Just (ffolRead "Q(a)") }
    |> .input
    == "fof(ax1, axiom, ![X]: (p(X) => q(X))).\nfof(ax2, axiom, p(a)).\nfof(goal, conjecture, q(a)).\n"

ffolToTPTP : FormulaFOL -> String

It translates a single formula to TPTP syntax (symbols renamed as in tptpProblem).

ffolToTPTP (ffolRead "!A[X] !E[Y] (s(X, Y) = e)") == "![X]: ?[Y]: (s(X, Y) = e)"

Answers

szsStatus : String -> Maybe String

It extracts the SZS status from the output of a prover (e.g. Theorem, CounterSatisfiable, Unsatisfiable, Satisfiable, Timeout, GaveUp), if there is one.

szsStatus "...\n# SZS status Theorem for problem.p\n..." == Just "Theorem"

logicUSLIB/logicus-fol/3.2.1

LogicUS.FOL.TPTP

Problems

Answers

Modules