Repository navigation
Phase 8: SMT-LIB translation and the Z3 auto-prover - #10
Merged
Merged
Conversation
- Translation to SMT-LIB 2: individuals, worlds for modal formulas (S5 as universal quantification over worlds, constant domains, rigid identity), properties with an application predicate and a comprehension axiom per lambda (Henkin semantics) - Z3 runs as an external program ( or z3 on the PATH), with a time limit; no link dependency, so MinGW builds are unaffected; the browser build reports that Z3 is unavailable - 'by z3' justification, theosc prove, theosc export --format smtlib - Z3 confirms every inference in the library except Goedel's T3, which it cannot decide in 20 s and which stands on its natural-deduction proof - Tests: script structure, valid and invalid inferences (so the encoding is not trivially inconsistent), 'by z3'; skipped when Z3 is absent - CI installs Z3 on Linux and in MSYS2 - docs/spec/smt.md Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019WEmxyo9CRKSbjbEdCuJTG
|
Important
This repository does not receive automatic reviews because it has fewer than 10 stars.
 |
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
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.
Stacked on #9. Implements Phase 8 of
ROADMAP.md.src/core/smt.cpp, spec indocs/spec/smt.md): individuals; worlds when formulas are modal (S5 as universal quantification over worlds, constant domains, rigid identity); properties with an application predicate and one comprehension axiom per λ (Henkin semantics, the standard embedding for Gödel's argument).theosc export --format smtlibprints the scripts.$THEOS_Z3orz3on the PATH) with a 20 s limit, so nothing links against it and MinGW builds are unaffected. The browser build reports that Z3 isn't available. Addsby z3as a justification andtheosc provefor a second opinion on every inference.Results on the library: Z3 independently confirms every inference except Gödel's T3, which Z3 4.8 can't decide within 20 s. T3 stands on its natural-deduction proof, and the docs say so.
Tests check that Z3 also rejects invalid inferences, including ones with λ, property quantification and modality, so the encoding isn't trivially inconsistent. Z3 tests are skipped when Z3 is missing; CI installs it on Linux and in MSYS2.
Generated by Claude Code