purescript-baskerville-mycroft

The SMT-backed oracle for Baskerville: Baskerville's ⊨ seam extended past enumerable world spaces. The claim universe stays finite; an SMT solver (mycroft) replaces world enumeration; unsat cores answer "which observations force this claim?"

Baskerville.Conformance.Smt mirrors the counting oracle in Baskerville.Conformance one instrument for one — entailed, unsound, gap, explainOr — each claim asked with a single query inside a push/pop scope, plus one the counting oracle can't offer: whyEntailed, the unsat core over the named observations (the ⊨-side twin of ⊢'s axiomsBehind).

• baskerville-core — the inference kernel and the conformance seam
• mycroft — the SMT solver wrapper (needs a z3 binary on PATH at runtime)

spago build
spago test    # requires z3 installed