Mistaber System Overview¶

Executive Summary¶

Mistaber (מסתבר - "It stands to reason") is the first formal symbolic reasoning system for computational halacha (Jewish religious law). It combines:

HLL (Halachic Logic Language): A domain-specific language for writing halachic rules
ASP Backend: Answer Set Programming via Clingo solver
Kripke Semantics: Multi-world reasoning for representing different halachic authorities
Comprehensive Ontology: Type system, foundational rules, and world definitions

The system translates human-readable halachic rules into formal logic, enabling automated reasoning about complex scenarios while preserving the structure of halachic discourse.

System Architecture¶

flowchart TB
    subgraph USER["USER LAYER"]
        hll["HLL Source Code<br/>directives, facts, rules"]
    end

    subgraph COMPILER["COMPILER PIPELINE"]
        parser["Parser (Lark)"]
        norm["Normalizer<br/>Surface→Canonical"]
        tc["TypeChecker<br/>Registry Validation"]
        emit["Emitter<br/>ASP Generation"]
        parser --> norm --> tc --> emit
    end

    subgraph ENGINE["ENGINE LAYER"]
        hsrs["HsrsEngine<br/>• query(pattern)<br/>• ask(atom)<br/>• compare(pattern, worlds)<br/>• analyze(scenario)<br/>• explain(atom)"]
    end

    subgraph LOGIC["LOGIC LAYER"]
        schema["Schema<br/>sorts.lp | constraints.lp"]
        base_ont["Base Ontology<br/>substance.lp | madrega.lp"]
        worlds["World Defs<br/>base.lp | mechaber.lp<br/>rema.lp | gra.lp"]
        engine_rules["Engine Rules<br/>priorities.lp | safek.lp"]
        kripke["kripke_rules.lp<br/>Truth propagation"]
    end

    subgraph SOLVER["SOLVER LAYER"]
        clingo["Clingo ASP Engine<br/>+ asprin optimization"]
    end

    subgraph RESULTS["RESULTS LAYER"]
        output["Forbidden/Permitted • Machloket<br/>Safek resolution • Source traceability"]
    end

    USER --> COMPILER
    COMPILER --> ENGINE
    ENGINE --> LOGIC
    LOGIC --> SOLVER
    SOLVER --> RESULTS

Core Components¶

1. HLL (Halachic Logic Language)¶

Location: mistaber/dsl/grammar.lark

A domain-specific language designed for halachic reasoning:

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

% Facts
is_food(beef).
food_type(beef, beheima).

% Rules - asserts into the world
asserts(mechaber, issur(achiila, M, d_oraita)) :-
    is_beheima_chalav_mixture(M).

2. HsrsEngine¶

Location: mistaber/engine/engine.py

The main interface for halachic reasoning, providing:

Method	Purpose
`ask(atom)`	Boolean query - does atom hold?
`query(pattern)`	Get all bindings for pattern
`compare(pattern, worlds)`	Compare results across worlds
`analyze(scenario, world)`	Push-mode scenario analysis
`explain(atom)`	Generate derivation explanation
`query_preferred(pattern)`	asprin-optimized query
`check_completeness(query, facts)`	OWA completeness checking

3. Kripke World System¶

Location: mistaber/ontology/worlds/

Seven halachic worlds forming a directed acyclic graph:

graph TD
    base --> mechaber
    base --> rema
    base --> gra
    mechaber --> sefardi_yo
    rema --> ashk_mb
    rema --> ashk_ah
    gra --> ashk_ah

Note: ashk_ah inherits from both rema AND gra (multiple inheritance)

4. Predicate Registry¶

Location: mistaber/dsl/vocabulary/base.yaml

Canonical specification of all valid predicates: - 69 predicates across multiple domains - 29 sorts (types) - 12 enumeration categories - CWA/OWA classification for each predicate

5. Ontology¶

Location: mistaber/ontology/

ontology/
├── schema/           # Type system
│   ├── sorts.lp          # Sort declarations
│   ├── constraints.lp    # Integrity constraints
│   └── disjointness.lp   # Mutual exclusivity
├── base/             # Foundational rules
│   ├── substance.lp      # Food properties
│   ├── madrega.lp        # Obligation levels
│   ├── issur_types.lp    # Prohibition types
│   ├── status.lp         # Status modalities
│   ├── shiur.lp          # Measurements
│   ├── temporal.lp       # Time-based reasoning
│   └── context.lp        # Contextual rules
├── worlds/           # Halachic authority worlds
│   ├── base.lp           # Common ground
│   ├── mechaber.lp       # Shulchan Aruch
│   ├── rema.lp           # Ashkenazi glosses
│   ├── gra.lp            # Vilna Gaon
│   ├── ashk_mb.lp        # Mishnah Berurah
│   ├── ashk_ah.lp        # Aruch Hashulchan
│   ├── sefardi_yo.lp     # Yalkut Yosef
│   └── kripke_rules.lp   # Truth propagation
└── extensions/       # User extensions
    └── README.md         # Extension protocol

Key Design Decisions¶

1. Kripke Semantics for Multi-World Reasoning¶

Each halachic authority is a "possible world" with: - Local assertions via asserts(World, Proposition) - Inheritance via accessible(Child, Parent) - Override mechanism via override(World, Prop, Replacement)

Truth propagates from parent to child unless explicitly overridden.

2. Closed World vs. Open World Assumption¶

CWA Predicates (Closed World Assumption): - Facts must be explicitly stated - Used for: classifications, structural data - Examples: is_food, food_type, madrega

OWA Predicates (Open World Assumption): - Absence doesn't imply falsity - Used for: derived conclusions - Examples: permitted, forbidden, safek

3. Mandatory Source Attribution¶

Every normative rule requires @makor directive:

@makor([sa("YD:87:1"), rambam("Maachalot Asurot 9:1")])
asserts(W, issur(...)) :- ...

Rationale: Ensures traceability to halachic sources

4. Interpretation Layer¶

Commentators (Shach, Taz, Pri Megadim) are NOT separate worlds. They are interpretation functions that modify rule conditions WITHIN a world:

commentator(shach).
interprets(shach, mechaber).
adds_condition(shach, r_some_rule, extra_condition).

5. Hierarchical Context System¶

ctx_shaat_hadchak (most lenient)
    ↓
ctx_hefsed (financial loss)
    ↓
ctx_normal (default, most strict)

What's permitted in strict context remains permitted in lenient contexts.

6. Madrega (Obligation Level) Ordering¶

d_oraita (Biblical) - strongest
    ↓
d_rabanan (Rabbinic)
    ↓
minhag (Custom)
    ↓
chumra (Stringency) - weakest

Used for conflict resolution and safek handling.

Usage Example¶

from mistaber.engine import HsrsEngine
from pathlib import Path

# 1. Initialize engine
engine = HsrsEngine(
    ontology_path=Path("mistaber/ontology"),
    default_world="base"
)

# 2. Configure for specific tradition
engine.configure(
    world="rema",
    safek_resolution="madrega",
    context="lechatchila"
)

# 3. Query - Is fish+dairy forbidden?
results = engine.compare(
    pattern="holds(issur(achiila, M, Madrega), W)",
    worlds=["mechaber", "rema"]
)
# mechaber: issur due to sakana
# rema: no issur (permitted)

# 4. Analyze a specific scenario
analysis = engine.analyze("""
    mixture(fish_cream).
    contains(fish_cream, salmon).
    contains(fish_cream, cream).
    food_type(salmon, dag).
    food_type(cream, chalav).
""", world="rema")

# 5. Get explanation
explanation = engine.explain("heter(achiila, fish_cream)", world="rema")
print(explanation["tree"])

Test Coverage¶

Category	Tests	Description
DSL	117	Parser, type checker, normalizer, emitter, compiler
Ontology	18	Schema validation, disjointness, inheritance
Engine	25	Query modes, world comparison, completeness
Integration	14	Gold scenario, multi-world, context sensitivity
Total	174	Complete system validation

Extension Points¶

New Predicates: Add to base.yaml registry
New Sorts: Add to sorts section of registry
New Rules: Add to ontology base files
New Surface Syntax: Extend normalizer mappings
New Directives: Extend grammar and transformer
New Worlds: Add .lp file in ontology/worlds/
New Commentators: Add to interpretations.lp

See Extension Protocol for detailed instructions.