ASP Rules Reference¶

This document describes the Answer Set Programming (ASP) patterns and conventions used in Mistaber's reasoning engine. The engine uses Clingo as its ASP solver with optional asprin for preference optimization.

Overview¶

Mistaber's ASP rules implement: - Kripke semantics for multi-world modal reasoning - Rule activation with scoping and inheritance - Override mechanics for child worlds - Safek (doubt) handling following halachic principles - Interpretation layer for commentator opinions - Preference optimization for deterministic outcomes

World Structure Rules¶

Located in mistaber/ontology/worlds/kripke_rules.lp and individual world files.

World Declaration¶

% Declare a world
world(base).
world(mechaber).
world(rema).

% World accessibility (inheritance)
accessible(mechaber, base).   % mechaber inherits from base
accessible(rema, mechaber).   % rema inherits from mechaber

Truth Propagation (holds/2)¶

The holds/2 predicate tracks what propositions hold in which worlds:

% 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, _).

Transitive Accessibility¶

accessible_transitive(W1, W2) :- accessible(W1, W2).
accessible_transitive(W1, W3) :-
    accessible(W1, W2),
    accessible_transitive(W2, W3).

Safek Policy by World¶

% Default safek policies (can be overridden by child worlds)
safek_policy(base, d_oraita, l_chumra).   % Biblical doubt -> stringent
safek_policy(base, d_rabanan, l_kula).    % Rabbinic doubt -> lenient

Rule Activation¶

Located in mistaber/engine/priorities.lp.

Ancestor Relation¶

% Direct parent is ancestor
ancestor(W_child, W_parent) :-
    world(W_child),
    world(W_parent),
    accessible(W_child, W_parent).

% Transitive closure: grandparent and beyond
ancestor(W1, W3) :-
    world(W1),
    world(W3),
    accessible(W1, W2),
    ancestor(W2, W3).

Rule Activation (active_in_world/2)¶

% A rule is active in a world if directly scoped to that world
active_in_world(R, W) :-
    rule(R),
    world(W),
    scope(R, W),
    not overridden_in(R, W).

% A rule is active in a world if scoped to an ancestor and not overridden
active_in_world(R, W) :-
    rule(R),
    world(W),
    scope(R, W_ancestor),
    ancestor(W, W_ancestor),
    not overridden_in(R, W).

Override Semantics (overrides/4)¶

% A rule is overridden in a world if another rule overrides it
overridden_in(R, W) :-
    rule(R),
    world(W),
    overrides(R_child, R, W, Override_type),
    active_override(R_child, R, W, Override_type).

% Unconditional override always applies
override_applies(R1, R2, W, always) :-
    rule(R1),
    rule(R2),
    world(W),
    overrides(R1, R2, W, always).

% Conditional override applies when condition holds
override_applies(R1, R2, W, condition(C)) :-
    rule(R1),
    rule(R2),
    world(W),
    overrides(R1, R2, W, condition(C)),
    condition_holds(C).

Normative Conclusions¶

Deriving Conclusions (derives/2)¶

% Direct derivation from active rules when conditions are met
derives(W, Conclusion) :-
    world(W),
    active_in_world(R, W),
    rule_concludes(R, Conclusion),
    rule_conditions_met(R).

% Derivation in specific world (for priority-based resolution)
derives_in_world(W, Conclusion) :-
    world(W),
    active_in_world(R, W),
    rule_concludes(R, Conclusion).

Forbidden and Permitted Patterns¶

In world definition files (e.g., mistaber/ontology/worlds/mechaber.lp):

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

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

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

Safek (Doubt) Handling¶

Located in mistaber/engine/safek.lp.

Explicit Unknown Markers (unknown/2)¶

% A food has unknown type if it exists but no food_type is declared
unknown(food_type, F) :-
    food(F),
    not known_food_type(F).

% A mixture has unknown contents if no contains/2 is declared
unknown(contains, M) :-
    mixture(M),
    not known_contains(M).

known_contains(M) :- contains(M, _).

% Temperature unknown
unknown(temperature, F) :-
    food(F),
    not known_temperature(F).

known_temperature(F) :- temperature(F, _).

Safek Propagation (safek/5)¶

% Safek from unknown food_type affecting a food directly
safek(forbidden, W, Act, F, Ctx) :-
    world(W),
    food(F),
    unknown(food_type, F),
    potentially_forbidden(W, Act, F, Ctx).

% Safek from unknown food_type affecting a mixture
safek(forbidden, W, Act, M, Ctx) :-
    world(W),
    mixture(M),
    contains(M, F),
    unknown(food_type, F),
    potentially_forbidden_mixture(W, Act, M, Ctx).

Safek Resolution by Policy (safek_resolved/4)¶

% Resolve safek d'rabanan leniently (safek d'rabanan l'kula)
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).

% Resolve safek d'oraita strictly (safek d'oraita l'chumra)
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).

% Default madrega if not specified: d_rabanan
madrega_of_safek(W, Act, F, Ctx, d_rabanan) :-
    safek(forbidden, W, Act, F, Ctx),
    not explicit_madrega_of_safek(W, Act, F, Ctx).

Sfek Sfeika (Double Doubt)¶

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

% Count independent doubts using aggregate
independent_doubt_count(W, Act, F, Ctx, N) :-
    world(W),
    safek(forbidden, W, Act, F, Ctx),
    N = #count { Reason : doubt_reason(W, Act, F, Ctx, Reason) }.

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

Safek Integrity Constraint¶

% Never derive permitted from absence of issur when unresolved safek exists
:- derives(W, permitted(Act, F, Ctx)),
   safek(forbidden, W, Act, F, Ctx),
   not safek_resolved(W, Act, F, Ctx).

Interpretation Layer¶

Located in mistaber/engine/interpretations.lp.

Commentator Declarations¶

commentator(shach).        % Sifsei Kohen - R' Shabsai HaKohen
commentator(taz).          % Turei Zahav - R' David HaLevi Segal
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
interpretation(Comm, Rule, adds_condition(Cond)) :-
    adds_condition(Comm, Rule, Cond).

% Type 2: Removes/relaxes a condition
interpretation(Comm, Rule, removes_condition(Cond)) :-
    removes_condition(Comm, Rule, Cond).

% Type 3: Restricts scope
interpretation(Comm, Rule, restricts_to(Scope)) :-
    restricts_scope(Comm, Rule, Scope).

% Type 4: Expands scope
interpretation(Comm, Rule, expands_to(Scope)) :-
    expands_scope(Comm, Rule, Scope).

Precedence System¶

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

% Override precedence from config if provided
effective_precedence(Authority, Comm, Prec) :-
    config_interp_precedence(Comm, Prec),
    interprets(Comm, Authority).

Conflict Resolution¶

% An interpretation is superseded if another has higher precedence
superseded_interpretation(Authority, Rule, Comm1) :-
    interpretation(Comm1, Rule, I1),
    interpretation(Comm2, Rule, I2),
    interprets(Comm1, Authority),
    interprets(Comm2, Authority),
    Comm1 != Comm2,
    effective_precedence(Authority, Comm1, Prec1),
    effective_precedence(Authority, Comm2, Prec2),
    Prec2 > Prec1,
    conflicts(I1, I2).

% Two interpretations conflict if they have opposing effects
conflicts(adds_condition(C), removes_condition(C)) :-
    interpretation(_, _, adds_condition(C)),
    interpretation(_, _, removes_condition(C)).

Integrity Constraints¶

Located in mistaber/ontology/schema/constraints.lp.

% Every food must have exactly one top-level classification
:- food(F),
   not food_type(F, basar),
   not food_type(F, chalav),
   not food_type(F, parve),
   not classification_unknown(F).

% A mixture must contain at least one food
:- mixture(M), not has_contents(M).
has_contents(M) :- mixture(M), contains(M, _).

% 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, _).

% World inheritance must be acyclic
:- ancestor(W, W).

% Valid action type check
:- forbidden(_, A, _, _), not action_type(A).
:- permitted(_, A, _, _), not action_type(A).

% Valid madrega type check
:- madrega(_, M), not madrega_type(M).

Preference Optimization (asprin)¶

Located in mistaber/engine/preferences.lp. Used with asprin instead of clingo.

Madrega Weights¶

% Higher weight = stronger normative force
madrega_weight(d_oraita, 100).
madrega_weight(d_rabanan, 50).
madrega_weight(minhag, 25).
madrega_weight(chumra, 10).

Specificity / Quality Tie-Breaker¶

% Prefer rules with more direct sources (makor) as a proxy for specificity.
rule_source_count(R, N) :-
    rule(R),
    N = #count { S : makor(R, S) }.

Preference Declarations¶

% Prefer models that activate higher-madrega rules.
#preference(ruling_by_madrega, more(weight)) {
    N,W,R :: active_rule_madrega_weight(W, R, N)
}.

% Avoid kula in safek d'oraita (penalize deriving permitted under d'oraita safek).
#preference(safek_doraita, less(weight)) {
    1000,W,Act,F,Ctx :: safek_bad_doraita(W, Act, F, Ctx)
}.

% World priority is a partial order declared via priority/3.
#preference(world_priority, poset) {
    world(W);
    world(W1) >> world(W2) : priority(W1, W2, _)
}.

% Tie-breaker: prefer rules with more sources.
#preference(specificity, more(weight)) {
    N,W,R :: active_rule_source_count(W, R, N)
}.

% Combined preference ordering (lexicographic).
#preference(combined, lexico) {
    1 :: **ruling_by_madrega;
    2 :: **safek_doraita;
    3 :: **safek_drabanan;
    4 :: **world_priority;
    5 :: **specificity
}.

#optimize(combined).

Naming Conventions¶

Predicates¶

Pattern	Purpose	Example
`is_X`	Sort membership	`is_food(F)`, `is_vessel(V)`
`X_type`	Classification	`food_type(F, C)`, `action_type(A)`
`has_X`	Existence helper	`has_makor(R)`, `has_scope(R)`
`known_X`	Known value helper	`known_temperature(F)`
`X_of_Y`	Relationship	`madrega_of_safek(...)`

Rules¶

Pattern	Purpose	Example
`r_domain_topic`	Rule identifier	`r_bb_beheima_achiila`
`W`	World variable	`world(W)`
`R`	Rule variable	`rule(R)`
`F`	Food variable	`food(F)`
`M`	Mixture variable	`mixture(M)`
`Act`	Action variable	`forbidden(W, Act, F, C)`
`Ctx`	Context variable	`forbidden(W, A, F, Ctx)`

Worlds¶

World	Description
`base`	Root world, common ground
`mechaber`	Shulchan Aruch author (Sefardi)
`rema`	R' Moshe Isserles (Ashkenazi)
`ashk_mb`	Ashkenazi per Mishnah Berurah
`gra`	Vilna Gaon

Show Directives¶

Each ASP file ends with #show directives to control output:

% World structure
#show world/1.
#show accessible/2.
#show holds/2.

% Rule activation
#show active_in_world/2.
#show overridden_in/2.
#show derives/2.

% Safek handling
#show unknown/2.
#show safek/5.
#show safek_resolved/4.
#show sfek_sfeika/4.

% Interpretation layer
#show commentator/1.
#show interpretation/3.
#show effective_interpretation/3.