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 in w (decide/unscoped-closures):
: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 in `w` (`decide/unscoped-closures`): `: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 a denial's type, that subsumption a
:strict-links too when the denial is above the part, 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, as a :strict-links too, since the nogood reads the edge's contrapositive and a
:default edge does not contrapose (docs/inference.md), and each cover route besides. Empty when the members are not one term's.
Read over the unscoped closures w (decide/unscoped-closures): 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 a denial's type, that subsumption a
`:strict-links` too when the denial is above the part, 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, as a `:strict-links` too, since the nogood reads the edge's contrapositive and a
`:default` edge does not contrapose (docs/inference.md), and each cover route besides. Empty when the members are not one term's.
Read over the unscoped closures `w` (`decide/unscoped-closures`): 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/unscoped-closures), 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/unscoped-closures`), 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 |