check_entailment
Determine whether SMT-LIB premises entail a conclusion by testing unsatisfiability of premises plus negated conclusion in Z3 and cvc5, returning solver verdicts and caveats.
Instructions
Check whether a conclusion is logically entailed by a set of premises, by asking whether (premises AND NOT conclusion) is unsatisfiable, cross-checked in both Z3 and cvc5.
YOU (the calling model) are responsible for translating the user's prose
question into declarations, premises, and conclusion. This server does
NOT interpret English — it only runs the SMT-LIB you hand it. Pass the
user's original wording in prose so the English and the formalization
travel together in the evidence trail.
Before presenting the verdict to the user as an answer about their original
English question, SHOW THEM THE FORMALIZATION (the declarations, premises,
and conclusion, or the assembled smtlib_script) and get their agreement
that it captures what they meant. A verdict from this tool is a fact about
the formalization, not directly about the user's English — whether the
formalization is a faithful translation of their intent is the user's call,
not yours.
Report exactly what the solvers returned. Do not upgrade "both solvers said
unsat under these bounds" into an unqualified "yes, this is true" — an
ENTAILMENT_HOLDS verdict is bounded-unsat relative to the premises and
declarations as written, not an unbounded proof about the world. Read the
caveats list and pass its contents along; each one names a specific way
the guarantee is weaker than it may sound (quantifiers, nonlinear
arithmetic, uninterpreted sorts, or a bounded check). If status comes back
DISAGREEMENT, that is the headline: tell the user the two solvers
returned different verdicts and that the result must not be trusted, do not
average or pick one to report.
declarations are full SMT-LIB forms, e.g. (declare-const x Int) or
(declare-fun key (String) String). premises and conclusion are bare
boolean terms, e.g. (> x 5) — this tool wraps each premise in (assert ...) for you (a premise that already starts with (assert is accepted
as-is, not double-wrapped).
Worked example (propositional modus ponens): declarations = ["(declare-const p Bool)", "(declare-const q Bool)"] premises = ["(=> p q)", "p"] conclusion = "q" -> entailment holds (both solvers report the negated-conclusion script is unsatisfiable).
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| logic | No | ||
| prose | No | ||
| premises | Yes | ||
| conclusion | Yes | ||
| timeout_ms | No | ||
| declarations | Yes |