Encoding Methodology

This document describes the core principles and systematic methodology for encoding halachic content into Mistaber's formal representation. Following these guidelines ensures consistent, accurate, and maintainable encodings across the corpus.

Core Principles

1. Single Seif Granularity

Each encoding unit corresponds to a single seif (paragraph) from the primary source. This granularity provides:

• Precise Attribution: Every rule traces to exactly one primary location
• Focused Review: Reviewers can verify one seif at a time
• Clean Versioning: Changes are isolated to specific seifim
• Parallel Development: Multiple encoders work on different seifim simultaneously

Multi-Seif Anti-Pattern

Never combine content from multiple seifim into a single rule. If a concept spans seifim, encode each seif separately with cross-references.

% WRONG - mixing seifim
asserts(mechaber, issur(achiila, M)) :-
    is_beheima_chalav_mixture(M),  % from YD 87:1
    derech_bishul(M).               % from YD 87:2 - SEPARATE SEIF

% CORRECT - separate rules with linking
asserts(mechaber, issur(achiila, M)) :-
    is_beheima_chalav_mixture(M).

asserts(mechaber, requires_derech_bishul(M)) :-
    is_beheima_chalav_mixture(M).

2. Complete Attribution Chain

Every normative rule must have a complete attribution chain:

% Complete attribution structure
rule(r_bb_beheima_achiila).                      % Rule identifier
makor(r_bb_beheima_achiila, sa("yd:87:1")).      % Primary source
makor(r_bb_beheima_achiila, gemara("Chullin 103b")). % Talmudic source
madrega(r_bb_beheima_achiila, d_oraita).         % Authority level
scope(r_bb_beheima_achiila, mechaber).           % World scope

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

The chain must include:

Component	Required	Description
rule/1	Yes	Unique rule identifier
makor/2	Yes	At least one citation
madrega/2	For normative	Authority level
scope/2	Yes	World where rule is defined

3. Multi-World Representation

Content that varies by tradition must be encoded with proper world scoping:

% Mechaber's position (Sefardi)
scope(r_bb_dag_sakana, mechaber).
asserts(mechaber, sakana(M)) :-
    is_dag_chalav_mixture(M).

% Rema's override (Ashkenazi)
scope(r_rema_dag_chalav_mutar, rema).
override(rema, sakana(M), no_sakana) :-
    is_dag_chalav_mixture(M).
asserts(rema, heter(achiila, M)) :-
    is_dag_chalav_mixture(M).

4. Explicit Over Implicit

Always encode rules explicitly rather than relying on inference:

% CORRECT - explicit permissions
asserts(mechaber, heter(bishul, M)) :-
    is_of_chalav_mixture(M).

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

% WRONG - relying on absence of issur to imply heter
% (No rule implies permission - dangerous!)

5. Semantic Rule Names

Rule identifiers must be semantically meaningful:

% CORRECT - descriptive names
r_bb_beheima_achiila      % basar bechalav beheima eating
r_bb_of_bishul_mutar      % basar bechalav poultry cooking permitted
r_bb_dag_sakana           % fish danger in bb laws
r_rema_waiting_time       % Rema's waiting time ruling

% WRONG - opaque names
r_87_1                    % what does this mean?
r_rule_001                % completely meaningless
r_a                       % unusable

The Encoding Decision Tree

Use this decision tree for every encoding task:

graph TD
    A[Read Source Seif] --> B{Is this halachically normative?}

    B -->|Yes| C{Does it apply to all traditions?}
    B -->|No| D[Encode as classification fact]

    C -->|Yes| E[Encode in base world]
    C -->|No| F{Is there explicit machloket?}

    F -->|Yes| G[Encode in each relevant world]
    F -->|No| H{Which authority stated it?}

    H -->|Mechaber| I[Encode in mechaber world]
    H -->|Rema| J[Encode in rema world]
    H -->|Later Ashkenazi| K[Encode in ashk_mb or ashk_ah]
    H -->|Later Sefardi| L[Encode in sefardi_yo]

    G --> M{Does child world need override?}
    I --> M
    J --> M
    K --> M
    L --> M

    M -->|Yes| N[Add override/3 predicate]
    M -->|No| O[Child inherits automatically]

    D --> P[Write tests]
    E --> P
    N --> P
    O --> P

    P --> Q[Run validation]
    Q --> R{All tests pass?}
    R -->|Yes| S[Submit for review]
    R -->|No| T[Fix issues and retry]
    T --> Q

Step-by-Step Encoding Process

Phase 1: Preparation (30 minutes)

Step 1.1: Source Analysis

1. Read the seif in the original Hebrew
2. Read the Rema's gloss (if any)
3. Read at least two commentaries (Shach, Taz, or others)
4. Note any machloket between authorities
5. Identify the madrega level (d_oraita, d_rabanan, minhag, chumra)

Commentary Selection

For Yoreh Deah, prioritize:

1. Taz (Turei Zahav)
2. Shach (Siftei Kohen)
3. Pri Megadim
4. Aruch HaShulchan
5. Mishnah Berurah (when applicable)

Step 1.2: World Mapping

Determine which worlds need content:

Question	If Yes	If No
Does Mechaber state this explicitly?	mechaber world	Check if implied
Does Rema gloss disagree?	rema world with override	rema inherits
Does GRA have unique position?	gra world	gra inherits
Do later poskim modify?	Add to child worlds	Children inherit

Step 1.3: Predicate Selection

1. Check the Predicate Registry for existing predicates
2. Verify sort compatibility
3. If no suitable predicate exists, document the need before creating new ones

Phase 2: Implementation (45-60 minutes)

Step 2.1: Create Base Definitions

Start with shared facts and helper predicates:

% ============================================================
% YD 87:1 - Beheima with Milk
% ============================================================

% === Mixture Classification ===
is_beheima_chalav_mixture(M) :-
    mixture_has_basar(M, beheima),
    mixture_has_chalav(M).

% === Madrega Determination ===
basar_chalav_madrega(M, d_oraita) :-
    is_beheima_chalav_mixture(M).

Step 2.2: Add Rule Metadata

Every rule needs complete metadata:

% Rule declaration
rule(r_bb_beheima_achiila).

% Source citation (MANDATORY)
makor(r_bb_beheima_achiila, sa("yd:87:1")).
makor(r_bb_beheima_achiila, rambam("ma:9:1")).

% Authority level
madrega(r_bb_beheima_achiila, d_oraita).

% World scope
scope(r_bb_beheima_achiila, mechaber).

Step 2.3: Write the Rule

The rule itself follows the metadata:

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

Step 2.4: Add Overrides (When Needed)

If a child world differs:

% Rema's override for fish+dairy
rule(r_rema_dag_chalav_mutar).
makor(r_rema_dag_chalav_mutar, rema("yd:87:3")).
scope(r_rema_dag_chalav_mutar, rema).

% Override the sakana ruling
override(rema, sakana(M), no_sakana) :-
    is_dag_chalav_mixture(M).

% Assert the alternative position
asserts(rema, heter(achiila, M)) :-
    is_dag_chalav_mixture(M).

Phase 3: Testing (30 minutes)

Step 3.1: Positive Test Cases

Test that rules fire correctly:

def test_beheima_chalav_issur_achiila():
    """Beheima+chalav eating is forbidden d'oraita in mechaber world."""
    result = query("""
        mixture(m1).
        food(beef). food_type(beef, beheima).
        food(milk). food_type(milk, chalav).
        contains(m1, beef). contains(m1, milk).
    """, world="mechaber")

    assert result.holds("issur(achiila, m1, d_oraita)")

Step 3.2: Negative Test Cases

Test that rules do not fire incorrectly:

def test_parve_no_issur():
    """Parve foods have no basar bechalav issur."""
    result = query("""
        mixture(m1).
        food(carrot). food_type(carrot, parve).
        food(rice). food_type(rice, parve).
        contains(m1, carrot). contains(m1, rice).
    """, world="mechaber")

    assert not result.holds("issur(achiila, m1, _)")

Step 3.3: Edge Cases

Test boundary conditions:

def test_single_food_no_mixture():
    """Single food item is not a basar bechalav mixture."""
    result = query("""
        food(beef). food_type(beef, beheima).
        % No mixture, no contains - just a single food
    """, world="mechaber")

    assert not result.holds("issur(achiila, beef, _)")

Step 3.4: Multi-World Tests

Test inheritance and overrides:

def test_fish_dairy_mechaber_vs_rema():
    """Fish+dairy: Mechaber=sakana, Rema=permitted."""
    setup = """
        mixture(m1).
        food(salmon). food_type(salmon, dag).
        food(cream). food_type(cream, chalav).
        contains(m1, salmon). contains(m1, cream).
    """

    mechaber_result = query(setup, world="mechaber")
    rema_result = query(setup, world="rema")

    # Mechaber: forbidden due to sakana
    assert mechaber_result.holds("sakana(m1)")
    assert mechaber_result.holds("issur(achiila, m1, sakana)")

    # Rema: permitted
    assert rema_result.holds("no_sakana(m1)")
    assert rema_result.holds("heter(achiila, m1)")

Phase 4: Documentation (15 minutes)

Step 4.1: File Header

Every file needs a comprehensive header:

% mistaber/ontology/corpus/yd_87/base.lp
% Yoreh Deah Siman 87: Basar Bechalav (Meat and Milk)
%
% This file contains the foundational predicates and rules for reasoning
% about the prohibition of mixing meat and milk, as codified in
% Shulchan Aruch Yoreh Deah 87.
%
% Source: SA YD 87:1-11
% "Lo tevashel gedi bachalev imo" - The Torah repeats this prohibition
% three times to teach:
%   1. Issur bishul (cooking prohibition)
%   2. Issur achiila (eating prohibition)
%   3. Issur hanaah (benefit prohibition)

Step 4.2: Section Comments

Group related rules with section headers:

% ============================================================================
% YD 87:3 - OF (POULTRY) + CHALAV: D'RABANAN
% ============================================================================
% "Basar chaya v'of... eino assur ela miderabanan"
% Poultry with milk is only rabbinically forbidden.
% Cooking and benefit are PERMITTED for of + chalav.
% Source: SA YD 87:3

Step 4.3: Inline Comments

Explain non-obvious logic:

% Note: Sakana is treated more stringently than regular issur in some aspects
% It does not have the same bitul (nullification) rules as regular issurim
asserts(mechaber, issur(achiila, M, sakana)) :-
    is_dag_chalav_mixture(M).

Quality Standards Table

Aspect	Requirement	Verification
Rule ID	Semantic, r_ prefix	Manual review
Makor	At least one citation	Type checker
Madrega	Specified for normative	Type checker
Scope	Explicit world declaration	Type checker
Comments	File header, section headers	Manual review
Tests	5 positive, 3 negative, 2 edge	CI pipeline
Override Syntax	Descriptive third argument	Manual review

Common Pitfalls and Solutions

Pitfall 1: Invalid Override Values

Never Use 'invalid' in Override/3

The third argument of override/3 must be a descriptive value, not 'invalid'.

% WRONG
override(rema, sakana(M), invalid) :- is_dag_chalav_mixture(M).

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

Pitfall 2: Siman-Based Rule Names

Never Use Siman:Seif as Rule Names

Rule names must be topic-based, not location-based.

% WRONG
rule(r_87_3).
rule(r_yd_87_seif_3).

% CORRECT
rule(r_bb_of_achiila).
rule(r_bb_chaya_bishul_mutar).

Pitfall 3: Missing Makor for Normative Rules

Every Normative Rule Needs Makor

The type checker rejects normative rules without citations.

% WRONG - missing makor
rule(r_something).
madrega(r_something, d_rabanan).
asserts(mechaber, issur(achiila, M)) :- ...

% CORRECT - with makor
rule(r_something).
makor(r_something, sa("yd:87:5")).
madrega(r_something, d_rabanan).
asserts(mechaber, issur(achiila, M)) :- ...

Pitfall 4: Incorrect World Inheritance

Understand the DAG Before Encoding

Rules in parent worlds propagate to children unless overridden.

% If encoded in 'base':
% - Propagates to ALL worlds (mechaber, rema, gra, and all children)

% If encoded in 'rema':
% - Propagates to ashk_mb and ashk_ah
% - Does NOT propagate to mechaber or sefardi_yo

% If encoded in 'mechaber':
% - Propagates to sefardi_yo
% - Does NOT propagate to rema or any Ashkenazi world

Pitfall 5: Negating OWA Predicates

Avoid Negating Open-World Predicates

Negating permitted, forbidden, or other OWA predicates is unsafe.

% WRONG - negating OWA predicate
allowed(F) :- food(F), not forbidden(_, _, F, _).

% CORRECT - use explicit positive conditions
allowed(F) :- food(F), has_heter(F).

Pitfall 6: Mixing Seif Content

One Seif Per Rule Set

Never combine content from multiple seifim.

% WRONG - mixing YD 87:1 and 87:2
asserts(mechaber, issur(achiila, M)) :-
    is_beheima_chalav_mixture(M),  % from 87:1
    not b_aino_mino(M).             % from 87:2

% CORRECT - separate rule sets with cross-references
% In yd_87_1:
asserts(mechaber, issur(achiila, M)) :-
    is_beheima_chalav_mixture(M),
    mixture_requires_87_1_analysis(M).

% In yd_87_2:
mixture_requires_87_1_analysis(M) :-
    not b_aino_mino(M).

Complete Example: YD 87:3 Of + Chalav

Here is a complete encoding example following all methodology:

% ============================================================================
% YD 87:3 - OF (POULTRY) + CHALAV: D'RABANAN
% ============================================================================
% "Basar chaya v'of... eino assur ela miderabanan"
%
% SOURCE ANALYSIS:
% - SA YD 87:3: Poultry with milk is only rabbinically forbidden
% - Gemara Chullin 104a-b: Discusses rabbinic origin of of+chalav
% - Rema: No gloss (agrees with Mechaber on this point)
%
% WORLD MAPPING:
% - Base rule applies to all traditions
% - No machloket on this specific point
% - Encoded in 'mechaber' as the primary source, inherited by all
%
% MADREGA: d_rabanan (explicitly stated in SA)

% === Rule: Of + Chalav - Eating forbidden d'rabanan ===
rule(r_bb_of_achiila).
makor(r_bb_of_achiila, sa("yd:87:3")).
makor(r_bb_of_achiila, gemara("Chullin 104a")).
madrega(r_bb_of_achiila, d_rabanan).
scope(r_bb_of_achiila, mechaber).

asserts(mechaber, issur(achiila, M, d_rabanan)) :-
    is_of_chalav_mixture(M).

% === Rule: Of + Chalav - Cooking permitted ===
% SA YD 87:3: "muter b'bishul"
rule(r_bb_of_bishul_mutar).
makor(r_bb_of_bishul_mutar, sa("yd:87:3")).
scope(r_bb_of_bishul_mutar, mechaber).

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

% === Rule: Of + Chalav - Benefit permitted ===
% SA YD 87:3: "muter... u'bhanaah"
rule(r_bb_of_hanaah_mutar).
makor(r_bb_of_hanaah_mutar, sa("yd:87:3")).
scope(r_bb_of_hanaah_mutar, mechaber).

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

Encoding Checklist

Before submitting, verify:

• [ ] Rule IDs are semantic with r_ prefix
• [ ] All normative rules have makor/2
• [ ] All normative rules have madrega/2
• [ ] All rules have scope/2
• [ ] Override/3 uses descriptive values (never 'invalid')
• [ ] World inheritance is correct
• [ ] At least 5 positive tests pass
• [ ] At least 3 negative tests pass
• [ ] At least 2 edge case tests pass
• [ ] Multi-world tests pass (if applicable)
• [ ] File has comprehensive header comment
• [ ] Sections have header comments
• [ ] Complex logic has inline comments
• [ ] Type checker passes with no errors
• [ ] Type checker passes with no warnings

Related Guidelines

• Halachic Accuracy - Verification standards
• Source Attribution - Makor chain details
• World Scoping - When to use which world
• Testing Requirements - Full test specifications
• Review Standards - Quality checklist