Published package / CLIR
calc.proof_checker
v0.1.0The package has no official source title — in CLIR its package carries neither description nor labels, and the showcase will not invent one.
A package can be printed as a standalone module in a general-purpose language that answers without the rules engine: an answer and its status, with no proof, hashes or canonical document. Everything on this page comes from the generation plan built with the index; the gallery computes nothing of its own.
Generation plan
The plan builds: the package can be printed as a module.
- plan format
- law-backend-plan/0.17
- capabilities
- aggregate, defeasible, negation, status:monotone, status:not_known, term:body
Checked against package scenarios
74 of 74 scenarios matched on ts, py, go
- answer statuses
- FALSE_ONLY 55 · NEITHER 5 · TRUE_ONLY 14
Target languages
gopyts
refuse this plan · 13
bslверсия плана не поддержана эмиттером: 'law-backend-plan/0.17' (поддержана law-backend-plan/0.7)RUcsверсия плана не поддержана эмиттером: 'law-backend-plan/0.17' (поддержана law-backend-plan/0.7)RUdartверсия плана не поддержана эмиттером: 'law-backend-plan/0.17' (поддержана law-backend-plan/0.7)RUerlверсия плана не поддержана эмиттером: 'law-backend-plan/0.17' (поддержана law-backend-plan/0.7)RUexверсия плана не поддержана эмиттером: 'law-backend-plan/0.17' (поддержана law-backend-plan/0.7)RUjavaверсия плана не поддержана эмиттером: 'law-backend-plan/0.17' (поддержана law-backend-plan/0.7)RUktверсия плана не поддержана эмиттером: 'law-backend-plan/0.17' (поддержана law-backend-plan/0.7)RUluaверсия плана не поддержана эмиттером: 'law-backend-plan/0.17' (поддержана law-backend-plan/0.7)RUphpверсия плана не поддержана эмиттером: 'law-backend-plan/0.17' (поддержана law-backend-plan/0.7)RUrbверсия плана не поддержана эмиттером: 'law-backend-plan/0.17' (поддержана law-backend-plan/0.7)RUrsверсия плана не поддержана эмиттером: 'law-backend-plan/0.17' (поддержана law-backend-plan/0.7)RUscalaверсия плана не поддержана эмиттером: 'law-backend-plan/0.17' (поддержана law-backend-plan/0.7)RUswiftверсия плана не поддержана эмиттером: 'law-backend-plan/0.17' (поддержана law-backend-plan/0.7)RU
./law dev backend corpus/clir/calc-proof-checker.lawir.json --target ts --target py --target go --out DIR
Module interface
Questions are public relations with a producing rule; inputs are the facts a question reads. Function names follow the language: ask_… in Python, ask.… in TypeScript, Ask… in Go.
Questions · 10
| Name | Parameters | Meaning | Reads | Sources |
|---|---|---|---|---|
| blocked_step | text, dec, dec | правильная форма шага зависит от непроверенного основанияRU | allowedcloseddocumentlinenode | |
| equivalent | text, dec, dec | структурное равенство формул с любыми идентификаторамиRU | node | |
| first_error | text, dec | первый первичный дефект по номеру строкиRU | allowedcloseddocumentlinenode | |
| formula_error | text, dec, text | дефект определения или ссылки на формулуRU | allowedcloseddocumentnode | |
| proof_error | text, text | дефект заголовка, контекста или заявленной целиRU | closeddocumentlinenode | |
| proof_valid | text | весь завершённый документ является доказательством цели относительно разрешённых предпосылокRU | allowedcloseddocumentlinenode | |
| proven | text, dec | проверенное заключение в контексте предпосылок данного доказательстваRU | allowedcloseddocumentlinenode | |
| step_error | text, dec, text | первичный дефект строкиRU | allowedcloseddocumentlinenode | |
| step_valid | text, dec | строка проверена и не содержит собственной ошибкиRU | allowedcloseddocumentlinenode | |
| well_formed | text, dec | конечная корректная структура формулыRU | node |
Inputs · 5
| Name | Parameters | Meaning |
|---|---|---|
| allowed | text, dec | разрешённая предпосылка именно этого доказательстваRU |
| closed | text | ввод формул, предпосылок и строк завершёнRU |
| document | text, dec, dec, text | число строк, цель и фиксированная версия исчисленияRU |
| line | text, dec, dec, text, dec, dec | предъявленная строка: формула, правило и номера основанийRU |
| node | text, dec, text, text, dec, dec | структура формулы: atom, imp либо and; неиспользуемые поля пусты или равны нулюRU |