diff --git a/Testimony/Semantics/Meaning.lean b/Testimony/Semantics/Meaning.lean index 73b51b0..038a730 100644 --- a/Testimony/Semantics/Meaning.lean +++ b/Testimony/Semantics/Meaning.lean @@ -108,13 +108,203 @@ def pairsOf {β : Type} : List β → List (β × β) | x :: xs => xs.map (x, ·) ++ pairsOf xs /-- **Every pair of claims whose meanings exclude each other**, under a given -ontology: `(a, b)`, with `a` listed before `b`, when the two meanings, read for -what their words mean, cannot both be held. -/ -def exclusionsUnder [DecidableEq α] (O : Ontology) : List (α × α) := +ontology, by definition: `(a, b)`, with `a` listed before `b`, when the two +meanings, read for what their words mean, cannot both be held. Every pair is +checked; `exclusionsUnder` computes the same list through shared keys. -/ +def exclusionsByPairs [DecidableEq α] (O : Ontology) : List (α × α) := let shaped := (all : List α).map fun a => (a, Ontology.closed O (means a)) (pairsOf shaped).filterMap fun ((a, s), (b, t)) => if a ≠ b && Ontology.excludes O s t then some (a, b) else none +/-! #### Exclusions through shared keys + +Two coherent meanings clash only where they share a key +(`Testimony.Semantics.Ontology.shares_of_clash`): a fact, or a thing a relation +is about. So the claims are taken from the last to the first, each against an +index from every key to the later claims that hold it, and each claim is +checked only against the claims it shares a key with. A pair sharing nothing is +never compared, which is almost every pair: checking all of them was what made +an argument's joins dear, quadratic in its claims and each check a comparison +of whole facts. The list found is the definition's, pair for pair and in the +same order (`exclusionsUnder_eq`). -/ + +/-- An index from keys to the claims holding them. -/ +abbrev KeyIndex (α : Type) := List (Ontology.Key × List α) + +/-- The claims the index holds under a key. -/ +def KeyIndex.find : KeyIndex α → Ontology.Key → List α + | [], _ => [] + | (k', as) :: rest, k => if k' = k then as else KeyIndex.find rest k + +/-- The index with one more claim under a key. -/ +def KeyIndex.add : KeyIndex α → Ontology.Key → α → KeyIndex α + | [], k, a => [(k, [a])] + | (k', as) :: rest, k, a => + if k' = k then (k', a :: as) :: rest else (k', as) :: KeyIndex.add rest k a + +omit [HasMeanings α] in +theorem KeyIndex.find_add (ix : KeyIndex α) (k k' : Ontology.Key) (a : α) : + KeyIndex.find (KeyIndex.add ix k a) k' = + if k = k' then a :: KeyIndex.find ix k' else KeyIndex.find ix k' := by + induction ix with + | nil => by_cases h : k = k' <;> simp [KeyIndex.add, KeyIndex.find, h] + | cons e rest ih => + obtain ⟨k'', as⟩ := e + by_cases h₁ : k'' = k + · subst h₁ + by_cases h₂ : k'' = k' <;> simp [KeyIndex.add, KeyIndex.find, h₂] + · by_cases h₂ : k'' = k' + · subst h₂ + simp [KeyIndex.add, KeyIndex.find, h₁, Ne.symm h₁] + · simp [KeyIndex.add, KeyIndex.find, h₁, h₂, ih] + +omit [HasMeanings α] in +theorem KeyIndex.mem_find_foldl_add (ks : List Ontology.Key) (a b : α) (k : Ontology.Key) : + ∀ ix : KeyIndex α, b ∈ KeyIndex.find (ks.foldl (fun ix k => KeyIndex.add ix k a) ix) k ↔ + b ∈ KeyIndex.find ix k ∨ (k ∈ ks ∧ b = a) := by + induction ks with + | nil => simp + | cons k₀ ks ih => + intro ix + rw [List.foldl_cons, ih, KeyIndex.find_add] + by_cases h : k₀ = k + · subst h; simp only [if_true, List.mem_cons, true_or, true_and]; tauto + · simp only [h, if_false, List.mem_cons] + constructor + · rintro (h' | ⟨hk, rfl⟩) + · exact .inl h' + · exact .inr ⟨.inr hk, rfl⟩ + · rintro (h' | ⟨hk | hk, rfl⟩) + · exact .inl h' + · exact absurd hk.symm h + · exact .inr ⟨hk, rfl⟩ + +/-- The exclusions among a list of claims, each with its meaning read under the +ontology, and the index of the coherent ones by key: the claims from the last +to the first, each checked against the later claims it shares a key with. Each +meaning is read once, before the walk, and not once for every pair. -/ +def exclusionsGo [DecidableEq α] (O : Ontology) : + List (α × Shape) → List (α × α) × KeyIndex α + | [] => ([], []) + | (a, s) :: ys => + match exclusionsGo O ys with + | (acc, ix) => + let c := Ontology.coherent O s + let ks := Ontology.keysOf s + let near := if c then ks.flatMap (KeyIndex.find ix) else [] + let found := ys.filterMap fun (b, t) => + if near.contains b && a ≠ b && Ontology.clash O (s.lits ++ t.lits) (s.nogoods ++ t.nogoods) + then some (a, b) else none + (found ++ acc, if c then ks.foldl (fun ix k => KeyIndex.add ix k a) ix else ix) + +/-- Each claim with its meaning read under the ontology. -/ +def shapedUnder (O : Ontology) (xs : List α) : List (α × Shape) := + xs.map fun a => (a, Ontology.closed O (means a)) + +theorem mem_find_exclusionsGo [DecidableEq α] (O : Ontology) (k : Ontology.Key) (b : α) : + ∀ xs : List α, b ∈ KeyIndex.find (exclusionsGo O (shapedUnder O xs)).2 k ↔ + b ∈ xs ∧ Ontology.coherent O (Ontology.closed O (means b)) = true ∧ + k ∈ Ontology.keysOf (Ontology.closed O (means b)) + | [] => by simp [shapedUnder, exclusionsGo, KeyIndex.find] + | a :: xs => by + have ih := mem_find_exclusionsGo O k b xs + simp only [shapedUnder, List.map_cons, exclusionsGo] at ih ⊢ + split + · rename_i hc + rw [KeyIndex.mem_find_foldl_add, ih] + constructor + · rintro (⟨hb, hcb, hkb⟩ | ⟨hk, rfl⟩) + · exact ⟨List.mem_cons_of_mem _ hb, hcb, hkb⟩ + · exact ⟨List.mem_cons_self, hc, hk⟩ + · rintro ⟨hb, hcb, hkb⟩ + rcases List.mem_cons.mp hb with rfl | hb + · exact .inr ⟨hkb, rfl⟩ + · exact .inl ⟨hb, hcb, hkb⟩ + · rename_i hc + rw [ih] + constructor + · rintro ⟨hb, hcb, hkb⟩ + exact ⟨List.mem_cons_of_mem _ hb, hcb, hkb⟩ + · rintro ⟨hb, hcb, hkb⟩ + rcases List.mem_cons.mp hb with rfl | hb + · exact absurd hcb (by simpa using hc) + · exact ⟨hb, hcb, hkb⟩ + +theorem exclusionsGo_fst [DecidableEq α] (O : Ontology) : ∀ xs : List α, + (exclusionsGo O (shapedUnder O xs)).1 = + (pairsOf (shapedUnder O xs)).filterMap + fun ((a, s), (b, t)) => if a ≠ b && Ontology.excludes O s t then some (a, b) else none + | [] => rfl + | a :: xs => by + have ih := exclusionsGo_fst O xs + have hmem := fun k b => mem_find_exclusionsGo O k b xs + rcases h : exclusionsGo O (shapedUnder O xs) with ⟨acc, ix⟩ + rw [h] at ih hmem + simp only at ih hmem + have hcons : shapedUnder O (a :: xs) = (a, Ontology.closed O (means a)) :: shapedUnder O xs := + rfl + rw [hcons] + simp only [exclusionsGo, h, pairsOf, List.filterMap_append, List.filterMap_map, ← ih] + simp only [shapedUnder, List.filterMap_map] + congr 1 + apply List.filterMap_congr + intro b hb + simp only [Function.comp_apply, Ontology.excludes] + by_cases hca : Ontology.coherent O (Ontology.closed O (means a)) = true + · by_cases hcb : Ontology.coherent O (Ontology.closed O (means b)) = true + · have hnear : ((Ontology.keysOf (Ontology.closed O (means a))).flatMap + (KeyIndex.find ix)).contains b = + (Ontology.keysOf (Ontology.closed O (means a))).any + (· ∈ Ontology.keysOf (Ontology.closed O (means b))) := by + apply Bool.eq_iff_iff.mpr + simp only [List.contains_iff_mem, List.mem_flatMap, List.any_eq_true, decide_eq_true_eq, + hmem] + constructor + · rintro ⟨k, hk, -, -, hkb⟩; exact ⟨k, hk, hkb⟩ + · rintro ⟨k, hk, hkb⟩; exact ⟨k, hk, hb, hcb, hkb⟩ + simp only [hca, hcb, if_true, hnear, Bool.true_and] + by_cases hcl : Ontology.clash O ((Ontology.closed O (means a)).lits ++ + (Ontology.closed O (means b)).lits) ((Ontology.closed O (means a)).nogoods ++ + (Ontology.closed O (means b)).nogoods) = true + · have hsa : Ontology.clash O (Ontology.closed O (means a)).lits + (Ontology.closed O (means a)).nogoods = false := by + simp only [Ontology.coherent, Bool.and_eq_true, Bool.not_eq_true'] at hca; exact hca.2 + have hsb : Ontology.clash O (Ontology.closed O (means b)).lits + (Ontology.closed O (means b)).nogoods = false := by + simp only [Ontology.coherent, Bool.and_eq_true, Bool.not_eq_true'] at hcb; exact hcb.2 + obtain ⟨k, hk, hkb⟩ := Ontology.shares_of_clash hsa hsb hcl + have : (Ontology.keysOf (Ontology.closed O (means a))).any + (· ∈ Ontology.keysOf (Ontology.closed O (means b))) = true := + List.any_eq_true.mpr ⟨k, hk, by simpa using hkb⟩ + simp only [this, hcl, Bool.true_and, Bool.and_true] + · simp only [Bool.not_eq_true] at hcl + simp [hcl] + · simp only [Bool.not_eq_true] at hcb + have hnear : ((Ontology.keysOf (Ontology.closed O (means a))).flatMap + (KeyIndex.find ix)).contains b = false := by + apply Bool.eq_false_iff.mpr + intro hc + obtain ⟨k, -, hk⟩ := List.mem_flatMap.mp (List.contains_iff_mem.mp hc) + obtain ⟨-, hcb', -⟩ := (hmem k b).mp hk + simp [hcb] at hcb' + simp only [hca, if_true, hnear, hcb, Bool.false_and, Bool.and_false, Bool.false_eq_true, + if_false] + · simp only [Bool.not_eq_true] at hca + simp [hca] + +/-- **Every pair of claims whose meanings exclude each other**, under a given +ontology: `(a, b)`, with `a` listed before `b`, when the two meanings, read for +what their words mean, cannot both be held. Computed through shared keys, and +the same list as the definition, `exclusionsByPairs` (`exclusionsUnder_eq`). -/ +def exclusionsUnder [DecidableEq α] (O : Ontology) : List (α × α) := + (exclusionsGo O (shapedUnder O (all : List α))).1 + +/-- **The exclusions through shared keys are the exclusions**, pair for pair and +in the same order. -/ +theorem exclusionsUnder_eq [DecidableEq α] (O : Ontology) : + exclusionsUnder (α := α) O = exclusionsByPairs O := + exclusionsGo_fst O _ + /-- **Every pair of claims whose meanings entail one another**, under a given ontology: `(a, b)` when the meaning of `a`, read for what its words mean, asserts everything the meaning of `b` does. -/ diff --git a/Testimony/Semantics/Ontology.lean b/Testimony/Semantics/Ontology.lean index 815852e..12a8bf6 100644 --- a/Testimony/Semantics/Ontology.lean +++ b/Testimony/Semantics/Ontology.lean @@ -297,6 +297,106 @@ for what its words mean, every literal of the other and every nogood. -/ def entails (O : Ontology) (s t : Shape) : Bool := coherent O s && t.read && t.lits.all s.lits.contains && t.nogoods.all s.nogoods.contains +/-! ### Where two meanings can meet + +Two meanings can clash only where they touch. A literal meets its negation in +the same fact; a definition's rule (**only**, **functional**) relates two facts +about the same thing; a nogood is completed by the other meaning's literal. +So a meaning's **keys** are the facts of its literals and nogoods, and the +things its relations are about, and two coherent meanings that share no key +cannot clash (`shares_of_clash`). A claim is then checked only against the +claims it shares a key with, found through an index of keys, rather than +against every claim (`Testimony.Semantics.HasMeanings.exclusionsUnder`). -/ + +/-- Where a meaning can meet another: a fact, or a thing a relation is about. -/ +inductive Key + /-- A fact a literal affirms or denies. -/ + | fact (f : Fact) + /-- A thing a relation is about. -/ + | term (t : Term) +deriving DecidableEq + +/-- The keys of one fact: itself, and the things it relates, if a relation. -/ +def factKeys : Fact → List Key + | f@(.rel _ a b) => [.fact f, .term a, .term b] + | f => [.fact f] + +/-- **The keys of a meaning**: those of every fact it affirms or denies, and of +every fact in its nogoods. -/ +def keysOf (s : Shape) : List Key := + s.lits.flatMap (fun l => factKeys l.fact) ++ s.nogoods.flatMap (·.map fun l => Key.fact l.fact) + +theorem fact_mem_factKeys (f : Fact) : Key.fact f ∈ factKeys f := by + cases f <;> simp [factKeys] + +theorem mem_keysOf_of_lit {s : Shape} {l : Lit} {k : Key} (hl : l ∈ s.lits) + (hk : k ∈ factKeys l.fact) : k ∈ keysOf s := by + simp only [keysOf, List.mem_append, List.mem_flatMap] + exact .inl ⟨l, hl, hk⟩ + +theorem mem_keysOf_of_nogood {s : Shape} {n : List Lit} {x : Lit} (hn : n ∈ s.nogoods) + (hx : x ∈ n) : Key.fact x.fact ∈ keysOf s := by + simp only [keysOf, List.mem_append, List.mem_flatMap, List.mem_map] + exact .inr ⟨n, hn, x, hx, rfl⟩ + +/-- A definition's rule makes two literals clash only when their relations are +about one same thing. -/ +theorem shares_of_clashes {a : Axiom} {l m : Lit} (h : a.clashes l m = true) : + ∃ t, Key.term t ∈ factKeys l.fact ∧ Key.term t ∈ factKeys m.fact := by + unfold Axiom.clashes at h + split at h + · rename_i _ _ _ _ b _ _ d + simp only [Bool.and_eq_true, beq_iff_eq, bne_iff_ne, ne_eq] at h + obtain ⟨⟨⟨-, -⟩, hbd⟩, -⟩ := h + exact ⟨b, by simp [factKeys], by simp [factKeys, hbd]⟩ + · rename_i _ _ a _ _ c _ + simp only [Bool.and_eq_true, beq_iff_eq, bne_iff_ne, ne_eq] at h + obtain ⟨⟨⟨-, -⟩, hac⟩, -⟩ := h + exact ⟨a, by simp [factKeys], by simp [factKeys, hac]⟩ + · simp at h + +/-- **Two coherent meanings that clash share a key.** A clash between them is +a literal and its negation, two literals a rule sets against each other, or a +nogood of one completed by the other; none of these is inside one meaning alone, +since each is coherent, so each joins the two, at a fact or at a thing their +relations are about. -/ +theorem shares_of_clash {O : Ontology} {s t : Shape} (hs : clash O s.lits s.nogoods = false) + (ht : clash O t.lits t.nogoods = false) + (h : clash O (s.lits ++ t.lits) (s.nogoods ++ t.nogoods) = true) : + ∃ k ∈ keysOf s, k ∈ keysOf t := by + simp only [clash, Bool.or_eq_false_iff, Bool.or_eq_true, List.any_eq_false, List.any_eq_true, + List.all_eq_true, List.contains_iff_mem, List.mem_append, Bool.not_eq_true] at hs ht h + obtain ⟨⟨hs₁, hs₂⟩, hs₃⟩ := hs + obtain ⟨⟨ht₁, ht₂⟩, ht₃⟩ := ht + rcases h with (⟨l, hl, hn⟩ | ⟨l, hl, m, hm, d, hd, hc⟩) | ⟨n, hn, hall⟩ + · -- a literal and its negation + rcases hl with hl | hl <;> rcases hn with hn | hn + · exact absurd (by simpa using hn) (hs₁ l hl) + · exact ⟨_, mem_keysOf_of_lit hl (fact_mem_factKeys _), + mem_keysOf_of_lit hn (fact_mem_factKeys _)⟩ + · exact ⟨_, mem_keysOf_of_lit hn (fact_mem_factKeys _), + mem_keysOf_of_lit hl (fact_mem_factKeys _)⟩ + · exact absurd (by simpa using hn) (ht₁ l hl) + · -- a rule setting two literals against each other + obtain ⟨u, hu₁, hu₂⟩ := shares_of_clashes hc + rcases hl with hl | hl <;> rcases hm with hm | hm + · exact absurd ⟨m, hm, d, hd, hc⟩ (hs₂ l hl) + · exact ⟨_, mem_keysOf_of_lit hl hu₁, mem_keysOf_of_lit hm hu₂⟩ + · exact ⟨_, mem_keysOf_of_lit hm hu₂, mem_keysOf_of_lit hl hu₁⟩ + · exact absurd ⟨m, hm, d, hd, hc⟩ (ht₂ l hl) + · -- a nogood completed across the two + rcases hn with hn | hn + · obtain ⟨x, hx, hxs⟩ : ∃ x ∈ n, x ∉ s.lits := + Classical.byContradiction fun hno => + hs₃ n hn fun x hx => Classical.byContradiction fun hxs => hno ⟨x, hx, hxs⟩ + have hxt : x ∈ t.lits := (hall x hx).resolve_left hxs + exact ⟨_, mem_keysOf_of_nogood hn hx, mem_keysOf_of_lit hxt (fact_mem_factKeys _)⟩ + · obtain ⟨x, hx, hxt⟩ : ∃ x ∈ n, x ∉ t.lits := + Classical.byContradiction fun hno => + ht₃ n hn fun x hx => Classical.byContradiction fun hxt => hno ⟨x, hx, hxt⟩ + have hxs : x ∈ s.lits := (hall x hx).resolve_right hxt + exact ⟨_, mem_keysOf_of_lit hxs (fact_mem_factKeys _), mem_keysOf_of_nogood hn hx⟩ + end Ontology end Testimony.Semantics diff --git a/arguments/TestimonyArguments/Checks.lean b/arguments/TestimonyArguments/Checks.lean index 3d4c82f..fd4161c 100644 --- a/arguments/TestimonyArguments/Checks.lean +++ b/arguments/TestimonyArguments/Checks.lean @@ -101,7 +101,7 @@ The canonical witness #check_refutations under TestimonyArguments using unfoldSets /-- -info: every entry is a tagged definition, and every key names one: 2298 definitions, 176 entries +info: every entry is a tagged definition, and every key names one: 2319 definitions, 176 entries -/ #guard_msgs in #check_citations under Testimony diff --git a/arguments/bench/Engine.lean b/arguments/bench/Engine.lean index 3fcb072..f530e6b 100644 --- a/arguments/bench/Engine.lean +++ b/arguments/bench/Engine.lean @@ -33,6 +33,8 @@ The benchmarks, from the smallest unit up: arguments' own tables are proved; and a row of a hearing, where every party's inferences are re-rated under a standard, with the parties' re-rated strengths; - **a verdict**: the solver's checked witness for each of the two disputes; +- **the joins**: the exclusions among sola fide's 111 claims, read for what + their words mean; - **an assessment** and **a rating**: Miller's dissent, searched and certified, and the laws' step; - **`establish`** on a package, the tactic every package's soundness uses; @@ -255,6 +257,10 @@ example (j : JamesParty) : (rerated_strength .evidence .trentOnTheWord) (rerated_strength .evidence j) ?_ cases j <;> horn_certify +#bench (runs := 1) "joins: sola fide exclusions, 111 claims" in +example : (Testimony.Semantics.HasMeanings.exclusions (α := Claim)).length = 6 := by + decide +kernel + #bench "verdict: sola fide, only Paul's word unanswered" in example : Verdict solaFideDispute where finite := solaFideFinite diff --git a/docs/src/performance.md b/docs/src/performance.md index 83aad5a..80100d4 100644 --- a/docs/src/performance.md +++ b/docs/src/performance.md @@ -76,6 +76,38 @@ The slowest modules of the arguments' build: `SolaFide.Ratings` (150 s), | 4 | Certify assessments and consistency; in a hearing, weigh a step's rank only once it is attacked (#183) | the hearings and assessments | 3.08 s, 97 MiB | 0.48 s, 16 MiB | 0.008 | kept | | 5 | Compare a citation by its key and locus, a key checked to name one entry | a hearing's rerated strengths | 2.54 s, 83 MiB | 0.86 s, 25 MiB | 0.008 | kept | | 6 | Replay a refutation on bitmasks (#180) | the certified defeat tables | 7.21 s, 94 MiB | 5.99 s, 70 MiB | 0.008 | kept | +| 7 | Find exclusions through shared keys, not every pair | the sola fide joins | 45.4 s, 3.43 GiB | 10.6 s, 1.06 GiB | 0.008 | kept | + +Round 7, `scripts/bench-ab.sh` against `main`, five interleaved rounds. A +profile of `Meanings.SolaFide` put 51 of its 64 seconds in one proof: that the +pinned exclusions are what the meanings contain, which the kernel checked by +testing every one of the 6105 pairs of the argument's 111 claims for a clash. +Two first guesses were wrong, and are recorded so that nobody tries them again: +that the kernel closed each meaning again for every pair (a table of closed +meanings, and one of their coherence, each checked once, changed nothing, +44 s), and that the closing was the cost (it is 0.4 s for every claim). The +cost was the clash check itself, comparing whole facts and terms a field at a +time, some 400,000 comparisons. Two coherent meanings can clash only where they +share a key, a fact or a thing their relations are about +(`Ontology.shares_of_clash`), so the claims are now taken from the last to the +first against an index of the later claims' keys, and each is checked only +against those it shares a key with; `HasMeanings.exclusionsUnder_eq` proves the +list the same, pair for pair and in order. The first version walked the claims +themselves and closed each later claim's meaning again for every claim before +it. The kernel shares those repeated terms, so its build was not slowed, but +the ontology check runs the same function compiled, once for every +definition, and there each closing was paid again: CI's gate found that check +5% slower (p = 0.008). So each meaning is now closed once, before the walk +(`HasMeanings.shapedUnder`). The exclusions fell from 45.4 s to 10.6 s (−77%, +p = 0.008) and from 3.43 to 1.06 GiB, and the ontology check from 3.16 s to +1.69 s (−47%, p = 0.008). The entailments were tried +the same way, indexed by each claim's first literal, and gained only 9.7 s to +8.3 s: their check already stops at the first missing literal, so the pairs +themselves are the cost, and the index does not remove them. They are left as +they are. Measured by hand on the first version, clean, on the same machine: the arguments' +`lake build` fell from 225 s to 204 s and its peak from 13.8 to 10.9 GiB, and +the kernel replay's peak from 9.3 to 6.9 GiB, at 226 s: the exclusions proof +was the largest single holder of memory in either. Round 6, `scripts/bench-ab.sh` against `main`, five interleaved rounds. A certified refutation was replayed over lists of settled atoms, each membership @@ -165,7 +197,7 @@ of memory. Two run in 293 s; one in 500 s with about 5.2 GiB. ## Fixed points -None yet. After round 6 the largest benchmarks are still the defeat tables, -about 80 ms a sola fide cell, of which converting each position to clauses and -the search at elaboration are now most; and the slowest modules of the build -are the meanings of sola fide and its dispute. +None yet. After round 7 the sola fide joins take 25 s of their module, of which +the entailments are 9 s; the next candidates are the support and part-of tables, +which still search in the kernel, and the models `satisfied_by` checks with +`simp`. diff --git a/docs/src/semantics.md b/docs/src/semantics.md index 34817d8..7a491b9 100644 --- a/docs/src/semantics.md +++ b/docs/src/semantics.md @@ -123,6 +123,17 @@ all, how many claims use each defined word as doctrine or of a text or voice, an each definition contributes: those found with it and not with it taken out. It fails the build if any meaning contradicts itself. +**How the exclusions are found.** Two meanings can clash only where they touch: a literal +meets its negation in one fact, a definition's rule relates two facts about one thing, a +nogood is completed by the other meaning's literal. So each meaning's **keys** are its facts +and the things its relations are about, and two coherent meanings that share no key cannot +exclude each other (`Testimony.Semantics.Ontology.shares_of_clash`). The claims are taken one +by one against an index of the keys of the claims after them, and each is checked only against +those it shares a key with, not against every claim. The list found is the definition's, pair +for pair and in order (`Testimony.Semantics.HasMeanings.exclusionsUnder_eq`), and it is +checked by the kernel in a fraction of the time: every pair compared, the sola fide joins took +the kernel 51 seconds. + The first article, `Testimony.Ontology.Relations`, writes out three definitions the vocabulary already gave in words: "not a ground" is the denial of "a ground"; the only means of a thing is a means of it, and nothing else is; the whole ground of a thing is a ground of it, and nothing