Skip to content

What is Mistaber?

Mistaber (Hebrew: מסתבר, "it stands to reason") is the first formal symbolic reasoning system for computational halacha. It encodes halachic rulings as logical propositions within a multi-world modal framework, enabling rigorous reasoning about disputes, uncertainties, and normative conclusions.

What Mistaber Does

Mistaber provides five core capabilities:

1. Query Halachic Status Across Traditions

Ask whether something is permitted or forbidden according to different halachic authorities.

# Query the status of fish with dairy according to different traditions
mistaber query "holds(issur(achiila, M, sakana), mechaber)" \
    --facts "mixture(m1). contains(m1, salmon). contains(m1, butter). food_type(salmon, dag). food_type(butter, chalav)."

# Result: Mechaber forbids due to sakana (health danger)
# But querying the Rema world shows it's permitted

2. Compare Rulings Between Authorities

Identify where poskim (halachic authorities) agree or disagree.

# Compare rulings on fish+dairy across all worlds
mistaber compare "holds(issur(achiila, M, X), W)" \
    --facts "is_dag_chalav_mixture(m1)."

Output shows the machloket (dispute): - Mechaber: issur(achiila, m1, sakana) - forbidden due to health concern - Rema: heter(achiila, m1) - permitted - GRA: heter(achiila, m1) - permitted - Ashkenazi worlds (ashk_mb, ashk_ah): inherit Rema's permission - Sefardi world (sefardi_yo): inherits Mechaber's prohibition

3. Trace Reasoning with Source Citations

Understand why a ruling holds, with references to primary sources.

mistaber explain "holds(issur(achiila, m1, d_oraita), mechaber)" \
    --facts "is_beheima_chalav_mixture(m1)."

Output includes the derivation tree: 

issur(achiila, m1, d_oraita) holds in mechaber because:
  ├── Rule: r_bb_beheima_achiila
  │   └── Makor: SA YD 87:1
  │   └── Madrega: d_oraita
  └── Condition: is_beheima_chalav_mixture(m1)
      ├── mixture_has_basar(m1, beheima)
      └── mixture_has_chalav(m1)

4. Handle Uncertainty Formally

Apply the correct safek (doubt) resolution based on normative level.

from mistaber.engine import HsrsEngine

engine = HsrsEngine(ontology_path="./mistaber/ontology")

# When food type is unknown, safek rules apply
result = engine.query_with_completeness(
    pattern="issur(achiila, item, X)",
    require_complete=False
)

# Result shows safek status and resolution:
# - Safek d'oraita l'chumra (Biblical doubt -> stringent)
# - Safek d'rabanan l'kula (Rabbinic doubt -> lenient)

5. Analyze Scenarios

Given a set of facts, derive all applicable conclusions.

mistaber analyze "mixture(m1). contains(m1, chicken). contains(m1, cream). \
              food_type(chicken, of). food_type(cream, chalav)." \
    --world ashk_mb

Output includes derived conclusions for the Ashkenazi Mishnah Berurah tradition: - issur(achiila, m1, d_rabanan) - eating forbidden rabbinically - heter(bishul, m1) - cooking permitted - heter(hanaah, m1) - benefit permitted

What Mistaber is NOT

Understanding what Mistaber is not is equally important:

Not a Posek (Halachic Decisor)

Mistaber does not issue halachic rulings. It is a reasoning tool that: - Encodes existing rulings from authoritative sources - Shows what different traditions hold - Identifies disputes and their sources - Does not replace rabbinic consultation

Not Text Search or Information Retrieval

Mistaber is not a search engine for halachic texts. It: - Does not search through sefarim (books) - Does not provide translations or commentaries - Works with formalized logical representations, not raw text

Not Machine Learning

Mistaber uses symbolic AI, not statistical learning. It: - Does not learn from examples - Does not make probabilistic predictions - Uses explicit logical rules derived from halachic sources - Provides deterministic, explainable reasoning

Not Complete

Mistaber currently covers a limited domain: - Yoreh Deah 87 (Basar Bechalav / Meat and Milk) - Seven halachic traditions (worlds) - Core commentators (Shach, Taz) - Expanding coverage is ongoing work

The Seven-World Model

Mistaber organizes halachic knowledge using Kripke semantics with seven worlds representing different traditions:

graph TD
    base["base<br/>(common ground)"]

    mechaber["mechaber<br/>(Sefardi)"]
    rema["rema<br/>(Ashkenaz)"]
    gra["gra<br/>(Vilna)"]

    sefardi_yo["sefardi_yo<br/>(Yalkut Yosef)"]
    ashk_mb["ashk_mb<br/>(Mishnah Berurah)"]
    ashk_ah["ashk_ah<br/>(Aruch Hashulchan)"]

    base --> mechaber
    base --> rema
    base --> gra

    mechaber --> sefardi_yo
    rema --> ashk_mb
    rema --> ashk_ah
    gra --> ashk_ah

World Descriptions

World Authority Tradition Inherits From
base Common ground Shulchan Aruch basics (root)
mechaber R' Yosef Karo Sefardi base
rema R' Moshe Isserles Ashkenazi base
gra Vilna Gaon Ashkenazi-Litvish base
ashk_mb Mishnah Berurah Ashkenazi-Litvish rema
ashk_ah Aruch Hashulchan Ashkenazi-Russian rema, gra
sefardi_yo Yalkut Yosef Sefardi-Edot HaMizrach mechaber

How Inheritance Works

Worlds inherit propositions from their parents via the accessible/2 relation:

% From kripke_rules.lp
holds(Prop, W_child) :-
    accessible(W_child, W_parent),
    holds(Prop, W_parent),
    not overridden(Prop, W_child).

A child world: 1. Inherits all propositions from its parent(s) 2. Can override specific propositions it disagrees with 3. Can add new propositions specific to its tradition

Example: The Rema overrides the Mechaber's sakana ruling on fish+dairy:

% From rema.lp
override(rema, sakana(M), no_sakana) :-
    is_dag_chalav_mixture(M).

asserts(rema, heter(achiila, M)) :-
    is_dag_chalav_mixture(M).

Core Technologies

Component Technology Purpose
Logic Engine Clingo (ASP) Answer Set Programming solver
World Semantics Kripke frames Modal logic for multi-tradition reasoning
Deontic Logic Custom extension Obligation, permission, prohibition
Uncertainty Safek calculus Formal doubt handling
Explanations xclingo2 Derivation tree generation
Interface Click (Python) Command-line interface

Answer Set Programming (ASP)

Mistaber uses ASP for non-monotonic reasoning, which is essential for halacha because: - Rules can have exceptions - Later authorities can override earlier ones - Default reasoning applies when specific rules don't

Example ASP rule from mechaber.lp:

% Rule: Beheima + Chalav - Eating forbidden d'oraita
rule(r_bb_beheima_achiila).
makor(r_bb_beheima_achiila, sa("yd:87:1")).
madrega(r_bb_beheima_achiila, d_oraita).
scope(r_bb_beheima_achiila, mechaber).

asserts(mechaber, issur(achiila, M, d_oraita)) :-
    is_beheima_chalav_mixture(M).

Key Predicates

The following predicates form the core vocabulary:

Status Predicates

Predicate Hebrew Meaning
issur(Action, Subject, Level) איסור Prohibition
heter(Action, Subject) היתר Permission
sakana(Subject) סכנה Health danger

World Predicates

Predicate Meaning
world(W) W is a valid world
accessible(W1, W2) W1 can access (inherits from) W2
asserts(W, Prop) W directly asserts proposition Prop
holds(Prop, W) Prop is true in world W
override(W, Prop, Reason) W overrides inherited Prop

Rule Metadata

Predicate Meaning
rule(R) R is a rule identifier
makor(R, Source) R cites Source
madrega(R, Level) R has normative level (d_oraita, d_rabanan, etc.)
scope(R, W) R is scoped to world W

Next Steps