lawref.evaluator.proof

Реестр proof-узлов — SPEC §180.

support-id → proof-node-id, детерминированно и однократно: один и тот же assertion даёт один и тот же узел при любом числе обращений.

Classes

Name	Description
ProofRegistry	Единый реестр proof-узлов: support-id → proof-node-id (детерминированно).

ProofRegistryclass#

View source

class ProofRegistry(assertions: dict[str, dict])

Единый реестр proof-узлов: support-id → proof-node-id (детерминированно).

assertionsattributeinstance attribute#

View source

assertions = assertions

by_supportattributeinstance attribute#

View source

by_support: dict[str, str] = {}

last_application_idattributeinstance attribute#

View source

last_application_id: str | None = None

nodesattributeinstance attribute#

View source

nodes: list[dict] = []

add_applicationmethod#

View source

def add_application(rule_id: str, seq: int, subst: dict[str, dict], conclusion: dict, premises: list[str]) -> str

annotate_a3_applicationmethod#

View source

def annotate_a3_application(rule: dict, calls: Iterable[dict] = ()) -> None

Attach A3 row provenance to the just-created ordinary rule proof.

annotate_definition_applicationmethod#

View source

def annotate_definition_application(rule: dict) -> None

DECISION-0151 / §180: применение правила, порождённого определением §144, несёт attributes.definition — понятие (символ-цель ребра provenance), режим, половину и номер альтернативы. Объяснение §183 читает это поле и говорит «по определению», а не «по правилу». В content-id узла §180 поле не входит: тождество применения — правило, подстановка, посылки и вывод.

for_supportmethod#

View source

def for_support(support_id: str) -> str