Introducing A New Scientific Domain — Computational Halacha. For centuries, scholars have studied Jewish law (halacha) through close reading of texts, legal reasoning, and responsa literature. Computer scientists, meanwhile, have built formal systems for regulatory compliance, medical diagnosis, and contract verification. These two worlds have never properly converged — until now.

We are introducing computational halacha as a rigorous scientific domain at the intersection of symbolic AI, legal philosophy, and traditional scholarship. And we built Mistaber (Hebrew: "it stands to reason") — the first system to demonstrate that the full complexity of multi-authority halachic reasoning can be captured formally, verified mathematically, and queried computationally.

The full system — source code, ontology, and test suite — is open source on GitHub. Visit mistaber.ai to learn more.

Why Halacha Demands a New Scientific Approach

Most computational law systems assume a single authoritative source: one legislature, one set of rules, one answer. Halacha has operated for over two millennia with multiple competing authorities whose rulings are all simultaneously binding — on different communities. The Shulchan Aruch codifies Sephardic practice; the Rema documents Ashkenazic variations; the Shach, Taz, Vilna Gaon, and later authorities each add interpretive layers that modify, restrict, or expand earlier rulings.

This isn't a defect. The Talmudic principle of elu v'elu divrei Elokim chayim — "these and those are the words of the Living God" (Eruvin 13b) — establishes that multiple conflicting opinions can simultaneously possess legal validity. Any computational system that flattens this plurality into a single answer has misrepresented the tradition before producing its first result.

Meanwhile, large language models (LLMs) with retrieval-augmented generation might seem promising, but they fail on every requirement for rigorous normative reasoning: they are non-deterministic (the same query yields different answers), lack persistent world models, cannot perform negation-as-failure reasoning ("if not prohibited, permitted"), and cannot guarantee that cited sources actually exist.

The Theoretical Foundations

Mistaber rests on four formal pillars:

Kripke Semantics. Originally developed for modal logic, Kripke possible-world semantics provides a natural model for multi-authority reasoning. Each halachic authority (posek) becomes a possible world. The accessibility relation captures "inherits from" — the Rema inherits shared rulings from a common base, but can override specific positions. Truth is local: a ruling holds in a world if explicitly asserted there or inherited from a parent world without being overridden. Mistaber defines this as a Kripke model M = (W, R, V) with 7 worlds arranged in a DAG across three tiers — common ground (base), classical authorities (Mechaber, Rema, Gra), and modern traditions (Sefardi-YO, Ashk-MB, Ashk-AH) — including diamond inheritance where a world inherits from multiple parents.

Deontic Logic. The standard deontic operators — O(p) obligation, P(p) permission, F(p) prohibition — are extended with graded obligations. Each norm carries a madrega level: d'oraita (biblical), d'rabanan (rabbinic), minhag (custom), chumra (voluntary stringency). Rules are conditional, and later authorities can override earlier rulings through defeasibility.

Answer Set Programming. ASP with stable model semantics provides the computational engine. Negation-as-failure gives us the Closed World Assumption — mirroring the halachic principle kol davar shelo ne'esar, mutar ("anything not forbidden is permitted"). Non-monotonicity enables later authorities to override earlier ones. The entire system runs on Clingo, the University of Potsdam's ASP solver.

Formal Ontology. Hundreds of predicates organized across three domains — physical (substances, vessels, mixtures, temperatures), normative (rules, worlds, statuses, sources), and classification (categories, hierarchies) — with typed sorts and explicit CWA/OWA designation per predicate. The ontology distinguishes what can be assumed false when absent (prohibitions, categories) from what remains genuinely unknown (unencoded authorities, historical facts).

The system carries proven formal guarantees: soundness (every derivation is semantically entailed), completeness (every entailed proposition is derivable), termination (all queries complete), decidability (query answering is in P for fixed schema), confluence (different inheritance paths never yield contradictions within a world), and provenance preservation (every derived ruling maintains a complete chain of halachic sources).

HLL: A Language for Encoding Halacha

We designed HLL (Halachic Logic Language), a domain-specific language that compiles to ASP. HLL enforces scholarly discipline by requiring every rule to carry metadata:

@world(mechaber)
@rule(basar_b_chalav)
@makor([sa("yd:87:1")])
@madrega(d_oraita)

asserts(mechaber, issur(achiila, M, d_oraita)) :-
    is_mixture(M),
    has_component(M, X), isa(X, beheima),
    has_component(M, Y), isa(Y, chalav).

Every @rule requires a @makor (source citation) and @madrega (normative level). The compiler pipeline — parser, normalizer, type checker, ASP emitter — validates sort assignments, predicate arities, and world references before generating Clingo-compatible output. Surface syntax expansions keep rules readable: assur(X, A) desugars to has_status(X, assur, A), isa(X, C) becomes food_instance(X, C).

Beyond core rules, Mistaber includes two specialized reasoning layers:

• Safek Calculus: A formal treatment of doubt. When facts relevant to a ruling are unknown (under Open World Assumption), the system generates a safek/5 predicate capturing the uncertainty's full context. Resolution follows halachic meta-rules: biblical doubt is resolved stringently (safek d'oraita l'chumra), rabbinic doubt is resolved leniently (safek d'rabanan l'kula), and double-doubt (sfek sfeika) may permit even biblical matters.
• Interpretation Layer: Commentators like the Shach and Taz don't issue independent rulings — they interpret existing authorities. Three predicates (adds_condition, removes_condition, expands_scope) formalize how commentators modify rules at fine granularity, without constructing entirely new worlds. Users can query "Mechaber according to Shach" to see how a commentator's reading affects practical rulings.

The Mistaber IDE: A Semi-Automated Encoding Pipeline

Encoding halacha is not a mechanical translation — it requires interpretive decisions at every step. We built a full VS Code-style IDE with a five-phase semi-automated pipeline, each phase gated by human approval:

1. Corpus Preparation — Source texts are fetched from Sefaria and organized with a provenance chain documenting every retrieval.
2. HLL Encoding — A Claude-powered AI agent drafts formal rules from source texts, but every encoding decision is human-reviewed. The dashboard displays a complexity radar (machloket depth, cross-references, novel predicates) to flag difficult encodings.
3. Validation — The compiler builds HLL to ASP, the test runner executes .hll scenario files and pytest suites, and xclingo generates derivation traces for proof inspection.
4. Review — Domain experts verify encoding accuracy through interactive checklists.
5. Commit — Approved encodings are archived with full provenance and versioned via git.

The IDE features an interactive D3 force graph for exploring ontology structure (sorts, predicates, worlds, and their relationships), a coverage heatmap tracking encoding progress across 200+ seifim, an integrated query executor for running Clingo queries live, a proof tree viewer showing xclingo derivation chains from conclusion back to source, and a live terminal connected to each encoding session.

The encoding process is itself a form of scholarly contribution. The encoder must decide which features of a physical situation are legally decisive, how to map halachic concepts to formal predicates, and which distinctions matter. We treat this explicitly through Deleuze's legal philosophy — every formalization is an act of "specifying the event", and different encoders reading the same texts might produce different but equally defensible formalizations. The five-phase pipeline ensures these decisions are documented, reviewed, and versioned — treating formalization as scholarship subject to peer review, not automated extraction.

What Mistaber Can Do Today

The current implementation encodes Yoreh De'ah 87 of the Shulchan Aruch — the laws of basar b'chalav (meat and dairy) — covering dozens of distinct halachic rules across 7 Kripke worlds and 2 commentators (Shach and Taz). A comprehensive test suite validates encoding correctness across all worlds, with all queries completing in under 100ms.

The system handles four classes of reasoning:

• Universal agreement — Beef + milk: d'oraita prohibition inherited faithfully across all 7 worlds.
• Machloket (disagreement) — Fish + dairy: the Mechaber prohibits due to sakana (health danger); the Rema permits; Sefardi worlds inherit the prohibition, Ashkenazi worlds inherit the permission. Both positions coexist with full provenance.
• Safek resolution — Uncertain ingredients resolved stringently for biblical matters, leniently for rabbinic, with world-specific policies (Gra and Mishnah Berurah traditions adopt stricter stances even for rabbinic doubts).
• Interpretation overlay — The Shach's condition narrows the Mechaber's fish-dairy ruling to cooked combinations only, without creating a new world.

Every ruling carries a complete provenance chain — from derived conclusion back through inheritance paths to the original source citation in the Shulchan Aruch, commentaries, or Talmud.

A New Scientific Domain

Computational halacha is not just about building a better search tool. It establishes a methodology for formalizing any legal system where legitimate disagreement is structural — not exceptional.

Islamic fiqh has competing schools (madhahib) with analogous inheritance structures. Canon law has layered authorities from papal decrees to local ordinances. Indigenous legal traditions feature overlapping customary authorities. The same Kripke-based framework applies wherever multiple authoritative voices coexist.

More fundamentally, Mistaber demonstrates that symbolic AI and formal methods have something genuine to offer legal scholarship — not as a replacement for human judgment, but as a verification substrate. It formalizes the current state of halachic positions. It does not model the generative process by which those positions were produced from encounter with cases. The system's value lies in supporting — rather than replacing — the creative work of halachic reasoning.

The roadmap ahead includes expanding to additional simanim (Yoreh De'ah 93–111 on mixtures), formalizing Rishonim (medieval commentators like Rambam and Tosafot) to trace the evolution of halachic concepts, adding temporal reasoning for time-dependent halachot, and building a natural language interface that combines LLM query translation with symbolic verification.

We believe this is the beginning of a conversation between two ancient disciplines — formal logic and Torah scholarship — that have more in common than either has recognized.

*Mistaber is developed by Levi Dubrovin and Asher Crispe at BrainyBlaze Dynamics Inc.*