Establish the evidence-gated executable logic museum and Lean oracle - #2
Draft
SMC17 wants to merge 21 commits into
Draft
Establish the evidence-gated executable logic museum and Lean oracle#2SMC17 wants to merge 21 commits into
SMC17 wants to merge 21 commits into
Conversation
…oracle - reason/abduction.zig: subset-minimal, background-consistent explanations; MARCO-style enumeration (MUS shrink / MSS grow), fresh-solver certificates - reason/induction.zig: exact SAT synthesis of minimal-k DNF from examples, deductively re-verified; distinct from circuit k-induction - api/v1 1.1.0: abduce/induceDnf + reason_abduce/reason_induce capability bits - taxonomy: inductive & abductive rows documented -> fragment - CLI: abduce-demo, induce-demo; api-info prints new caps - pre-registered exp-1784298692-629536463 / exp-1784298694-561301438, both confirmed
…on, Bayesian induction, defaults, rational closure - sat/maxsat.zig: weighted partial MaxSAT, exact via descending bound + SWC encoding, brute-force verified on 60 random instances - reason/abduction.zig abduceMinCost: implicit hitting-set duality over the MaxSAT oracle; cardinality & weighted objectives, brute-force cross-checked - reason/alp.zig: abductive logic programming — first-order SLD abduction with trail unification, occurs check, variable denials, independent derives() check - reason/bayes.zig: exact Bayesian posterior over conjunction class (Occam prior, ε-noise), MAP + model-averaged prediction, Laplace succession - reason/default_logic.zig: Reiter extensions (groundedness, justification vs final extension, stability), credulous/skeptical; full canon incl. Nixon, no-extension, self-support rejection - reason/klm.zig: rational closure via SAT exceptionality ranks; specificity, irrelevance, vacuity canon - api/v1 1.2.0 (6 new caps), taxonomy +5 fragment rows, CLI reason-demo - six pre-registered experiments, all confirmed (1 Type-I caught by falsifier)
…ircumscription, analogy - reason/argumentation.zig: Dung AFs — grounded fixpoint, admissible/complete/ stable/preferred, credulous & skeptical acceptance; full canon incl. floating acceptance and grounded ⊆ preferred - reason/asp.zig: stable models via Gelfond–Lifschitz reduct least-model certificate; unfounded positive loops rejected, constraints, stratified canon - reason/agm.zig: AGM base contraction via remainder sets (maxichoice / full-meet / cardinality) + Levi revision; success, inclusion, vacuity, tautology-failure, consistency postulates tested - reason/circumscription.zig: P-minimal-model entailment (minimized/fixed/ varying), bird/ab canon + 30 random instances vs independent brute oracle - reason/analogy.zig: Miclet–Prade Boolean proportions — axioms verified, unique solving, affine-exact abstaining classifier (XOR overclaim caught by falsifier, rewritten as abstention test) - api/v1 1.3.0: Capability u32→u64 (low word stable), 5 new bits + re-exports - taxonomy +5 fragment rows; coverage: Analogical & Dialogical modes now M - five pre-registered experiments confirmed (1 Type-I self-caught)
…emic, syllogistic, EL - logic/intuitionistic.zig: G4ip (Dyckhoff) decision procedure with immutable contexts; canon + 80-formula Glivenko cross-check vs truth-table oracle (context-corruption Type-I in first draft caught by the falsifier) - logic/manyvalued.zig: classical/K3/LP/FDE/Ł3 matrices, designated-value consequence; LP paraconsistency, K3 gaps, Ł3 contraction failure, FDE gap+glut; classical matrix brute-verified - modal/epistemic.zig: multi-agent S5 with common knowledge (reachability fixpoint) and public announcements; full muddy-children canon + S5 introspection + E-vs-C separation - logic/syllogistic.zig: complete Venn-region decision — exactly 15 Boolean / 24 import-valid of 256 forms; named canon incl. Darapti import-only, AAA-2 - logic/el.zig: EL normalization + completion subsumption; role-chain and pericarditis canon with exact closure - api/v1 1.4.0 (5 new caps), taxonomy: 6 rows documented→fragment (now 25 fragments / 10 engines / 5 documented) - five pre-registered experiments confirmed (1 Type-I self-caught)
…egistry map widened - logic/linear.zig: MLL+units one-sided sequent prover (invertible ⅋/⊥, exact ⊗ splitting); weakening/contraction/MIX refuted; balanced-atom invariant on 300 random formulas; dual involutive - modal/deontic.zig: SDL (KD) on serial finite frames — O/P duality, D⇔seriality with failure demo, K distribution, no-conflict, Ross valid / converse refuted - api/v1 1.5.0: modal_deontic + logic_linear_mll caps - taxonomy: linear-logic & deontic → fragment; +12 honest documented rows (PDL, hybrid, μ-calculus, causal models, team logic, free logic, second-order, quantum, natural logic, medieval consequence, possibilistic, autoepistemic) — registry now 61 systems: 27 fragment / 10 engine / 15 documented - build.zig.zon version unstuck 0.12.0 → 0.22.0 - both pre-registered experiments confirmed
SMC17
changed the title
SMC17
added
exhibit
…nt evaluators + exhaustive oracle) - src/modal/pdl.zig: Propositional Dynamic Logic on finite frames. Programs a|α;β|α∪β|α*|φ? with [α]φ / ⟨α⟩φ modalities. - Two independent evaluators (matrix RTC and Fischer-Ladner graph reach) cross-checked over hundreds of randomized formulas/models. - Exhaustive finite-frame oracle confirms validities (K, distribution, composition, union, star unroll, star induction, test equivalence, diamond-star fixpoint) and produces countermodels for known non-validities. - verifyClaim replays a verdict against both engines, fails closed on divergence. - Registry dynamic-pdl: documented -> fragment; museum promotion derived to verified_exhibit (12th exhibit); api/v1 -> 1.6.0 with modal_pdl cap bit. - Evidence contract docs/exhibits/pdl.md; STATUS/NEXT/CHANGELOG updated. 436/436 tests pass.
…PASIR version bump, FOL scope doc
Verification against the ChatGPT audit (which could not execute the repo and
audited a stale main@v0.17):
- CONFIRMED STALE: k-induction unsoundness, cumulative SAT conflict budgets,
IPASIR callback no-ops, trust fail-open, FOL binder collisions — all already
fixed on this branch (see CHANGELOG Unreleased lines 59-75).
- FIXED (genuinely live on this branch):
- root helpers isTautology/areEquivalent folded solver unknown into false;
now tri-state ?bool (null=unknown) with regression test (max_conflicts=0).
CLI tautology/equiv report UNKNOWN (exit 2) instead of NOT_TAUTOLOGY.
- Bounded CTL result labels renamed holds/fails -> holds_within_bound/
fails_within_bound so the API cannot be read as a complete unbounded proof.
- IPASIR signature() bumped logic-zig-ipasir-0.12 -> 1.0.
- FOL finite-model finder scope documented honestly (name-keyed symbols,
missing constant -> error.Unbound, domain cap 4).
zig build test green (429 root tests + full suite, FULL_EXIT=0).
…s-check
- src/ctl/ltl.zig: bounded LTL over finite traces (X/F/G/U/R), two
independent evaluators (direct structural recursion + SAT via Tseitin
encoding) that MUST agree, exhaustive small-trace oracle, and a
fail-closed verifyClaim (returns error on divergence / expected mismatch,
never a silent pass).
- Correct finite-trace recurrence semantics: U_i = psi_i \/ (phi_i /\ U_{i+1}),
R_i = psi_i \/ (phi_i /\ R_{i+1}), base U_{L+1}=R_{L+1}=false; X off-end=false.
- docs/exhibits/ltl.md: formal identity, two-semantics contract, boundary
semantics, oracle method.
- Wired into museum: root.ltl export, registry 'ltl-bounded' row
(verified_exhibit), exhibit manifest entry (all 7 claims complete),
promotion assertion.
- Verified: canonical 'zig build test' green (62 tests); exhaustive
direct==SAT cross-check on all traces (frames<=4, nets<=2) and random
proofs of validity (F p <-> ~G~p, p U q => F q, G p => p@0).
registry.Maturity has no 'verified_exhibit' member (that concept lives in exhibit.Promotion, derived from claims). The ltl-bounded row used '.verified_exhibit', which broke compilation of the whole registry module. Revert to '.fragment' to match the convention (dynamic-pdl uses .fragment too); the verified_exhibit promotion is already asserted via exhibit.promotion() in the manifest. Verified: 'zig build test' green (FULL_EXIT=0).
- src/ctl/ltl.zig: add strict previous Y, weak previous Z, since S, before B.
Same two-evaluator discipline as LTL: direct backward recurrence
(S_i = psi_i \/ (phi_i /\ S_{i-1}), B dual) and a Tseitin SAT encoding
that mirrors it exactly (prev/preweak look back to frame i-1; S/B use
prev_var at i>0, base S_{-1}=B_{-1}=false).
- Folded into the exhaustive cross-check oracle (all traces frames<=4,
nets<=2, every operator incl. Y/Z/S/B): direct == SAT on all, 0 mismatches.
- Added PLTL duality/validity tests (Z phi <-> ~Y~phi, boundary Z true /
Y false at frame 0), cross-checked by both evaluators.
- Museum wiring: STATUS.md modal/temporal row, registry ltl-bounded notes,
CHANGELOG.
- Verified: exhaustive direct==SAT oracle green; canonical 'zig build test'
green (FULL_EXIT=0).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What changed
museumcommand.Why
The repository previously mixed real solver kernels with broad registry claims. This change makes completeness local, explicit, fail-closed, and tied to executable evidence while preserving the long-term goal of implementing every branch of logic.
Evidence
Local:
zig fmt --check src build.zigzig build test --summary all— 430/430 tests passed.zig build --summary all— 19/19 build steps passed.logic-zig doctor—DOCTOR_OK.logic-zig trust-report—TRUST_OK.(cd lean && lake build)— Lean 4.28.0 kernel build passed.actionlint1.7.12 passed.CITATION.cffvalidates against schema 1.2.0.Hosted CI now builds pinned CaDiCaL, DRAT-trim, and ABC before requiring
TRUST_OK. The Lean lane rejects trust escapes, builds under Lean 4.28, and runs the bundled whole-environmentleanchecker. Independent nanoda checking is not claimed: its current parser rejects Lean 4.28 exports, tracked upstream in leanprover/lean-action#169. Hosted results are pending on this commit.Explicit limits
This PR does not claim universal completion, industrial parity with specialist solvers, formal verification of the Zig checkers, or trust in raw Aristotle output. The Lean-to-Zig specification correspondence remains a reviewed and tested boundary.