Scientific Contributions¶

Mistaber introduces eight novel scientific contributions to the fields of computational law, knowledge representation, and Jewish studies.

1. Kripke Semantics for Halacha¶

The Innovation¶

Mistaber applies Kripke semantics (modal logic with possible worlds) to model halachic disagreements. Each halachic authority or tradition is represented as a "possible world" where different propositions may hold true.

Why It Matters¶

Traditional databases model data as either true or false. But in halacha, the same question can have different answers depending on which authority you follow. A proposition like "fish with dairy is forbidden" is true in the Mechaber's world but false in the Rema's world.

Implementation¶

% World declarations (from worlds/*.lp)
world(base).
world(mechaber).
world(rema).

% Accessibility relations define inheritance
accessible(mechaber, base).
accessible(rema, base).

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

% Override mechanism
overridden(Prop, W) :-
    override(W, Prop, _).

The Seven-World Structure¶

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

Each world inherits from its parent(s) and can override specific rulings:

World	Authority	Key Characteristic
`base`	Common ground	Shared axioms
`mechaber`	R' Yosef Karo	Sefardi rulings, sakana for fish+dairy
`rema`	R' Moshe Isserles	Ashkenazi rulings, permits fish+dairy
`gra`	Vilna Gaon	Independent Ashkenazi, strict on safek
`ashk_mb`	Mishnah Berurah	Litvish, strict on d'rabanan doubts
`ashk_ah`	Aruch Hashulchan	Multiple inheritance (rema + gra)
`sefardi_yo`	Yalkut Yosef	Modern Sefardi, follows Mechaber

2. Deontic Logic Extension¶

The Innovation¶

Mistaber extends standard deontic logic (the logic of obligation and permission) with halacha-specific modalities and their interactions.

Standard Deontic Operators¶

Operator	Meaning
O(p)	Obligatory that p
P(p)	Permitted that p
F(p)	Forbidden that p

Halachic Extensions¶

Mistaber adds:

Status	Hebrew	Meaning	Formal
`assur`	אסור	Prohibited	F(action)
`mutar`	מותר	Permitted	P(action)
`chiyuv`	חיוב	Obligatory	O(action)
`reshut`	רשות	Optional	P(action) ∧ P(¬action)
`mitzvah`	מצוה	Meritorious	Good(action)
`sakanah`	סכנה	Dangerous	Danger(action)

Implementation¶

% Status modalities (from schema/sorts.lp)
status(assur).
status(mutar).
status(chiyuv).
status(reshut).
status(mitzvah).
status(sakanah).

% Issur with action type and level
asserts(mechaber, issur(achiila, M, d_oraita)) :-
    is_beheima_chalav_mixture(M).

% Heter (permission) explicitly granted
asserts(rema, heter(achiila, M)) :-
    is_dag_chalav_mixture(M).

% Sakana is a distinct modality (not just another issur)
asserts(mechaber, sakana(M)) :-
    is_dag_chalav_mixture(M).

Constraint: Consistency¶

% Cannot be both forbidden and permitted in same context
:- forbidden(W, A, F, C), permitted(W, A, F, C).

3. Formal Upper Ontology¶

The Innovation¶

Mistaber provides a rigorous upper ontology for halachic concepts, with formally defined sorts, predicates, and constraints.

Sort Hierarchy¶

# Physical Domain
- food              # Physical food items
- vessel            # Cooking vessels (kelim)
- mixture           # Combined substances
- action            # Physical actions
- agent             # Actors

# Normative Domain
- world             # Possible worlds
- rule_id           # Rule identifiers
- source_ref        # Citations
- posek             # Authorities

# Classification Domain (Enumerated)
- food_category     # basar, chalav, parve...
- action_type       # achiila, bishul, hanaah
- madrega_type      # d_oraita, d_rabanan, minhag, chumra
- temp_status       # tzonen, cham, roteiach
- kli_status        # kli_rishon, kli_sheni, kli_shlishi

Food Category Hierarchy¶

% From schema/sorts.lp
food_category(maakhal).    % Generic food
food_category(basar).      % Meat
food_category(chalav).     % Dairy
food_category(parve).      % Neutral

% Basar subcategories
subcategory(beheima, basar).  % Domesticated animal
subcategory(chaya, basar).    % Wild animal
subcategory(of, basar).       % Poultry
subcategory(dag, basar).      % Fish

Disjointness Constraints¶

% From schema/disjointness.lp
% Food cannot be both meat and dairy
:- food_type(F, basar), food_type(F, chalav).

% Cannot be multiple basar subtypes
:- food_type(F, beheima), food_type(F, of).

4. Multi-World Inheritance¶

The Innovation¶

Mistaber implements a directed acyclic graph (DAG) of worlds with non-monotonic inheritance. Child worlds can selectively override parent rulings while inheriting everything else.

Inheritance Mechanism¶

% From kripke_rules.lp

% Local assertions hold in their world
holds(Prop, W) :-
    asserts(W, Prop),
    world(W).

% Inherit from accessible (parent) worlds
holds(Prop, W_child) :-
    accessible(W_child, W_parent),
    holds(Prop, W_parent),
    not overridden(Prop, W_child).

% Override mechanism
overridden(Prop, W) :-
    override(W, Prop, _).

Multiple Inheritance Example¶

The Aruch Hashulchan (ashk_ah) inherits from both Rema and GRA:

% From ashk_ah.lp
world(ashk_ah).
accessible(ashk_ah, rema).
accessible(ashk_ah, gra).

When a proposition holds in both parents, the child inherits it. When parents disagree, the child must either: 1. Inherit from one (non-deterministic without explicit choice) 2. Explicitly override with its own ruling

Override Example¶

The Rema overrides the Mechaber's sakana ruling:

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

override(rema, issur(achiila, M, sakana), permitted) :-
    is_dag_chalav_mixture(M).

% Explicitly assert the opposite
asserts(rema, heter(achiila, M)) :-
    is_dag_chalav_mixture(M).

5. ASP for Halacha¶

The Innovation¶

Mistaber is the first system to apply Answer Set Programming (ASP) to halachic reasoning, leveraging its strengths in: - Non-monotonic reasoning (rules with exceptions) - Negation as failure (Closed World Assumption where appropriate) - Default reasoning - Constraint satisfaction

Why ASP?¶

Halachic reasoning has characteristics that make ASP ideal:

Halachic Feature	ASP Capability
Rules with exceptions	Non-monotonic reasoning
"Unless otherwise stated"	Negation as failure
Multiple valid rulings	Multiple answer sets
Constraints must hold	Integrity constraints
Priority between rules	Preference optimization

Example: Default with Override¶

% Default: Of (poultry) + chalav is d'rabanan
asserts(mechaber, issur(achiila, M, d_rabanan)) :-
    is_of_chalav_mixture(M).

% But cooking and benefit are permitted (unlike beheima)
asserts(mechaber, heter(bishul, M)) :-
    is_of_chalav_mixture(M).

asserts(mechaber, heter(hanaah, M)) :-
    is_of_chalav_mixture(M).

Constraint Example¶

% From schema/constraints.lp
% Rules must have at least one makor (source citation)
:- rule(R), not has_makor(R).
has_makor(R) :- rule(R), makor(R, _).

6. Safek Calculus¶

The Innovation¶

Mistaber implements a formal calculus for handling halachic uncertainty (safek), including: - Explicit unknown markers (Open World Assumption) - Safek propagation - Resolution based on normative level - Sfek Sfeika (double doubt)

The Halachic Principle¶

Safek d'oraita l'chumra  - Biblical doubt → be stringent
Safek d'rabanan l'kula   - Rabbinic doubt → be lenient

Implementation¶

% From safek.lp

% Explicit unknown markers
unknown(food_type, F) :-
    food(F),
    not known_food_type(F).

% Safek arises when unknown affects outcome
safek(forbidden, W, Act, F, Ctx) :-
    world(W),
    food(F),
    unknown(food_type, F),
    potentially_forbidden(W, Act, F, Ctx).

% Resolution based on madrega
safek_resolved(W, Act, F, Ctx) :-
    safek(forbidden, W, Act, F, Ctx),
    policy(W, safek_issur, lenient),
    madrega_of_safek(W, Act, F, Ctx, d_rabanan).

derives(W, forbidden(Act, F, Ctx)) :-
    safek(forbidden, W, Act, F, Ctx),
    policy(W, safek_issur, strict),
    madrega_of_safek(W, Act, F, Ctx, d_oraita).

Sfek Sfeika (Double Doubt)¶

% Two independent doubts combine
sfek_sfeika(W, Act, F, Ctx) :-
    safek(forbidden, W, Act, F, Ctx),
    independent_doubt_count(W, Act, F, Ctx, N),
    N >= 2.

% Sfek sfeika resolved leniently
safek_resolved(W, Act, F, Ctx) :-
    sfek_sfeika(W, Act, F, Ctx),
    not sfek_sfeika_strict(W).

World-Specific Policies¶

Different worlds have different safek policies:

% From base.lp - Default
safek_policy(base, d_oraita, l_chumra).
safek_policy(base, d_rabanan, l_kula).

% From ashk_mb.lp - Stricter
safek_policy(ashk_mb, d_oraita, l_chumra).
safek_policy(ashk_mb, d_rabanan, l_chumra).  % Stricter!

% From ashk_ah.lp - Standard
safek_policy(ashk_ah, d_oraita, l_chumra).
safek_policy(ashk_ah, d_rabanan, l_kula).    % Lenient

7. Provenance-Preserving Inference¶

The Innovation¶

Every conclusion in Mistaber traces back to explicit source citations (makor). No rule fires without documented provenance.

Source Citation Format¶

% Rule declaration with mandatory metadata
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).

% The rule body
asserts(mechaber, issur(achiila, M, d_oraita)) :-
    is_beheima_chalav_mixture(M).

Source Types¶

Prefix	Source	Example
`sa`	Shulchan Aruch	`sa("yd:87:1")`
`rema`	Rema's gloss	`rema("yd:87:3")`
`taz`	Turei Zahav	`taz("yd:87:3")`
`shach`	Siftei Kohen	`shach("yd:87:5")`
`biur_hagra`	Vilna Gaon	`biur_hagra("yd:87:1")`
`mishnah_berurah`	Mishnah Berurah	`mishnah_berurah("yd:87:3")`
`beit_yosef`	Beit Yosef	`beit_yosef("yd:87")`

Constraint Enforcement¶

% From schema/constraints.lp
% Rules must have at least one makor
:- rule(R), not has_makor(R).
has_makor(R) :- rule(R), makor(R, _).

% Rules must be scoped to a world
:- rule(R), not has_scope(R).
has_scope(R) :- rule(R), scope(R, _).

Explanation Generation¶

The explain command traces the full derivation:

mistaber explain "holds(issur(achiila, m1, d_oraita), mechaber)"

Output includes the complete reasoning chain with sources.

8. Interpretation Layer Semantics¶

The Innovation¶

Mistaber separates world rulings (what an authority holds) from interpretations (how commentators clarify or modify those rulings). Commentators like Shach and Taz are not separate worlds; they are interpretation functions operating within existing worlds.

Architecture¶

graph LR
    subgraph world["World Layer"]
        mechaber["mechaber"]
    end

    subgraph interp["Interpretation Layer"]
        shach["shach"]
        taz["taz"]
        pri["pri_megadim"]
    end

    shach --> mechaber
    taz --> mechaber
    pri --> shach
    pri --> taz

Commentator Declarations¶

% From interpretations.lp
commentator(shach).        % Sifsei Kohen
commentator(taz).          % Turei Zahav
commentator(pri_megadim).  % R' Yosef Teomim
commentator(pri_chadash).  % R' Chizkiyah da Silva

% Who interprets whom
interprets(shach, mechaber).
interprets(taz, mechaber).
interprets(pri_megadim, shach).
interprets(pri_megadim, taz).

Interpretation Types¶

% Type 1: Adds a condition to a rule
adds_condition(shach, r_bb_dag_sakana, cooked_together).

% Type 2: Removes/relaxes a condition
removes_condition(taz, r_bb_dag_sakana, sakana).

% Type 3: Restricts scope
restricts_scope(comm, rule, scope).

% Type 4: Expands scope
expands_scope(taz, r_bitul_shishim, hefsed_merubeh).

The Shach-Taz Dispute¶

A concrete example of the interpretation layer:

% From shach.lp
% Shach: Sakana only applies when COOKED together
adds_condition(shach, r_bb_dag_sakana, cooked_together).

% From taz.lp
% Taz: The entire sakana ruling is a scribal error!
removes_condition(taz, r_bb_dag_sakana, sakana).
annotation(taz, r_bb_dag_sakana, scribal_error_argument).

Precedence Resolution¶

When commentators conflict:

% Default precedence (higher = wins)
interpretation_precedence(mechaber, taz, 1).
interpretation_precedence(mechaber, shach, 2).
interpretation_precedence(mechaber, pri_chadash, 3).

% Conflict detection and resolution
superseded_interpretation(Authority, Rule, Comm1) :-
    interpretation(Comm1, Rule, I1),
    interpretation(Comm2, Rule, I2),
    Comm1 != Comm2,
    effective_precedence(Authority, Comm1, Prec1),
    effective_precedence(Authority, Comm2, Prec2),
    Prec2 > Prec1,
    conflicts(I1, I2).

Summary¶

Contribution	Domain	Impact
Kripke Semantics	Modal Logic	Multi-tradition reasoning
Deontic Extension	Normative Logic	Halacha-specific modalities
Upper Ontology	Knowledge Rep.	Formal halachic vocabulary
Multi-World Inheritance	KR	Non-monotonic tradition modeling
ASP Application	AI/KRR	Non-monotonic halachic inference
Safek Calculus	Uncertainty	Formal doubt handling
Provenance	Explainability	Traceable conclusions
Interpretation Layer	Modularity	Commentator semantics

These contributions together form a rigorous foundation for computational halacha, enabling verifiable, explainable, and tradition-aware reasoning.