Skip to content

HolRefute: Quickcheck, narrowing and a Nitpick-style Kodkod model finder #2051

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
lukaszcz wants to merge 601 commits into
base: develop
Choose a base branch
from
Open

HolRefute: Quickcheck, narrowing and a Nitpick-style Kodkod model finder #2051

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
601 commits
Select commit Hold shift + click to select a range
698370e
HolRefute: retain compact upper bounds during validation
lukaszcz Jul 30, 2026
b25b258
HolRefute: retain mixed arithmetic cardinality axioms
lukaszcz Jul 30, 2026
5b225c8
HolRefute: reject oracle-tagged certificates
lukaszcz Jul 30, 2026
e8036f8
HolRefute: mark rejected QC candidates incomplete
lukaszcz Jul 30, 2026
356f4f3
HolRefute: distrust disk theorems in certification
lukaszcz Jul 30, 2026
f8aed18
HolRefute: make uncertified QC hits incomplete
lukaszcz Jul 30, 2026
0457d13
HolRefute: require random draws for completeness
lukaszcz Jul 30, 2026
f66f652
HolRefute: bind smart generator outputs before residual checks
lukaszcz Jul 30, 2026
9942674
HolRefute: freshen retyped preprocessing binders
lukaszcz Jul 30, 2026
a863218
HolRefute: restrict harmless arithmetic axioms
lukaszcz Jul 30, 2026
6e8a33e
HolRefute: report only certified model evaluations
lukaszcz Jul 30, 2026
8cd6a04
HolRefute: vary polymorphic finite types independently
lukaszcz Jul 30, 2026
b6b17a5
HolRefute: reject mixed bisimulation depth modes
lukaszcz Jul 30, 2026
4a0e7fc
HolRefute: bound solver output capture
lukaszcz Jul 30, 2026
325c6cd
HolRefute: treat solver exit 130 as an error
lukaszcz Jul 30, 2026
30abd9c
HolRefute: bound solver cancellation cleanup
lukaszcz Jul 30, 2026
aa423c3
mosml: mask SIGINT in uninterruptible sections
lukaszcz Jul 30, 2026
83a18e9
HolRefute: retain theorem hypotheses in unused probes
lukaszcz Jul 30, 2026
fe81867
HolRefute: require closed abstract generator predicates
lukaszcz Jul 30, 2026
c1ac5ad
HolRefute: track binders in arithmetic axiom checks
lukaszcz Jul 30, 2026
dc1818c
HolRefute: use absolute cancellation timer
lukaszcz Jul 30, 2026
569bbc4
HolRefute: remove untrusted evaluation merge
lukaszcz Jul 30, 2026
1fd0a22
HolRefute: reject unsupported finite type sizes
lukaszcz Jul 30, 2026
bd0923e
HolRefute: reject conditional display evaluations
lukaszcz Jul 30, 2026
798ff31
HolRefute: declare QC model-finder dependency
lukaszcz Jul 30, 2026
772b383
HolRefute: make generator registrations replaceable
lukaszcz Jul 30, 2026
2d617a1
HolRefute: reject overflowing scope bounds
lukaszcz Jul 30, 2026
12dfaf7
HolRefute: retain discarded potential-model evidence
lukaszcz Jul 30, 2026
2aeab37
HolRefute: make weakened model search inconclusive
lukaszcz Jul 30, 2026
603dd75
HolRefute: bound substrate cleanup
lukaszcz Jul 30, 2026
e745ede
HolRefute: apply abstract predicates before narrowing closure
lukaszcz Jul 30, 2026
42beb32
HolRefute: preserve nonlinear native patterns
lukaszcz Jul 30, 2026
62e82d5
HolRefute: align model-finder certificate tests
lukaszcz Jul 30, 2026
197ffc8
mosml: do not disable SIGINT exception delivery
lukaszcz Jul 30, 2026
3837273
HolRefute: align range-guard selftests
lukaszcz Jul 30, 2026
6a06617
HolRefute: make evaluator lock waits interruptible
lukaszcz Jul 30, 2026
f2b0f24
HolRefute: avoid equality in type-only extraction
lukaszcz Jul 30, 2026
11a8c6b
HolRefute: preserve narrowing search failures over cleanup
lukaszcz Jul 30, 2026
8c8a094
HolRefute: validate all model-finder term row keys
lukaszcz Jul 30, 2026
cd0748e
HolRefute: preserve unknown set memberships
lukaszcz Jul 30, 2026
4db843d
HolRefute: reject duplicate solver tuples
lukaszcz Jul 30, 2026
fadc9a5
HolRefute: reap solver groups after normal launcher exit
lukaszcz Jul 30, 2026
96676da
HolRefute: omit uncertified data from genuine models
lukaszcz Jul 30, 2026
19fa4d7
HolRefute: reject unresolved certificate evaluations
lukaszcz Jul 30, 2026
2c9b2b2
HolRefute: honor quiet mode in reentrant calls
lukaszcz Jul 30, 2026
5ea3368
docs: state Refute model-finder validation ranges
lukaszcz Jul 30, 2026
3d9f187
docs: describe Refute backend result records
lukaszcz Jul 30, 2026
0df7420
HolRefute: run full model-finder corpus on SAT4J
lukaszcz Jul 30, 2026
3e5399d
Merge branch 'HOL-Theorem-Prover:develop' into develop
lukaszcz Jul 30, 2026
e88fe5f
Merge branch 'develop' into nitpick
lukaszcz Jul 30, 2026
bf93132
Revert unrelated ThmSetData delta-ordering fix
lukaszcz Jul 30, 2026
b9605e6
coalgebras: keep path_11 local
lukaszcz Jul 30, 2026
43f953d
HolRefute: make the selftest runnable and fix what it exposed
lukaszcz Jul 31, 2026
297a07b
HolRefute: add user-level examples
lukaszcz Jul 31, 2026
9b4f2bf
HolRefute: accept total equivalences and encode subset typedefs
lukaszcz Jul 31, 2026
9cbc4e2
HolRefute: fix the SML extraction naming and matching layers
lukaszcz Jul 31, 2026
3b330f2
HolRefute: keep the numeral skeleton built in
lukaszcz Jul 31, 2026
1b9aaba
HolRefute: keep first-order data types concrete
lukaszcz Jul 31, 2026
cdbaa48
HolRefute: monomorphize type variables uniformly again
lukaszcz Jul 31, 2026
2db1913
HolRefute: re-baseline seven Kodkodi smokes to the trust model
lukaszcz Jul 31, 2026
c488ce6
HolRefute: make the evaluator theory bracket re-entrant
lukaszcz Jul 31, 2026
cd30fa2
HolRefute: give the ParList loser a worker to lose on
lukaszcz Jul 31, 2026
18b6e59
HolRefute: record the Kodkodi trust decision as settled
lukaszcz Jul 31, 2026
ef95af3
HolRefute: keep planned enumerators across the evaluator bracket
lukaszcz Jul 31, 2026
19aa93b
HolRefute: restore the Kodkodi trust model
lukaszcz Jul 31, 2026
e59dbe6
Merge branch 'HOL-Theorem-Prover:develop' into develop
lukaszcz Aug 1, 2026
a25f23e
HolRefute: charge only unsound encodings to the potential budget
lukaszcz Aug 1, 2026
3d2682f
HolRefute: stop faithful ersatz substitutions from voiding a verdict
lukaszcz Aug 1, 2026
860c3fd
HolRefute: a cleanup that finished is not a timeout
lukaszcz Aug 1, 2026
638897a
HolRefute: bound a cleanup by not waiting on it
lukaszcz Aug 1, 2026
ced8b5c
HolRefute: card 1 is a real scope for one_or_two, so the model is real
lukaszcz Aug 1, 2026
ed68b75
HolRefute: refresh the stale 07 narrowing needle witness
lukaszcz Aug 1, 2026
0c72c6d
HolRefute: keep the shared pattern matcher's refusals mode-neutral
lukaszcz Aug 1, 2026
42f048d
HolRefute: parenthesise the random generator's function point state
lukaszcz Aug 1, 2026
3458628
HolRefute: make every application-argument splice an atom
lukaszcz Aug 1, 2026
19eb7e1
HolRefute examples: re-run 01-08 and 11, reconcile the prose
lukaszcz Aug 1, 2026
9624704
HolRefute examples: re-run 09, 10 and the index, reconcile the prose
lukaszcz Aug 1, 2026
33a2105
HolRefute: size the MF acceptance budgets from measurement
lukaszcz Aug 1, 2026
8f042b0
HolRefute: keep wall-clock out of the substrate conformance verdict
lukaszcz Aug 1, 2026
6179495
HolRefute: cover the non-bitword IntToNat encoding
lukaszcz Aug 1, 2026
32e38bc
HolRefute: match lazy char lists as the datatype they are
lukaszcz Aug 1, 2026
e898d3b
HolRefute: document that backend racing needs --mt
lukaszcz Aug 1, 2026
757301f
HolRefute: take the monotonicity degradation test off the clock
lukaszcz Aug 2, 2026
e868d61
Merge branch 'develop' into nitpick
lukaszcz Aug 2, 2026
1c26e2e
HolRefute: keep internal names and raw exceptions out of reports
lukaszcz Aug 4, 2026
addc323
HolRefute examples: pin the model finder and assert every verdict
lukaszcz Aug 4, 2026
4a19afa
HolRefute examples: close the API gaps and add the library-type file
lukaszcz Aug 4, 2026
cf4c874
HolRefute: decide a spent tactic budget instead of racing it
lukaszcz Aug 4, 2026
3924005
Merge branch 'develop' into nitpick
lukaszcz Aug 5, 2026
fd499a2
revert tttUnfold changes
lukaszcz Aug 5, 2026
bb39ce1
HolRefute: turn examples into theory scripts
lukaszcz Aug 5, 2026
e11c19f
HolRefute: remove stale refuteheap manual reference
lukaszcz Aug 5, 2026
b6fbdae
HolRefute: make tactics the primary interface
lukaszcz Aug 6, 2026
7343cb7
HolRefute: add configurable tactic interface
lukaszcz Aug 6, 2026
42b6209
HolRefute examples: remove redundant imports
lukaszcz Aug 6, 2026
fff11e7
HolRefute: parallelize backend phases by default
lukaszcz Aug 7, 2026
2286551
HolRefute: add time-bounded iterative deepening
lukaszcz Aug 7, 2026
acb8b4e
HolRefute: clarify model-finder outcomes
lukaszcz Aug 7, 2026
afd58af
Add quantified model certificate replay
lukaszcz Aug 8, 2026
59b8ca5
HolRefute: expand model certificate replay
lukaszcz Aug 9, 2026
d187a31
Bound model certification replay preparation
lukaszcz Aug 9, 2026
a99e0cd
HolRefute: simplify model certificate replay
lukaszcz Aug 10, 2026
01ca20b
HolRefute: short-circuit decisive replay evaluation
lukaszcz Aug 10, 2026
6dedff9
HolRefute: share certificate kernel derivations
lukaszcz Aug 10, 2026
b0e8422
HolRefute: keep QC certainty on inconclusive certification
lukaszcz Aug 10, 2026
f686983
HolRefute: unify certification evaluation portfolio
lukaszcz Aug 10, 2026
d1721de
HolRefute: unify Skolem replay metadata
lukaszcz Aug 10, 2026
1971063
HolRefute: canonicalize Skolem origin numbering
lukaszcz Aug 10, 2026
aab6fb3
HolRefute: test Skolem preprocessing replay pairing
lukaszcz Aug 10, 2026
354c630
Merge branch 'develop' into nitpick
lukaszcz Aug 10, 2026
2b091e8
HolRefute: document monotone QC certification
lukaszcz Aug 10, 2026
ba14fc2
ParList: keep masked joins observant of Ctrl-C
lukaszcz Aug 10, 2026
7b48e22
HolRefute: surface cleanup and solver-parse failures faithfully
lukaszcz Aug 10, 2026
e3d2c85
HolRefute: share the constructor-pattern recogniser, drop dead code
lukaszcz Aug 10, 2026
46ad166
cv_compute: keep auxiliary translations free of preconditions
lukaszcz Aug 10, 2026
1cca601
HolRefute: avoid idle solver reap and rerun selftests
lukaszcz Aug 10, 2026
04b31cf
HolRefute docs: catch up with the implemented semantics
lukaszcz Aug 10, 2026
6905dfd
HolRefute: unify search-frontier messages on 'searched up to size'
lukaszcz Aug 10, 2026
fa603c7
Fix nested binary datatype model reconstruction
lukaszcz Aug 10, 2026
de8235d
Tighten HolRefute example commentary
lukaszcz Aug 11, 2026
682876d
HolRefute: reserve NoCounterexample for total search
lukaszcz Aug 12, 2026
1642146
HolRefute: keep totality results sound
lukaszcz Aug 13, 2026
e1dd0f5
HolRefute: replay partially reconstructed models
lukaszcz Aug 14, 2026
ec6d287
Merge branch 'develop' into nitpick
lukaszcz Aug 14, 2026
a441700
HolRefute: evaluate certified Skolem terms
lukaszcz Aug 14, 2026
609c3e6
Fix extracted function-valued definition arity
lukaszcz Aug 14, 2026
bf26c6a
HolRefute: close supervisor startup cancellation race
lukaszcz Aug 14, 2026
f48ff92
Certify QC candidates through universal PNF
lukaszcz Aug 14, 2026
f3d981b
Improve Boolean counterexample rendering
lukaszcz Aug 17, 2026
545099d
Merge branch 'develop' into nitpick
lukaszcz Aug 17, 2026
0b9b7c9
HolRefute: one signature per .sig file for the help DB
lukaszcz Aug 17, 2026
36007ca
HolRefute: drop the unreachable mosml selftest.exe rule
lukaszcz Aug 17, 2026
af15fee
HolRefute: drop the unimplemented use_subtype and allow_function_inve…
lukaszcz Aug 17, 2026
d513fbf
HolRefute: stop accepting an ignored partial field in register_quotient
lukaszcz Aug 17, 2026
afb793a
HolRefute: correct comments claiming compatibility obligations
lukaszcz Aug 17, 2026
e176fd7
HolRefute: fold upd_backends into the typed upd_search
lukaszcz Aug 17, 2026
c7e71a7
HolRefute: instantiate a word's symbolic width to an fcp numeral type
lukaszcz Aug 17, 2026
9570f47
HolRefute: give the model finder a native machine-word carrier
lukaszcz Aug 17, 2026
fa982a1
HolRefute: make the docs describe the code as it is
lukaszcz Aug 17, 2026
93974fa
HolRefute: read a character as a carrier, not a typedef over num
lukaszcz Aug 17, 2026
c104fc3
HolRefute: reach WF through a wf' ersatz
lukaszcz Aug 17, 2026
79fa80d
HolRefute: guard the Hilbert-choice encoding against an out-of-scope …
lukaszcz Aug 18, 2026
879473f
HolRefute: encode SUM_IMAGE through a witness-list surrogate
lukaszcz Aug 18, 2026
3daee96
HolRefute: box a goal free variable the same way in every formula
lukaszcz Aug 18, 2026
529adef
HolRefute: give WFREC a guarded ersatz that ties its own knot
lukaszcz Aug 19, 2026
400e725
HolRefute: say what the wfrec' rows actually do, and pin the real stage
lukaszcz Aug 19, 2026
b784067
HolRefute: recognize hand-rolled lfp/gfp definitions
lukaszcz Aug 19, 2026
3d3c71c
HolRefute: let callers register a codatatype, and check the witness
lukaszcz Aug 19, 2026
5efd658
HolRefute: harvest a typedef whose bijection halves are saved apart
lukaszcz Aug 19, 2026
d919f50
HolRefute: give the model finder an opt-in real Frac carrier
lukaszcz Aug 20, 2026
e7f8d02
HolRefute: certify real-via-Frac counterexamples
lukaszcz Aug 20, 2026
d999b49
HolRefute: register the real Frac carrier by default
lukaszcz Aug 20, 2026
6d621b7
HolRefute: give quickcheck a built-in :rat generator
lukaszcz Aug 21, 2026
4882e1b
HolRefute: give quickcheck a built-in :real generator
lukaszcz Aug 21, 2026
77e5228
HolRefute: pin the rat and real totality rule on both backends
lukaszcz Aug 21, 2026
d157049
HolRefute: move the selftest and its fixtures into tests/
lukaszcz Aug 21, 2026
2e635e0
HolRefute: quickcheck finite maps through a generator family
lukaszcz Aug 21, 2026
a4ee054
HolRefute: give the model finder a finite-map route
lukaszcz Aug 22, 2026
b2ce591
HolRefute: correct the fmap typedef's axioms and its own account of i…
lukaszcz Aug 22, 2026
a1a5ca1
HolRefute: let random QC test datatypes recursive under a function type
lukaszcz Aug 22, 2026
2305b4d
HolRefute: let QC pin type variables individually
lukaszcz Aug 22, 2026
41a4947
HolRefute: transport a generator-less typedef goal to its representation
lukaszcz Aug 23, 2026
0bee04a
HolRefute: replace the transport contraction walker; pin transport mo…
lukaszcz Aug 24, 2026
1fd05b5
HolRefute: rewrite bounded quantifiers over an offset interval
lukaszcz Aug 24, 2026
799404b
HolRefute: count QC candidates honestly, three ways
lukaszcz Aug 24, 2026
6bd2dac
HolRefute: report the candidate counters on a witness-less search
lukaszcz Aug 25, 2026
15bf179
HolRefute: one display walk for counterexamples and models alike
lukaszcz Aug 25, 2026
0a21380
HolRefute: infer the modes in which a relation's complement decides
lukaszcz Aug 25, 2026
07d2b98
HolRefute: compile a negated relational premise to its complement
lukaszcz Aug 25, 2026
404e143
HolRefute: infer higher-order smart-generator modes
lukaszcz Aug 25, 2026
218dc9b
HolRefute: specialise a relation on a closed higher-order argument
lukaszcz Aug 26, 2026
e2e413d
HolRefute: correct prose left behind by the specialisation work
lukaszcz Aug 26, 2026
53781c2
HolRefute: key a relation by predicate or function graph
lukaszcz Aug 26, 2026
28d4a5c
HolRefute: synthesise a function's graph clauses and mode-check them
lukaszcz Aug 26, 2026
f91d39b
HolRefute: consume a goal premise by inverting its function graph
lukaszcz Aug 26, 2026
8593ee4
HolRefute: pin the predicate compiler's soundness at level 2
lukaszcz Aug 27, 2026
2a3342f
HolRefute: stop a certificate pin from racing the backend pool
lukaszcz Aug 27, 2026
4d96837
HolRefute: name the real reason a dependent-bound goal is uncertified
lukaszcz Aug 27, 2026
3a90dbf
HolRefute: make four soundness counterparts able to fail
lukaszcz Aug 27, 2026
6fe4565
HolRefute: make the soundness counterparts' comments true
lukaszcz Aug 28, 2026
d0b6224
HolRefute: correct what the finite-map pins claim about their counts
lukaszcz Aug 28, 2026
f25bc2e
HolRefute: say what actually stops the dependent-bound pin certifying
lukaszcz Aug 28, 2026
e48fe42
HolRefute: measure the graph-inversion twin in one run
lukaszcz Aug 28, 2026
3fe44c7
HolRefute: anchor the twin's second counter to its own line
lukaszcz Aug 28, 2026
5584571
HolRefute: require the model-finder twins to finish their scopes
lukaszcz Aug 28, 2026
7f9aca6
HolRefute: record the model-finder twins' timeout headroom
lukaszcz Aug 28, 2026
976dbc8
HolRefute: widen the split-typedef scope and share the finished check
lukaszcz Aug 28, 2026
fee4f2a
HolRefute: state inherited limitations, retire a resolved follow-up
lukaszcz Aug 28, 2026
22e3496
HolRefute: correct the essential-existential limitation's verdict
lukaszcz Aug 28, 2026
ed47aaa
HolRefute: fix width, recursion, and snapshot regressions
lukaszcz Aug 28, 2026
864b3f5
HolRefute: share duplicated helpers and drop repeated work
lukaszcz Aug 28, 2026
22d440b
HolRefute: merge the two mode fixpoints and fold repeated shapes
lukaszcz Aug 29, 2026
95abe0f
Merge branch 'develop' into nitpick
lukaszcz Aug 29, 2026
23fae45
HolRefute: share duplicated logic and drop repeated work
lukaszcz Aug 29, 2026
2aabcf1
HolRefute: share duplicated logic, and quiet the default trace
lukaszcz Aug 31, 2026
0d51580
Add HolRefute AA tree case study
lukaszcz Aug 31, 2026
d4270c4
Add HolRefute AVL case study
lukaszcz Aug 31, 2026
9fe95da
Add de Bruijn substitution refutation example
lukaszcz Aug 31, 2026
70b1395
Add context-free grammar refutation example
lukaszcz Aug 31, 2026
816e23b
Clarify grammar soundness diagnostic
lukaszcz Aug 31, 2026
aeed9c0
Clarify grammar diagnostic outcome
lukaszcz Aug 31, 2026
d4d9c48
Complete grammar soundness diagnostic
lukaszcz Aug 31, 2026
5aa0857
Add security typing HolRefute case study
lukaszcz Aug 31, 2026
d74da90
Document AA-tree wellformedness diagnostic
lukaszcz Aug 31, 2026
0894b45
Document hotel feels-safe stretch fallback
lukaszcz Aug 31, 2026
341c36f
Document grammar completeness fallback
lukaszcz Aug 31, 2026
471ab67
Add two-list queue case study and document the series
lukaszcz Aug 31, 2026
3e67c92
Refute the AA-tree wellformedness equation
lukaszcz Sep 1, 2026
1fafa2a
HolRefute: define generator bundles one clique at a time
lukaszcz Sep 1, 2026
71276d8
HolRefute examples: run the diagnostics on the real conjectures
lukaszcz Sep 1, 2026
1798c89
update .gitignore
lukaszcz Sep 1, 2026
6be995f
HolRefute: one policy literal, one spelling of the carrier names
lukaszcz Sep 1, 2026
61afbe2
HolRefute: keep the extraction template under 80 columns
lukaszcz Sep 1, 2026
e97eb09
Merge branch 'develop' into nitpick
lukaszcz Sep 1, 2026
64596ce
HolRefute manual: lead with the tactics, not the SML layer
lukaszcz Sep 1, 2026
bd5f5fd
HolRefute Docfiles: document the configurable tactics
lukaszcz Sep 1, 2026
f6224f5
HolRefute: keep the private theory bracket quiet
lukaszcz Sep 1, 2026
fe58af3
HolRefute: cv declines while a goalstack tactic holds the proof manager
lukaszcz Sep 1, 2026
551169f
realSimps: constrain let_id's variable instead of guessing it
lukaszcz Sep 2, 2026
2ba5db2
HolRefute: cv pre-flights the goal's functions before synthesizing
lukaszcz Sep 2, 2026
43aef0b
HolRefute: keep the rat equality conv off other types
lukaszcz Sep 2, 2026
e309448
Merge branch 'develop' into nitpick
lukaszcz Sep 2, 2026
a093761
HolRefute: let REFUTE_TAC keep what its backends find
lukaszcz Sep 2, 2026
d6c3811
HolRefute: extract membership as the application IN_DEF says it is
lukaszcz Sep 2, 2026
b6b5a32
remove comment
lukaszcz Sep 2, 2026
c644434
HolRefute: keep backend deadlines within call budget
lukaszcz Sep 2, 2026
c8bc036
HolRefute: trim the selftest to user-visible behaviour
lukaszcz Sep 2, 2026
06e5b9c
HolRefute: remove dead code and duplication, trim README
lukaszcz Sep 2, 2026
d7ad7b3
HolRefute: drop extension-API entry points with no caller
lukaszcz Sep 2, 2026
1445a8d
HolRefute docs: tighten the Docfiles and manual chapter
lukaszcz Sep 3, 2026
60cf651
HolRefute: serialize trace output across backend workers
lukaszcz Sep 3, 2026
d2ed299
HolRefute: key narrowing reconstruction on the alternative id
lukaszcz Sep 3, 2026
43e5236
HolRefute: cleanup pass over the recent Refute changes
lukaszcz Sep 3, 2026
028f1d2
HolRefute: drop the unreachable monotonicity trace
lukaszcz Sep 3, 2026
c735f95
HolRefute: one builder for function updates
lukaszcz Sep 3, 2026
c6c2849
HolRefute: decide ground finite-map equality on the compute substrate
lukaszcz Sep 3, 2026
b08316e
ParList: defer rather than refuse interrupts in the masked windows
lukaszcz Sep 4, 2026
f6ae9ca
HolRefute: final review pass, and drop the Cv substrate
lukaszcz Sep 4, 2026
10771be
HolRefute: refuse re-entrant Refute, and drop the machinery for it
lukaszcz Sep 4, 2026
2ea85f7
HolRefute: charge each quantifier its own cardinality
lukaszcz Sep 4, 2026
f4b6ddd
HolRefute: documentation accuracy and concision pass
lukaszcz Sep 4, 2026
4be84f7
Merge branch 'develop' into nitpick
lukaszcz Sep 4, 2026
430cc71
HolRefute: correct the port-fidelity claims in headers, comments and …
lukaszcz Sep 4, 2026
93c57ee
HolRefute: build under the otknl kernel too
lukaszcz Sep 4, 2026
1186e73
Manual/Reference: support Pandoc tables
lukaszcz Sep 4, 2026
3a6efcc
Merge branch 'develop' into nitpick
lukaszcz Sep 7, 2026
a30d23b
Merge branch 'develop' into nitpick
mn200 Sep 10, 2026
403d532
Merge branch 'develop' into nitpick
lukaszcz Sep 16, 2026
414fb32
Fix HolRefute tactic context handling
lukaszcz Sep 16, 2026
6192d6a
Merge branch 'develop' into nitpick
lukaszcz Sep 22, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions AGENTS.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
CLAUDE.md
2 changes: 2 additions & 0 deletions Manual/Description/.gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ drules.tex
HolSat.tex
HolQbf.tex
HolSmt.tex
Refute.tex
QuantHeuristics.tex
enumfset.tex
libraries.tex
Expand All @@ -26,6 +27,7 @@ PatternMatchesLib.md
HolSat.md
HolQbf.md
HolSmt.md
Refute.md
QuantHeuristics.md
enumfset.md
modern-syntax.tex
Expand Down
Loading
Loading