The membership families: two memberships of one term whose types a separation holds
apart (disjoint), a membership beside a denial of a supertype of its type
(supertype), and a membership under a cover's whole beside a denial of each part
(covering), placed as nogoods (chain/place-memberships!). See docs/nmtms.md, "A
nogood placed as a conclusion".
The membership families: two memberships of one term whose types a separation holds apart (`disjoint`), a membership beside a denial of a supertype of its type (`supertype`), and a membership under a cover's whole beside a denial of each part (`covering`), placed as nogoods (`chain/place-memberships!`). See docs/nmtms.md, "A nogood placed as a conclusion".
(exempt-at? tax recs members up)Does a reader with ancestor set up read no separation of the membership nogood
members while the KB stores a siblingDisjointException: two memberships of one term
whose types tax/disjoint? over up does not separate, or two or more memberships of
one term refuting a cover through a separation the reader reads no cover refutation of
(cover-convicted-at?). An exception the reader sees removes a separation its
placement reads, the one read below a placement that seeing more takes away
(docs/taxonomy.md). False for any other nogood.
Does a reader with ancestor set `up` read no separation of the membership nogood `members` while the KB stores a `siblingDisjointException`: two memberships of one term whose types `tax/disjoint?` over `up` does not separate, or two or more memberships of one term refuting a cover through a separation the reader reads no cover refutation of (`cover-convicted-at?`). An exception the reader sees removes a separation its placement reads, the one read below a placement that seeing more takes away (docs/taxonomy.md). False for any other nogood.
The membership family's entry in decide/registry. Recover keeps the entries of the
terms recovered-terms names that held? holds, with no separation read: the first
read after it tests every pair once (sync-memberships).
The membership family's entry in `decide/registry`. Recover keeps the entries of the terms `recovered-terms` names that `held?` holds, with no separation read: the first read after it tests every pair once (`sync-memberships`).
(kind-of w recs ms)The kind of the membership nogood over the member handles ms, read off their
sentences and the unscoped genl closure of the write view w (decide/write-view):
:disjoint for two memberships of one term in distinct types a declaration separates
(tax/pair-separated?), :supertype for one membership of a term beside one denial of
a strict supertype of its type, :cover for any other membership of a term beside
denials of it and for two or more memberships of a term in distinct types (a cover
refuted through a separation's denial), else nil.
The kind of the membership nogood over the member handles `ms`, read off their sentences and the unscoped `genl` closure of the write view `w` (`decide/write-view`): `:disjoint` for two memberships of one term in distinct types a declaration separates (`tax/pair-separated?`), `:supertype` for one membership of a term beside one denial of a strict supertype of its type, `:cover` for any other membership of a term beside denials of it and for two or more memberships of a term in distinct types (a cover refuted through a separation's denial), else nil.
(moved? c)Has the index queued a term whose nogoods the settle places again (take-moved!)?
Has the index queued a term whose nogoods the settle places again (`take-moved!`)?
(nogoods-of c x)Term x's nogoods under the candidate index c, each {:members #{h} :kind k}.
Term `x`'s nogoods under the candidate index `c`, each `{:members #{h} :kind k}`.
(nogoods-terms c)The kept terms holding a nogood under the candidate index c.
The kept terms holding a nogood under the candidate index `c`.
(routes w recs {:keys [members kind]})Each way the declarations convict the membership nogood ng over the unscoped
taxonomy, as tax/separation-routes answers for a :disjoint one: {:keys #{k} :links [[sub super]] :pair [x y]}, the flat-cache keys read, the genl subsumptions climbed
and the separated pair. For a :cover one, a cover over a whole above the held type
with a member denial at or above each part: the cover's key, the subsumption from the
held type to the whole and from each part to the first such denial's type, and no
pair, and for a part a held type's separation denies, the separation's keys and links
with the soundness rule's :strict-links, :strict-keys and :pairs (cover-routes).
A :disjoint one takes each cover route of its two memberships besides, since
term-nogoods keeps a cover refuted by the same two memberships as the one nogood.
For a :supertype one, the subsumption from the held type to the denied type with no
key, and each cover route besides. Empty when the members are not one term's.
Read over the write view w (decide/write-view): a route is a superset over every
reader, and the placement decides which contexts see it.
Each way the declarations convict the membership nogood `ng` over the unscoped
taxonomy, as `tax/separation-routes` answers for a `:disjoint` one: `{:keys #{k} :links
[[sub super]] :pair [x y]}`, the flat-cache keys read, the `genl` subsumptions climbed
and the separated pair. For a `:cover` one, a cover over a whole above the held type
with a member denial at or above each part: the cover's key, the subsumption from the
held type to the whole and from each part to the first such denial's type, and no
pair, and for a part a held type's separation denies, the separation's keys and links
with the soundness rule's `:strict-links`, `:strict-keys` and `:pairs` (`cover-routes`).
A `:disjoint` one takes each cover route of its two memberships besides, since
`term-nogoods` keeps a cover refuted by the same two memberships as the one nogood.
For a `:supertype` one, the subsumption from the held type to the denied type with no
key, and each cover route besides. Empty when the members are not one term's.
Read over the write view `w` (`decide/write-view`): a route is a superset over every
reader, and the placement decides which contexts see it.(take-moved! kb){x #{h}}, the terms whose nogoods moved since the last call, each with the members of
its nogoods before and after the move, and the queue emptied (place-term).
`{x #{h}}`, the terms whose nogoods moved since the last call, each with the members of
its nogoods before and after the move, and the queue emptied (`place-term`).(terms-of kb c hs)The terms of the memberships and denials among the handles hs that the candidate
index c keeps.
The terms of the memberships and denials among the handles `hs` that the candidate index `c` keeps.
(terms-under kb w c ends)The kept terms with a nogood (::ngs) holding a type at or below one of the types
ends over the unscoped genl closure (w, decide/write-view), in a membership or a
denial (listed-under): those whose nogoods a separation over ends arriving can give
a route.
The kept terms with a nogood (`::ngs`) holding a type at or below one of the types `ends` over the unscoped `genl` closure (`w`, `decide/write-view`), in a membership or a denial (`listed-under`): those whose nogoods a separation over `ends` arriving can give a route.
(terms-under-edges kb w c lows)The kept terms with a nogood whose routes climb a genl edge with its lower end at one
of the types lows: those holding a type at or below one of them, and those holding a
type at or below the whole of a cover with a part at or below one
(cover-wholes-under). An edge's defeat class moving moves which placements a cover
refuted through a separation's denial reads (chain/route-placements), with no
membership and no declaration moving.
The kept terms with a nogood whose routes climb a `genl` edge with its lower end at one of the types `lows`: those holding a type at or below one of them, and those holding a type at or below the whole of a cover with a part at or below one (`cover-wholes-under`). An edge's defeat class moving moves which placements a cover refuted through a separation's denial reads (`chain/route-placements`), with no membership and no declaration moving.
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |