From 363623897c12201e2ff775195ce6e82b91a810d3 Mon Sep 17 00:00:00 2001 From: WaylandYang Date: Thu, 3 Sep 2026 09:32:05 +0800 Subject: [PATCH 1/2] A contradiction points at an error upstream Co-Authored-By: Claude Fable 5.1 --- .../0017-a-contradiction-points-upstream.md | 205 ++++++++++++++++++ docs/decisions/README.md | 3 +- 2 files changed, 207 insertions(+), 1 deletion(-) create mode 100644 docs/decisions/0017-a-contradiction-points-upstream.md diff --git a/docs/decisions/0017-a-contradiction-points-upstream.md b/docs/decisions/0017-a-contradiction-points-upstream.md new file mode 100644 index 000000000..82cd813fb --- /dev/null +++ b/docs/decisions/0017-a-contradiction-points-upstream.md @@ -0,0 +1,205 @@ +# 0017 · A contradiction points at an error upstream + +- **Status**: planned · B2 of 0016, wider than the one line written there: contradictions become visible everywhere, not only as a new kind in the queue +- **Written**: 2026-09-03 (conventions in [README](README.md)) +- **Related**: the two unbuilt rows of the "derived vs asserted" table in [0002](0002-reasoning-engine.md) §2; [0016](0016-close-the-open-seams-before-cutting-new-ones.md) B2; the proof chain (B1, #227) supplies the "premises expand to the sentence" half of the card below + +> This record changes one phrase in 0002. There, a contradiction "goes to Review for a ruling". +> In discussion (2026-09-03) it became clear what a person actually does when two edges +> disagree: follow the signal to **where something went wrong upstream** — a fact went +> stale, extraction misread, resolution merged the wrong pair, the ontology is too strict. +> So this queue is built as an audit, and every button is a repair. + +## The problem + +R1 derivation only yields to "this exact triple is already asserted". It does not consult +axioms: `part_of` transitivity derives `A part_of C` while the ledger asserts `C part_of A` +(asymmetric); `ceo_of` is functional and `Acme ceo_of Zhang San` is asserted, yet the +engine still lands `Acme ceo_of Li Si`. R0 scans `facts` only, derivations live in their +own table, so this class of contradiction is **invisible on both sides**: absent from +Review, absent from the graph. + +It is not the only invisible class. Temporal conflicts and axiom violations are known to +the Review page alone; on the graph and in the entity panel a contested edge looks exactly +like any other. + +## Criteria + +1. **A contradiction points at an error upstream.** The error is in one of four places: + stale knowledge (most common), a misread extraction, a wrong merge, an over-strict + ontology. The interface's job is to lay out the clues and offer the repairs. +2. **Write less to the graph rather than write wrong** (0002). A derivation that hits a + contradiction does not land; when two derivations collide, neither lands. +3. **Anything reported item by item needs an upper bound.** Only "one assertion against one + concrete edge" — a volume that can be predicted — goes into the queue individually, and + with a per-predicate cap; whatever is produced in batches is aggregated by its cause. +4. **A disputed fact is visible where it sits.** The assertion stays live, but someone + passing it on the graph or in the panel should see that it is questioned, and reach the + place to fix it in one step. + +## Decisions + +### 1. Detection: two tiers, pure logic in `utopia-reason` + +`derive::contradictions(derived, edges, axioms)` checks every derivation against the axioms +of its predicate, once against assertions and once against other derivations: + +| Axiom | What counts as a contradiction | +|---|---| +| functional | same subject and predicate, different object, **validity intervals overlap** (Mira leaving and Devin taking over is a succession; the half-open interval semantics of `validity` are reused) | +| inverse_functional | the dual | +| asymmetric | the reverse edge exists with overlapping validity | +| irreflexive | the derivation is a self-loop | + +**Derived vs asserted**: per item. The derivation does not land; one `axiom_violations` +row of kind `derived_contradiction`. Capped per predicate (same shape as R1's +`MAX_DERIVED_PER_PREDICATE`; 50 suggested); the overflow stays out of the queue and is +counted in the report. + +**Derived vs derived**: aggregated. The cause is a rule set that contradicts itself — +`ceo_of ⊑ works_at` together with `works_at` functional necessarily produces contradictions +in batches. Queuing every pair would flood Review, and a person facing a hundred identical +"two derivations disagree" cards cannot decide anything from them. So one row per **pair of +rules** goes into `ontology_defects`, kind `rules_disagree`, recording both rules, the +count, and two or three examples. It is the dynamic form of the existing static defects +`transitive_and_functional` and `symmetric_and_asymmetric`: invisible in the declarations, +surfacing once data arrives. Neither derivation lands. + +`run()` (R0) and `materialize` (R1) share the one function: R0 already holds the edges and +axioms and adds a `derive` + `contradictions` pass to report; R1 uses the same result to +decide what stays unlanded. **Both must compute it** — otherwise R0's "clear open rows not +recomputed this round" would sweep away what R1 wrote. + +### 2. The Review card: lay out the clues, lay out the repairs + +**The derived-vs-asserted card**, three parts: + +1. **The contradiction itself**: the derived edge (rule, premise chain expandable to the + sentence — from B1) beside the asserted edge (evidence quote, interval, confidence). + Most errors are visible at a glance. +2. **A diagnostic hint**, one line when a clue can be computed, none when it cannot: + - the assertion has no end date and the derivation starts after it → "looks stale: did + Zhang San's tenure end in 2024-07?" + - an entity on either side has same-name neighbours (the existing `same_name` machinery) + → "looks like a wrong merge: are these two Acmes one company?" + - the assertion's confidence is below 0.75 → "the extraction was unsure to begin with" + - none of the above → "read both sentences" +3. **Actions that are repairs**, all on existing endpoints; once a repair is made the + violation clears on the next recomputation, with no separate resolve step: + +| Action | What it repairs | Where it lands | +|---|---|---| +| Close the assertion at a date | stale knowledge | `POST /facts/{id}/close` (same as the temporal-conflict queue, with a date input) | +| Retract the assertion | misread extraction / wrong merge | `reject_fact`, append-only | +| Go to possible duplicates | wrong merge | the Duplicates queue in Review | +| The ontology is too strict | wrong definition | the relation on the Ontology page | +| Both hold; let the derivation through | the world is like that | `resolution = accepted`; the next `materialize` lets that pair land | + +**The derived-vs-derived card** (in the ontology-defects queue): "these two declarations +together produced N contradicting pairs; examples below — usually a sub-property attached +in the wrong place, or a functional declaration that is too strict". Two actions: go to the +Ontology page and change a declaration; or "accept" (contradicting derivations from this +pair of rules never land and are not reported again). Both sides are derived and the +assertions beneath may each be right, so there is no "the data is wrong" here; "both hold" +would mean giving up the meaning of functional, which belongs on the Ontology page, so +there is no such button either. + +### 3. Disputed facts are visible where they sit + +"Disputed" becomes one status with three sources: open temporal conflicts +(`fact_conflicts`), open axiom violations (`axiom_violations`, including the new kind), and +blocked derivations (the `detail` of `derived_contradiction` rows). B2 makes it a first-class +state of the browse pages and wires up the first two sources along the way — they are +equally invisible today. + +**Rows in the entity panel**: `EntityFact` already carries `stale` and `corrected`; a third +flag `contested: Option` is computed with one EXISTS. The chip +reads "disputed"; hover gives one sentence ("derived works_at Li Si contradicts this"); +click goes to the matching Review item. The row is not dimmed: the assertion is still live. + +**The Derived tab of the panel**: a new section, "derivations that did not land", read from +`axiom_violations.detail`, each row naming what blocked it and expanding to its premise +chain. Here a person sees "the engine could have drawn this edge, and what stopped it". + +**Edges on the graph**: + +- A contested assertion switches to the **alert colour**, edge and all, with no reliance on + a node ring. The request was explicit: a ring sits on the node while the edge stays grey, + and peripheral vision cannot tell them apart. +- A blocked derivation is drawn as a **ghost edge**: the same hue mixed toward `EDGE_DIM` + (under premultiplied blending alpha cannot darken an edge; only the RGB can be mixed — see + the note at `EDGE_DIM`), thinner. It follows the Derived toggle; clicking it opens the + entity panel at that row. sigma's default edge program does not draw dashes, and no custom + program is introduced for this. +- The hover label chip gets a "⚠" prefix, and the tooltip states the dispute. + +**Colour**: one new token, `--u-contest`, set to **#ff6a3d** (hot coral orange). It has to +stand apart from three colours already in use: derived edges are gold +(`rgb(231,197,124)`), warning chips are amber (`--u-warn` #f2b66d, too close to gold to +double as an edge colour), and danger is pink (`--u-danger` #ff9daf, reserved for +destructive actions). Coral orange is bright enough on the dark ground, its hue is far from +all three, and it is no common type colour (the type palette leans blue, green and violet). +Edge colour `rgba(255,106,61,0.55)`; ghost edge `lerp(#ff6a3d, EDGE_DIM, 0.55)`. This is +the only new colour; chips on the Ontology and Review pages use the same token. + +### 4. Data + +Migration `0020` (0019 was taken by #199 / #233): + +- `axiom_violations.kind` CHECK gains `derived_contradiction` +- `axiom_violations` gains `detail JSONB NOT NULL DEFAULT '{}'`: the derived triple (three + ids and three names), the rule kind, the premise ids — without it the interface cannot + say what was derived; `path` holds the premises for the proof chain but cannot draw the + ghost edge +- `axiom_violations.resolution` CHECK gains `fact_closed` (closing an assertion is a repair + that leaves its own trace, kept apart from `fact_retracted`) +- `ontology_defects.kind` CHECK gains `rules_disagree`, plus `detail JSONB` (both rules, the + count, the examples) + +`left_fact` / `right_fact` stay non-null and keep pointing at `facts`: for derived vs +asserted, `left` is the contradicted assertion and `right` the derivation's last premise; +`rules_disagree` does not live in this table. + +### 5. Interfaces + +- `GET /kbs/{id}/graph`: edges gain `contested: bool`; a new class of edge with + `blocked: true` (the ghosts) +- `GET /kbs/{id}/entities/{id}`: `facts[].contested`; `blocked: [...]` next to `derived` +- Review `violations` queue: rows gain `detail` and `hint` (the diagnostic as a code; wording + belongs to the frontend) +- `POST /kbs/{id}/review/violations/{id}`: `resolution` gains `fact_closed` (with + `close_at`); the server calls `close_fact` and then marks the row resolved + +### 6. Tests + +- `utopia-reason` unit tests: one per axiom, non-overlapping intervals are no contradiction, + derived-vs-derived aggregates by rule pair, the cap is counted +- Store integration: a functional assertion stands and a derivation collides → the + derivation stays out and one violation carries `detail`; retract the assertion and rerun → + the derivation lands and the violation clears; `accepted` → both coexist; `fact_closed` + runs the close path; R0 and R1 agree +- Browser: an edge turns coral, ghost edges follow the toggle, the panel chip jumps to the + Review item, the Review card shows three parts and five actions + +## Two cuts + +**B2a · engine and queue**: §1, §2, §4, and the Review parts of §5, with the integration +tests. Two days. +**B2b · visibility**: §3 plus the graph and panel interfaces, wiring existing temporal +conflicts and axiom violations along the way. A day and a half. + +B1 (#227) merges first after a rebase; B2a branches from it. + +## Open questions + +- **The per-predicate cap of 50 is a guess**, awaiting a bench number like R1's twenty + thousand. +- **Granularity of `accepted`**: per pair (one derivation against one assertion). An + assertion hit by several derivations needs several clicks; aggregating the exemption per + assertion would generalise "this axiom does not apply to this assertion" too far. Per + pair first, measure later. +- **Could ghost edges be too many?** Their number is bounded by the (capped) violation + count, so it should stay manageable; failing that, draw them only when a related node is + selected. +- **Does the disputed status need its own SSE event?** The `review` event is already sent; + graph and panel can refetch on it. No new event. diff --git a/docs/decisions/README.md b/docs/decisions/README.md index 81142c040..264bce745 100644 --- a/docs/decisions/README.md +++ b/docs/decisions/README.md @@ -20,7 +20,7 @@ **行号会漂，文件名会换。** 正文里的 `file.rs:123` 是成文时的坐标，不保证仍然准确；迁移在 #130 / #131 从 53 份折成 10 份、一个域一份，所以 2026-08-31 之前写的迁移文件名都要按域重找。引用时优先写函数名、表名、常量名。 -**语言**：中文，与代码注释一致（UI 与 README 保持英文）。目前的读者是维护者，不是外部贡献者；将来需要时再译。 +**语言**：2026-09-03 起新记录用英文（0017 起），读者已经包括外部贡献者；此前的十六篇仍是中文，与代码注释一致，是否回译等有人需要时再定。 ## 索引 @@ -42,6 +42,7 @@ | 0014 | [身份跟着人，范围跟着令牌](0014-identity-from-the-person-scope-from-the-token.md) | 已实施（#180）· MCP 只读五工具 · 令牌页在账户层（A2）· 误导性的占位 crate 已删 | | 0015 | [记下一句话，不等于断言一个事实](0015-recording-a-sentence-is-not-asserting-a-fact.md) | 已实施 · 记忆抽出的事实进 `pending_facts`，Review 新档 + 跟在 remember 步骤后的确认卡 · `remember` 重新打开 · MCP 放开写是下一刀 | | 0016 | [先把开着的口子收上，再开新的](0016-close-the-open-seams-before-cutting-new-ones.md) | 规划中 · v0.1.0 之后的排期：A 收口 → B 推理机 ∥ C 尺子与本体 → D 语义层 → E 企业交付；模拟引擎后置 | +| 0017 | [A contradiction points at an error upstream](0017-a-contradiction-points-upstream.md) | 规划中 · 0016 B2 的完整方案：派生撞断言逐条封顶、派生撞派生按规则聚合、卡片给线索与修法、争议在图和面板上原地可见（新警戒色）| ## 不是决策记录的那些 From 34964b415f27c82563e9b3a4c09006d478cfedda Mon Sep 17 00:00:00 2001 From: WaylandYang Date: Thu, 3 Sep 2026 10:28:47 +0800 Subject: [PATCH 2/2] A contradiction points at an error upstream (B2a) Co-Authored-By: Claude Fable 5.1 --- crates/utopia-core/src/models.rs | 15 +- crates/utopia-reason/src/derive.rs | 405 +++++++++++++++- crates/utopia-reason/src/lib.rs | 8 +- crates/utopia-server/src/api/review_routes.rs | 94 +++- crates/utopia-store/src/reasoning.rs | 453 +++++++++++++++--- .../tests/a_contradiction_points_upstream.rs | 341 +++++++++++++ docs/decisions/0002-reasoning-engine.md | 2 + ...-the-open-seams-before-cutting-new-ones.md | 2 +- .../0017-a-contradiction-points-upstream.md | 2 +- docs/decisions/README.md | 2 +- .../0020_a_contradiction_points_upstream.sql | 34 ++ web/src/api.ts | 56 ++- web/src/i18n/en.ts | 28 ++ web/src/i18n/zh.ts | 23 + web/src/pages/Review.tsx | 147 +++++- web/src/styles.css | 2 + 16 files changed, 1517 insertions(+), 97 deletions(-) create mode 100644 crates/utopia-store/tests/a_contradiction_points_upstream.rs create mode 100644 migrations/0020_a_contradiction_points_upstream.sql diff --git a/crates/utopia-core/src/models.rs b/crates/utopia-core/src/models.rs index 06e1a0b41..ab05c1848 100644 --- a/crates/utopia-core/src/models.rs +++ b/crates/utopia-core/src/models.rs @@ -867,10 +867,10 @@ pub struct ConceptMapping { /// /// **两条事实都展开成 主-谓-宾 文本**：Review 页要让人一眼看出矛盾在哪， /// 而两个 UUID 看不出任何东西。自反那一类两条相同——它就是一条事实。 -#[derive(Debug, Clone, Serialize, sqlx::FromRow)] +#[derive(Debug, Clone, Serialize)] pub struct AxiomViolation { pub id: Uuid, - /// self_loop | asymmetry | cycle | functional + /// self_loop | asymmetry | cycle | functional | signature | derived_contradiction pub kind: String, /// 判据来自哪条关系。人若判「公理写错了」，从这里进本体去改 pub predicate: Option, @@ -881,6 +881,12 @@ pub struct AxiomViolation { /// 环的长度（含首尾）。其余三类为 0——前端据此决定要不要显示「查看路径」 pub path_len: i32, pub detected_at: chrono::DateTime, + /// `derived_contradiction` 独有（0017）：推出来的那条三元组——它没有落库， + /// 只能在这里写出来。字段见 `reasoning::run`。其余种类是 `{}` + pub detail: serde_json::Value, + /// 审核线索（0017 §2）：`stale`（旧断言没写结束日期）、`duplicate`（有同名 + /// 实体）、`unsure`（抽取置信度低）。只给一条，没有就空 + pub hint: Option, } /// 本体自己的一处自相矛盾（见 `ontology_defects`）。 @@ -891,8 +897,11 @@ pub struct AxiomViolation { pub struct OntologyDefect { pub id: Uuid, /// symmetric_and_asymmetric | transitive_and_functional | subclass_cycle - /// | disjoint_with_ancestor | inherits_disjoint + /// | disjoint_with_ancestor | inherits_disjoint | inverse_of_itself + /// | inverse_not_mutual | sub_property_cycle | rules_disagree pub kind: String, + /// `rules_disagree` 独有（0017）：哪两条规则、撞在哪条公理上、几对、几个例子 + pub detail: serde_json::Value, /// 出问题那个对象的标签（类或谓词）。查不到就是它已经被删了 pub subject_label: Option, /// 另一方：互斥的那个类 diff --git a/crates/utopia-reason/src/derive.rs b/crates/utopia-reason/src/derive.rs index 73c8ab2e1..aa6c473dc 100644 --- a/crates/utopia-reason/src/derive.rs +++ b/crates/utopia-reason/src/derive.rs @@ -20,7 +20,7 @@ //! 前提 A `[2020,2023)`、前提 B `[2022,∞)` → 派生 `[2022,2023)`。交集为空 //! 就不推——两段没有重叠的时候,链本身在任何时刻都不成立。 -use crate::{Axioms, Edge, MAX_DEPTH}; +use crate::{Axioms, Edge, Kind, MAX_DEPTH}; use std::collections::{HashMap, HashSet}; use uuid::Uuid; @@ -31,7 +31,7 @@ use uuid::Uuid; /// ——悄悄截断会让「推完了」和「推了一部分」长得一模一样。 pub const MAX_DERIVED_PER_PREDICATE: usize = 20_000; -#[derive(Debug, Clone, Copy, PartialEq, Eq)] +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] pub enum Rule { /// `A p B` ∧ `B p C` ⟹ `A p C` Transitive, @@ -379,6 +379,248 @@ pub fn validity( Some(acc) } +// ===================== 矛盾：派生撞上了什么（0017） ===================== + +/// 一条派生撞上了一条断言。 +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct Clash { + /// `Derivation::facts` 里的下标 + pub derived: usize, + /// 撞在哪条公理上：`Functional`（含 inverse_functional）、`Asymmetry`、`SelfLoop` + pub axiom: Kind, + /// 被撞的断言。自环没有对方，取派生的最后一条前提 + pub against: Uuid, +} + +/// 两条规则加在一起产出了互相矛盾的派生。 +/// +/// **按规则对聚合，不逐对报**：`ceo_of ⊑ works_at` 加 `works_at` functional，每个有 +/// 两个 ceo 的组织就撞一对——根子是那两条声明，逐对进队列只会淹掉 Review。 +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct RuleClash { + /// (声明所在的谓词, 规则种类)，两条按 (谓词, 种类) 排过序，a ≤ b + pub a: (Uuid, Rule), + pub b: (Uuid, Rule), + pub axiom: Kind, + /// 互撞的派生对，按 `Derivation::facts` 的下标 + pub pairs: Vec<(usize, usize)>, +} + +/// 半开区间 `[from, to)`，两端可空 +type Span = (Option, Option); +/// (谓词, 一端) → 另一端的边：(另一端, 事实, 区间)。functional 两个方向各一份 +type ByEnd = HashMap<(Uuid, Uuid), Vec<(Uuid, Uuid, Span)>>; +/// 一条规则的身份：声明所在的谓词 + 规则种类 +type RuleSide = (Uuid, Rule); +/// 互撞的派生对，按 (规则 a, 规则 b, 撞在哪条公理上) 分组 +type Grouped = HashMap<(RuleSide, RuleSide, Kind), Vec<(usize, usize)>>; + +#[derive(Debug, Clone, Default, PartialEq, Eq)] +pub struct Contradictions { + pub with_assertions: Vec, + pub between_derivations: Vec, +} + +impl Contradictions { + /// 不该落地的派生下标：撞过断言的，和撞过别的派生的。**写图宁少勿错**（0002） + pub fn blocked(&self) -> HashSet { + let mut out: HashSet = self.with_assertions.iter().map(|c| c.derived).collect(); + for rc in &self.between_derivations { + for (i, j) in &rc.pairs { + out.insert(*i); + out.insert(*j); + } + } + out + } +} + +/// 拿公理量一遍派生：与断言撞的逐条列出，派生之间撞的按规则对聚合。 +/// +/// 只查四类——`functional`（含 inverse）、`asymmetric`、`irreflexive`——因为只有它们 +/// 能由**两条边**判出矛盾；传递环那类要走闭包，派生本身就是闭包的一部分，R0 对断言 +/// 查过就够了。functional 与 asymmetric 都要求**有效区间重叠**：Mira 走了 Devin +/// 接任，两条 `ceo_of` 区间不交，那是接任，不是矛盾。 +/// +/// 撞上断言的派生一律**不落地**（asserted > derived，硬性）；这一步把「让路」这件事 +/// 从静默变成可见——0002 那张表里写了没做的那一行。 +pub fn contradictions( + derivation: &Derivation, + edges: &[TimedEdge], + axioms: &HashMap, + spans: &HashMap, Option)>, +) -> Contradictions { + // 断言的三份索引：(谓词, 主) → 宾；(谓词, 宾) → 主；(谓词, 主, 宾) → 边 + let mut by_ps: ByEnd = HashMap::new(); + let mut by_po: ByEnd = HashMap::new(); + let mut by_spo: HashMap<(Uuid, Uuid, Uuid), Vec<(Uuid, Span)>> = HashMap::new(); + for e in edges { + let span = (e.from, e.to); + let x = e.edge; + by_ps + .entry((x.predicate, x.subject)) + .or_default() + .push((x.object, x.fact, span)); + by_po + .entry((x.predicate, x.object)) + .or_default() + .push((x.subject, x.fact, span)); + by_spo + .entry((x.predicate, x.subject, x.object)) + .or_default() + .push((x.fact, span)); + } + + let mut out = Contradictions::default(); + // 派生的区间：与落库那一侧同一个函数算，算不出的（前提区间不交）本来就不会落 + let derived_spans: Vec> = derivation + .facts + .iter() + .map(|d| validity(&d.premises, spans)) + .collect(); + + for (i, d) in derivation.facts.iter().enumerate() { + let Some(span) = derived_spans[i] else { + continue; + }; + let Some(ax) = axioms.get(&d.predicate) else { + continue; + }; + let Some(&last) = d.premises.last() else { + continue; + }; + if ax.irreflexive && d.subject == d.object { + out.with_assertions.push(Clash { + derived: i, + axiom: Kind::SelfLoop, + against: last, + }); + } + if ax.asymmetric { + if let Some(v) = by_spo.get(&(d.predicate, d.object, d.subject)) { + for (fact, sp) in v { + if overlap(span, *sp).is_some() { + out.with_assertions.push(Clash { + derived: i, + axiom: Kind::Asymmetry, + against: *fact, + }); + } + } + } + } + if ax.functional { + if let Some(v) = by_ps.get(&(d.predicate, d.subject)) { + for (obj, fact, sp) in v { + if *obj != d.object && overlap(span, *sp).is_some() { + out.with_assertions.push(Clash { + derived: i, + axiom: Kind::Functional, + against: *fact, + }); + } + } + } + } + if ax.inverse_functional { + if let Some(v) = by_po.get(&(d.predicate, d.object)) { + for (subj, fact, sp) in v { + if *subj != d.subject && overlap(span, *sp).is_some() { + out.with_assertions.push(Clash { + derived: i, + axiom: Kind::Functional, + against: *fact, + }); + } + } + } + } + } + + // 派生之间：同样三份索引，只不过键的是下标 + let mut d_ps: HashMap<(Uuid, Uuid), Vec> = HashMap::new(); + let mut d_po: HashMap<(Uuid, Uuid), Vec> = HashMap::new(); + let mut d_spo: HashMap<(Uuid, Uuid, Uuid), Vec> = HashMap::new(); + for (i, d) in derivation.facts.iter().enumerate() { + if derived_spans[i].is_none() { + continue; + } + d_ps.entry((d.predicate, d.subject)).or_default().push(i); + d_po.entry((d.predicate, d.object)).or_default().push(i); + d_spo + .entry((d.predicate, d.subject, d.object)) + .or_default() + .push(i); + } + let mut grouped: Grouped = HashMap::new(); + let mut note = |i: usize, j: usize, axiom: Kind| { + let (i, j) = if i < j { (i, j) } else { (j, i) }; + let ri = (derivation.facts[i].via, derivation.facts[i].rule); + let rj = (derivation.facts[j].via, derivation.facts[j].rule); + let (a, b) = if (ri.0, ri.1.as_str()) <= (rj.0, rj.1.as_str()) { + (ri, rj) + } else { + (rj, ri) + }; + grouped.entry((a, b, axiom)).or_default().push((i, j)); + }; + for (i, d) in derivation.facts.iter().enumerate() { + let Some(span) = derived_spans[i] else { + continue; + }; + let Some(ax) = axioms.get(&d.predicate) else { + continue; + }; + let overlapping = |j: usize| derived_spans[j].is_some_and(|s| overlap(span, s).is_some()); + if ax.asymmetric { + if let Some(v) = d_spo.get(&(d.predicate, d.object, d.subject)) { + for &j in v { + if j > i && overlapping(j) { + note(i, j, Kind::Asymmetry); + } + } + } + } + if ax.functional { + if let Some(v) = d_ps.get(&(d.predicate, d.subject)) { + for &j in v { + if j > i && derivation.facts[j].object != d.object && overlapping(j) { + note(i, j, Kind::Functional); + } + } + } + } + if ax.inverse_functional { + if let Some(v) = d_po.get(&(d.predicate, d.object)) { + for &j in v { + if j > i && derivation.facts[j].subject != d.subject && overlapping(j) { + note(i, j, Kind::Functional); + } + } + } + } + } + let mut rule_clashes: Vec = grouped + .into_iter() + .map(|((a, b, axiom), mut pairs)| { + pairs.sort_unstable(); + pairs.dedup(); + RuleClash { a, b, axiom, pairs } + }) + .collect(); + // 输出排过序——这条路的价值有一半在确定性 + rule_clashes.sort_by(|x, y| { + (x.a.0, x.a.1.as_str(), x.b.0, x.b.1.as_str()).cmp(&( + y.a.0, + y.a.1.as_str(), + y.b.0, + y.b.1.as_str(), + )) + }); + out.between_derivations = rule_clashes; + out +} + #[cfg(test)] mod tests { use super::*; @@ -796,4 +1038,163 @@ mod tests { let d = derive(&[ep(P, 1, 1, 1)], &ax); assert!(d.facts.is_empty(), "`A p A` 的逆还是 `A p A`——自环不推"); } + + // ---------- 矛盾（0017） ---------- + + /// 指定谓词的一条带区间的边 + fn et(pred: Uuid, fact: u8, s: u8, o: u8, from: Option, to: Option) -> TimedEdge { + TimedEdge { + edge: Edge { + fact: f(fact), + predicate: pred, + subject: n(s), + object: n(o), + }, + from, + to, + } + } + + fn spans_of(edges: &[TimedEdge]) -> HashMap, Option)> { + edges + .iter() + .map(|e| (e.edge.fact, (e.from, e.to))) + .collect() + } + + /// `ceo_of ⊑ works_at`，works_at functional：Mira 的 ceo_of 推出 works_at Acme， + /// 而账本里说她 works_at Globex——派生撞上断言，指名道姓 + #[test] + fn a_derivation_that_breaks_functional_names_the_assertion_it_hit() { + let ax = HashMap::from([ + ( + P, + Axioms { + sub_property_of: Some(Q), + ..Default::default() + }, + ), + ( + Q, + Axioms { + functional: true, + ..Default::default() + }, + ), + ]); + let edges = [ep(P, 1, 1, 2), ep(Q, 2, 1, 3)]; + let d = derive(&edges, &ax); + assert_eq!(d.facts.len(), 1); + let c = contradictions(&d, &edges, &ax, &spans_of(&edges)); + assert_eq!( + c.with_assertions, + vec![Clash { + derived: 0, + axiom: Kind::Functional, + against: f(2) + }] + ); + assert!(c.between_derivations.is_empty()); + assert_eq!(c.blocked(), HashSet::from([0])); + } + + /// 区间不交就不是矛盾：前任与继任 + #[test] + fn disjoint_intervals_are_succession_and_stay_silent() { + let ax = HashMap::from([ + ( + P, + Axioms { + sub_property_of: Some(Q), + ..Default::default() + }, + ), + ( + Q, + Axioms { + functional: true, + ..Default::default() + }, + ), + ]); + let edges = [ + et(P, 1, 1, 2, Some(10), Some(20)), + et(Q, 2, 1, 3, Some(30), None), + ]; + let d = derive(&edges, &ax); + let c = contradictions(&d, &edges, &ax, &spans_of(&edges)); + assert!(c.with_assertions.is_empty(), "{c:?}"); + } + + /// 对称与非对称：`A p B` 对称推出 `B p A`，而 p 又声明 asymmetric—— + /// 每条断言都撞上自己的镜像 + #[test] + fn a_symmetric_derivation_hits_the_asymmetric_assertion() { + let ax = HashMap::from([( + P, + Axioms { + symmetric: true, + asymmetric: true, + ..Default::default() + }, + )]); + let edges = [ep(P, 1, 1, 2)]; + let d = derive(&edges, &ax); + let c = contradictions(&d, &edges, &ax, &spans_of(&edges)); + assert_eq!(c.with_assertions.len(), 1); + assert_eq!(c.with_assertions[0].axiom, Kind::Asymmetry); + assert_eq!(c.with_assertions[0].against, f(1)); + } + + /// 两条派生互撞时按规则对聚合，而且都不落地 + #[test] + fn derivations_that_disagree_are_grouped_by_the_rules_that_made_them() { + let ax = HashMap::from([ + ( + P, + Axioms { + sub_property_of: Some(Q), + ..Default::default() + }, + ), + ( + Q, + Axioms { + functional: true, + ..Default::default() + }, + ), + ]); + // 1 ceo_of 2 与 1 ceo_of 3：两条 works_at 由同一条规则推出，互相排斥 + let edges = [ep(P, 1, 1, 2), ep(P, 2, 1, 3), ep(P, 3, 4, 5)]; + let d = derive(&edges, &ax); + assert_eq!(d.facts.len(), 3); + let c = contradictions(&d, &edges, &ax, &spans_of(&edges)); + assert!(c.with_assertions.is_empty()); + assert_eq!(c.between_derivations.len(), 1); + let rc = &c.between_derivations[0]; + assert_eq!(rc.a, (P, Rule::SubProperty)); + assert_eq!(rc.b, (P, Rule::SubProperty)); + assert_eq!(rc.axiom, Kind::Functional); + assert_eq!(rc.pairs.len(), 1); + // 第三条（4 works_at 5）没跟谁撞，照常落地 + assert_eq!(c.blocked().len(), 2); + assert!(!c.blocked().contains(&2)); + } + + /// 谓词上没有公理就没有矛盾可言 + #[test] + fn a_predicate_without_axioms_cannot_contradict() { + let ax = HashMap::from([( + P, + Axioms { + sub_property_of: Some(Q), + ..Default::default() + }, + )]); + let edges = [ep(P, 1, 1, 2), ep(Q, 2, 1, 3)]; + let d = derive(&edges, &ax); + let c = contradictions(&d, &edges, &ax, &spans_of(&edges)); + assert_eq!(c, Contradictions::default()); + } } diff --git a/crates/utopia-reason/src/lib.rs b/crates/utopia-reason/src/lib.rs index b12b6528d..b6c3ca5cc 100644 --- a/crates/utopia-reason/src/lib.rs +++ b/crates/utopia-reason/src/lib.rs @@ -67,7 +67,7 @@ pub struct Violation { pub path: Vec, } -#[derive(Debug, Clone, Copy, PartialEq, Eq)] +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] pub enum Kind { /// `A p A`，而 p 声明了 irreflexive SelfLoop, @@ -85,6 +85,11 @@ pub enum Kind { /// 是为了与其它四类走同一条落库、清陈、裁决的路——left 与 right 同一条事实， /// 与自反那类同款 Signature, + /// 一条派生撞上了一条断言（0017）：推出来的 `A p B` 与账本里的某条断言在 p 的 + /// 公理上不能并存。派生不落地，这一行把它摆到人面前。`left` 是被撞的断言， + /// `right` 是派生的最后一条前提，`path` 是全部前提；推出来的三元组本身在 + /// `axiom_violations.detail` 里——它没有落库，没有 id 可指 + DerivedContradiction, } impl Kind { @@ -95,6 +100,7 @@ impl Kind { Kind::Cycle => "cycle", Kind::Functional => "functional", Kind::Signature => "signature", + Kind::DerivedContradiction => "derived_contradiction", } } } diff --git a/crates/utopia-server/src/api/review_routes.rs b/crates/utopia-server/src/api/review_routes.rs index ba1a619e7..c6fc951d2 100644 --- a/crates/utopia-server/src/api/review_routes.rs +++ b/crates/utopia-server/src/api/review_routes.rs @@ -497,8 +497,11 @@ pub async fn decide_mapping( #[derive(Deserialize)] pub struct DecideViolationReq { - /// fact_retracted | axiom_relaxed | accepted + /// fact_retracted | fact_closed | axiom_relaxed | accepted pub resolution: String, + /// `fact_closed` 必填：旧断言在哪一天结束 + #[serde(default)] + pub close_at: Option>, } /// 人裁决一处公理违规。 @@ -518,16 +521,101 @@ pub async fn decide_violation( require_kb(&state, &user, kb_id, Role::Editor).await?; if !matches!( req.resolution.as_str(), - "fact_retracted" | "axiom_relaxed" | "accepted" + "fact_retracted" | "fact_closed" | "axiom_relaxed" | "accepted" ) { return Err(utopia_core::AppError::invalid( "bad_resolution", - "resolution 只能是 fact_retracted、axiom_relaxed 或 accepted", + "resolution 只能是 fact_retracted、fact_closed、axiom_relaxed 或 accepted", ) .into()); } + let row: Option<(String, Uuid)> = sqlx::query_as( + "SELECT kind, left_fact FROM axiom_violations + WHERE id = $1 AND kb_id = $2 AND status = 'open'", + ) + .bind(violation_id) + .bind(kb_id) + .fetch_optional(&state.pool) + .await + .map_err(utopia_core::AppError::Db)?; + let Some((kind, left)) = row else { + return Err(utopia_core::AppError::NotFound.into()); + }; + // 派生撞断言那一类（0017）的修法就在卡片上，端点替人执行：撤旧断言、或给它一个 + // 结束日期。其它几类仍只记决定——那些卡片上两条都是断言，撤哪条端点判不了 + let repaired = kind == "derived_contradiction"; + match (repaired, req.resolution.as_str()) { + (true, "fact_retracted") => { + let snap = fact_snapshot(&state, kb_id, left).await; + utopia_store::graph::reject_fact(&state.pool, kb_id, left).await?; + if let Some(d) = snap { + let _ = utopia_store::audit::record( + &state.pool, + Some(kb_id), + user.id, + "fact.reject", + "fact", + Some(left), + d, + ) + .await; + } + } + (true, "fact_closed") => { + let Some(at) = req.close_at else { + return Err(utopia_core::AppError::invalid( + "close_at_required", + "fact_closed 要给出结束日期", + ) + .into()); + }; + let open: Option<(Uuid,)> = sqlx::query_as( + "SELECT id FROM facts + WHERE id = $1 AND invalidated_at IS NULL AND valid_to IS NULL", + ) + .bind(left) + .fetch_optional(&state.pool) + .await + .map_err(utopia_core::AppError::Db)?; + if open.is_none() { + return Err(utopia_core::AppError::invalid( + "not_open", + "这条断言已有结束日期，或已被撤", + ) + .into()); + } + let snap = fact_snapshot(&state, kb_id, left).await; + utopia_store::temporal::close_superseded(&state.pool, left, at, "day").await?; + if let Some(mut d) = snap { + d["valid_to"] = json!(at.to_rfc3339()); + let _ = utopia_store::audit::record( + &state.pool, + Some(kb_id), + user.id, + "fact.close", + "fact", + Some(left), + d, + ) + .await; + } + } + (false, "fact_closed") => { + return Err(utopia_core::AppError::invalid( + "bad_resolution", + "fact_closed 只用于 derived_contradiction", + ) + .into()); + } + _ => {} + } utopia_store::reasoning::decide(&state.pool, kb_id, violation_id, &req.resolution, user.id) .await?; + // 路清了就让派生落地，人不必再去点一次「推一遍」。撤与闭合把断言挪开了， + // 认可则在 materialize 里放行 + if repaired { + utopia_store::reasoning::materialize(&state.pool, kb_id).await?; + } let _ = utopia_store::audit::record( &state.pool, Some(kb_id), diff --git a/crates/utopia-store/src/reasoning.rs b/crates/utopia-store/src/reasoning.rs index 37c42f54a..1b9764aac 100644 --- a/crates/utopia-store/src/reasoning.rs +++ b/crates/utopia-store/src/reasoning.rs @@ -12,13 +12,14 @@ //! 提案刷回待看，等于每跑一次就把人的否决抹掉一次。所以这里 `ON CONFLICT` //! 什么都不做——已经在库里的那一行，无论 open 还是 resolved，都按原样留着。 +use serde_json::json; use sqlx::PgPool; -use std::collections::HashMap; +use std::collections::{HashMap, HashSet}; use utopia_core::models::{AxiomViolation, DerivedFactView, OntologyDefect}; /// 规则种类的字面量。用 &'static str 而不是枚举:它直接进 SQL 也直接做键 type RuleKind = &'static str; use utopia_core::AppResult; -use utopia_reason::derive::TimedEdge; +use utopia_reason::derive::{Contradictions, Derivation, TimedEdge}; use utopia_reason::{check, Axioms, Edge, Kind, Violation}; use uuid::Uuid; @@ -35,37 +36,17 @@ pub struct Report { pub inserted: usize, /// 清掉的陈旧 open 行 pub cleared: usize, + /// 派生撞上断言的条数（0017），已含在 `found` 里 + pub contradictions: usize, + /// 撞上单谓词上限、没进队列的矛盾条数。**不为零时说明根子在规则**： + /// 一条谓词上上百条派生都撞了，逐条看是没有意义的 + pub contradictions_capped: usize, + /// 互撞的规则对数——进 `ontology_defects`，不进这张表 + pub rules_disagree: usize, } -/// 取这个库里所有能参与检查的边。 -/// -/// 三个过滤条件都是必要的： -/// -/// - `invalidated_at IS NULL`——被推翻的事实不该再报矛盾，它已经不是我们的断言了 -/// - `predicate_id IS NOT NULL`——没有谓词就没有公理可依（见 `facts.predicate_id`） -/// - `object_id IS NOT NULL`——属性事实的宾语是字面值，公理谈的是实体之间的关系 -async fn edges(pool: &PgPool, kb_id: Uuid) -> AppResult> { - let rows: Vec<(Uuid, Uuid, Uuid, Uuid)> = sqlx::query_as( - "SELECT id, predicate_id, subject_id, object_id - FROM facts - WHERE kb_id = $1 - AND invalidated_at IS NULL - AND predicate_id IS NOT NULL - AND object_id IS NOT NULL", - ) - .bind(kb_id) - .fetch_all(pool) - .await?; - Ok(rows - .into_iter() - .map(|(fact, predicate, subject, object)| Edge { - fact, - predicate, - subject, - object, - }) - .collect()) -} +/// 单个谓词上进队列的矛盾上限（0017 §1）。超出的部分只计数。 +const MAX_CLASHES_PER_PREDICATE: usize = 50; /// 取这个库的谓词公理。 /// @@ -229,7 +210,8 @@ pub async fn record_signature_breaks( /// 跑一遍检查，把结果落库。 pub async fn run(pool: &PgPool, kb_id: Uuid) -> AppResult { - let edges = edges(pool, kb_id).await?; + let (timed, spans, _) = timed_edges(pool, kb_id).await?; + let edges: Vec = timed.iter().map(|t| t.edge).collect(); let axioms = axioms(pool, kb_id).await?; let mut violations = check(&edges, &axioms); // 第五类不在纯逻辑引擎里：它要看实体的类型与谓词的 domain / range，那是库里的 @@ -243,10 +225,63 @@ pub async fn run(pool: &PgPool, kb_id: Uuid) -> AppResult { }); } + // 第六类（0017）：推出来却落不了地的派生。与 `materialize` 用同一个函数算， + // 所以这里报的正是那边拦下的——两边各算一套的话，队列会跟图对不上 + let derivation = utopia_reason::derive::derive(&timed, &axioms); + let clashes = utopia_reason::derive::contradictions(&derivation, &timed, &axioms, &spans); + let names = names_for(pool, &derivation, &clashes).await?; + let mut details: HashMap<(Uuid, Uuid), serde_json::Value> = HashMap::new(); + let mut per_pred: HashMap = HashMap::new(); + let mut contradictions_capped = 0usize; + for c in &clashes.with_assertions { + let d = &derivation.facts[c.derived]; + let Some(&last) = d.premises.last() else { + continue; + }; + let key = (c.against, last); + if details.contains_key(&key) { + continue; + } + let n = per_pred.entry(d.predicate).or_default(); + if *n >= MAX_CLASHES_PER_PREDICATE { + contradictions_capped += 1; + continue; + } + *n += 1; + let span = utopia_reason::derive::validity(&d.premises, &spans); + details.insert( + key, + json!({ + "axiom": c.axiom.as_str(), + "rule": d.rule.as_str(), + "via": d.via, + "via_label": names.predicate(d.via), + "subject_id": d.subject, + "subject": names.entity(d.subject), + "predicate_id": d.predicate, + "predicate": names.predicate(d.predicate), + "object_id": d.object, + "object": names.entity(d.object), + "valid_from": span.and_then(|s| s.0).map(|t| stamp(t).to_rfc3339()), + "valid_to": span.and_then(|s| s.1).map(|t| stamp(t).to_rfc3339()), + "premises": d.premises, + }), + ); + violations.push(Violation { + kind: Kind::DerivedContradiction, + left: c.against, + right: last, + path: d.premises.clone(), + }); + } + let mut report = Report { edges: edges.len(), predicates_with_axioms: axioms.len(), found: violations.len(), + contradictions: details.len(), + contradictions_capped, + rules_disagree: clashes.between_derivations.len(), ..Default::default() }; @@ -261,9 +296,13 @@ pub async fn run(pool: &PgPool, kb_id: Uuid) -> AppResult { right, path, } = v; + let detail = details + .get(&(*left, *right)) + .cloned() + .unwrap_or_else(|| json!({})); let id: Option<(Uuid,)> = sqlx::query_as( - "INSERT INTO axiom_violations (id, kb_id, kind, left_fact, right_fact, path) - VALUES ($1, $2, $3, $4, $5, $6) + "INSERT INTO axiom_violations (id, kb_id, kind, left_fact, right_fact, path, detail) + VALUES ($1, $2, $3, $4, $5, $6, $7) ON CONFLICT (kb_id, kind, left_fact, right_fact) DO NOTHING RETURNING id", ) @@ -273,6 +312,7 @@ pub async fn run(pool: &PgPool, kb_id: Uuid) -> AppResult { .bind(left) .bind(right) .bind(path) + .bind(&detail) .fetch_optional(&mut *tx) .await?; if id.is_some() { @@ -303,10 +343,144 @@ pub async fn run(pool: &PgPool, kb_id: Uuid) -> AppResult { .execute(&mut *tx) .await?; report.cleared = cleared.rows_affected() as usize; + + // 派生之间互撞的按规则对进 `ontology_defects`——根子是那两条声明，不是哪条事实。 + // 同一对谓词上可能有几种撞法（functional 与 asymmetric 各撞各的），唯一键只到 + // 谓词对，所以合成一行，几种撞法都写进 detail + let mut by_pair: HashMap<(Uuid, Uuid), Vec> = HashMap::new(); + let mut order: Vec<(Uuid, Uuid)> = Vec::new(); + for rc in &clashes.between_derivations { + let triple = |i: usize| { + let d = &derivation.facts[i]; + format!( + "{} · {} · {}", + names.entity(d.subject), + names.predicate(d.predicate), + names.entity(d.object) + ) + }; + let examples: Vec = rc + .pairs + .iter() + .take(3) + .map(|(i, j)| json!([triple(*i), triple(*j)])) + .collect(); + let key = (rc.a.0, rc.b.0); + if !by_pair.contains_key(&key) { + order.push(key); + } + by_pair.entry(key).or_default().push(json!({ + "rule_a": rc.a.1.as_str(), + "via_a": names.predicate(rc.a.0), + "rule_b": rc.b.1.as_str(), + "via_b": names.predicate(rc.b.0), + "axiom": rc.axiom.as_str(), + "count": rc.pairs.len(), + "examples": examples, + })); + } + let mut fresh_defects: Vec = Vec::with_capacity(order.len()); + for key in order { + let rules = by_pair.remove(&key).unwrap_or_default(); + let count: usize = rules + .iter() + .map(|r| r["count"].as_u64().unwrap_or(0) as usize) + .sum(); + // 已经有人认可过的那一行保持 resolved，只刷 detail：0017 说认可之后不再报 + let (id,): (Uuid,) = sqlx::query_as( + "INSERT INTO ontology_defects (id, kb_id, kind, subject, other, path, detail) + VALUES ($1, $2, 'rules_disagree', $3, $4, '{}', $5) + ON CONFLICT (kb_id, kind, subject, other) DO UPDATE SET detail = EXCLUDED.detail + RETURNING id", + ) + .bind(Uuid::now_v7()) + .bind(kb_id) + .bind(key.0) + .bind(key.1) + .bind(json!({ "count": count, "rules": rules })) + .fetch_one(&mut *tx) + .await?; + fresh_defects.push(id); + } + sqlx::query( + "DELETE FROM ontology_defects + WHERE kb_id = $1 AND kind = 'rules_disagree' AND status = 'open' + AND NOT (id = ANY($2))", + ) + .bind(kb_id) + .bind(&fresh_defects) + .execute(&mut *tx) + .await?; tx.commit().await?; Ok(report) } +/// 矛盾要写成人能读的话，而派生没有落库、没有文本可查——名字在这里补。 +struct Names { + entities: HashMap, + predicates: HashMap, +} + +impl Names { + fn entity(&self, id: Uuid) -> String { + self.entities + .get(&id) + .cloned() + .unwrap_or_else(|| "?".into()) + } + fn predicate(&self, id: Uuid) -> String { + self.predicates + .get(&id) + .cloned() + .unwrap_or_else(|| "?".into()) + } +} + +async fn names_for( + pool: &PgPool, + derivation: &Derivation, + clashes: &Contradictions, +) -> AppResult { + let mut ents: HashSet = HashSet::new(); + let mut preds: HashSet = HashSet::new(); + let mut want = |i: usize| { + let d = &derivation.facts[i]; + ents.insert(d.subject); + ents.insert(d.object); + preds.insert(d.predicate); + preds.insert(d.via); + }; + for c in &clashes.with_assertions { + want(c.derived); + } + for rc in &clashes.between_derivations { + for (i, j) in rc.pairs.iter().take(3) { + want(*i); + want(*j); + } + } + for rc in &clashes.between_derivations { + preds.insert(rc.a.0); + preds.insert(rc.b.0); + } + let ents: Vec = ents.into_iter().collect(); + let preds: Vec = preds.into_iter().collect(); + let entities: Vec<(Uuid, String)> = + sqlx::query_as("SELECT id, canonical_name FROM entities WHERE id = ANY($1)") + .bind(&ents) + .fetch_all(pool) + .await?; + let predicates: Vec<(Uuid, String)> = + sqlx::query_as("SELECT id, label FROM relation_types WHERE id = ANY($1)") + .bind(&preds) + .fetch_all(pool) + .await?; + Ok(Names { + entities: entities.into_iter().collect(), + predicates: predicates.into_iter().collect(), + }) +} + /// Review 页要看的:还没人表态的违规,连同两条事实的三元组文本。 /// /// 展开成文本在 SQL 里做而不是回来再查一遍:一页几十条,每条两个三元组, @@ -336,10 +510,20 @@ pub async fn open_violations( v.left_fact, l.text AS left_text, v.right_fact, rt.text AS right_text, coalesce(array_length(v.path, 1), 0) AS path_len, - v.detected_at + v.detected_at, v.detail, + lf.valid_to IS NULL AS left_open, + lf.confidence AS left_confidence, + EXISTS ( + SELECT 1 FROM entities e + JOIN entities x ON x.kb_id = e.kb_id AND x.id <> e.id + AND x.merged_into IS NULL + AND lower(x.canonical_name) = lower(e.canonical_name) + WHERE e.id IN (lf.subject_id, lf.object_id) + ) AS same_name_peers FROM axiom_violations v JOIN triple l ON l.id = v.left_fact JOIN triple rt ON rt.id = v.right_fact + JOIN facts lf ON lf.id = v.left_fact WHERE v.kb_id = $1 AND v.status = 'open' ORDER BY v.detected_at DESC LIMIT $2 OFFSET $3", @@ -348,7 +532,60 @@ pub async fn open_violations( .bind(limit) .bind(offset) .fetch_all(pool) - .await?) + .await? + .into_iter() + .map(|r: ViolationRow| { + let hint = if r.kind == "derived_contradiction" { + hint_for(&r).map(String::from) + } else { + None + }; + AxiomViolation { + id: r.id, + kind: r.kind, + predicate: r.predicate, + left_fact: r.left_fact, + left_text: r.left_text, + right_fact: r.right_fact, + right_text: r.right_text, + path_len: r.path_len, + detected_at: r.detected_at, + detail: r.detail, + hint, + } + }) + .collect()) +} + +#[derive(sqlx::FromRow)] +struct ViolationRow { + id: Uuid, + kind: String, + predicate: Option, + left_fact: Uuid, + left_text: String, + right_fact: Uuid, + right_text: String, + path_len: i32, + detected_at: chrono::DateTime, + detail: serde_json::Value, + left_open: bool, + left_confidence: f32, + same_name_peers: bool, +} + +/// 线索按最常见的错法排（0017 §2）：旧断言没写结束日期、两个同名实体、抽取本来就 +/// 没把握。一次只给一条——三条并列等于没给 +fn hint_for(r: &ViolationRow) -> Option<&'static str> { + if r.left_open && r.detail.get("valid_from").is_some_and(|v| !v.is_null()) { + Some("stale") + } else if r.same_name_peers { + Some("duplicate") + } else if r.left_confidence < 0.75 { + Some("unsure") + } else { + None + } } /// 人裁决一处违规。 @@ -463,7 +700,8 @@ pub async fn check_ontology(pool: &PgPool, kb_id: Uuid) -> AppResult 'rules_disagree' + AND NOT (id = ANY($2))", ) .bind(kb_id) .bind(&fresh) @@ -497,6 +735,84 @@ pub struct DeriveReport { /// 而下游靠它推出的 `employs` 反倒进了库——一条派生的前提凭空消失。 /// 数出来，别再让它静默一次 pub unruled: usize, + /// 推出来了却撞上断言或别的派生、这一轮拦下没落的（0017）。**拦下的每一条 + /// 都在 Review 里有对应的一行**——`run` 与这里用同一个函数算 + pub blocked: usize, +} + +/// 一次取数，三样东西：带区间的边、每条事实的区间、精度与置信度。 +/// `run` 与 `materialize` 共用——两边看到的边必须是同一批 +type TimedEdges = ( + Vec, + HashMap, Option)>, + HashMap, Option, f32)>, +); + +async fn timed_edges(pool: &PgPool, kb_id: Uuid) -> AppResult { + // 输入**只有断言**。派生住在另一张表，所以这里连过滤都不必写——那正是 + // 分表买到的东西：忘了排除的后果是推不出东西，不是把自己的输出喂回自己 + let rows: Vec = sqlx::query_as( + "SELECT id, predicate_id, subject_id, object_id, + valid_from, valid_to, valid_from_precision, valid_to_precision, confidence + FROM facts + WHERE kb_id = $1 + AND invalidated_at IS NULL + AND predicate_id IS NOT NULL + AND object_id IS NOT NULL", + ) + .bind(kb_id) + .fetch_all(pool) + .await?; + + let mut edges = Vec::with_capacity(rows.len()); + let mut meta: HashMap, Option, f32)> = HashMap::new(); + let mut spans: HashMap, Option)> = HashMap::new(); + for (id, pred, subj, obj, from, to, fp, tp, conf) in rows { + let (f, t) = (from.map(|x| x.timestamp()), to.map(|x| x.timestamp())); + edges.push(TimedEdge { + edge: Edge { + fact: id, + predicate: pred, + subject: subj, + object: obj, + }, + from: f, + to: t, + }); + spans.insert(id, (f, t)); + meta.insert(id, (fp, tp, conf)); + } + Ok((edges, spans, meta)) +} + +/// 人认可过并存的（派生三元组, 断言）对：这些派生下一轮照常落地（0017 §2）。 +async fn accepted_clashes( + pool: &PgPool, + kb_id: Uuid, +) -> AppResult> { + let rows: Vec<(Uuid, serde_json::Value)> = sqlx::query_as( + "SELECT left_fact, detail FROM axiom_violations + WHERE kb_id = $1 AND kind = 'derived_contradiction' AND resolution = 'accepted'", + ) + .bind(kb_id) + .fetch_all(pool) + .await?; + let id = |v: &serde_json::Value, k: &str| { + v.get(k) + .and_then(|x| x.as_str()) + .and_then(|s| s.parse::().ok()) + }; + Ok(rows + .into_iter() + .filter_map(|(against, d)| { + Some(( + id(&d, "subject_id")?, + id(&d, "predicate_id")?, + id(&d, "object_id")?, + against, + )) + }) + .collect()) } /// 派生事实的身份：三元组 + 区间。 @@ -610,52 +926,40 @@ type LiveRow = ( pub async fn materialize(pool: &PgPool, kb_id: Uuid) -> AppResult { let ax = axioms(pool, kb_id).await?; let rules = compile_rules(pool, kb_id, &ax).await?; - - // 输入**只有断言**。派生住在另一张表，所以这里连过滤都不必写——那正是 - // 分表买到的东西：忘了排除的后果是推不出东西，不是把自己的输出喂回自己 - let rows: Vec = sqlx::query_as( - "SELECT id, predicate_id, subject_id, object_id, - valid_from, valid_to, valid_from_precision, valid_to_precision, confidence - FROM facts - WHERE kb_id = $1 - AND invalidated_at IS NULL - AND predicate_id IS NOT NULL - AND object_id IS NOT NULL", - ) - .bind(kb_id) - .fetch_all(pool) - .await?; - - let mut edges = Vec::with_capacity(rows.len()); - let mut meta: HashMap, Option, f32)> = HashMap::new(); - let mut spans: HashMap, Option)> = HashMap::new(); - for (id, pred, subj, obj, from, to, fp, tp, conf) in rows { - let (f, t) = (from.map(|x| x.timestamp()), to.map(|x| x.timestamp())); - edges.push(TimedEdge { - edge: Edge { - fact: id, - predicate: pred, - subject: subj, - object: obj, - }, - from: f, - to: t, - }); - spans.insert(id, (f, t)); - meta.insert(id, (fp, tp, conf)); - } + let (edges, spans, meta) = timed_edges(pool, kb_id).await?; let derivation = utopia_reason::derive::derive(&edges, &ax); + // asserted > derived 是硬性的（0002）：撞上断言的派生不落地。人认可过并存的 + // 除外；派生之间互撞的两边都不落，认可与否只影响报不报（0017） + let clashes = utopia_reason::derive::contradictions(&derivation, &edges, &ax, &spans); + let accepted = accepted_clashes(pool, kb_id).await?; + let mut blocked: HashSet = HashSet::new(); + for c in &clashes.with_assertions { + let d = &derivation.facts[c.derived]; + if !accepted.contains(&(d.subject, d.predicate, d.object, c.against)) { + blocked.insert(c.derived); + } + } + for rc in &clashes.between_derivations { + for (i, j) in &rc.pairs { + blocked.insert(*i); + blocked.insert(*j); + } + } let mut report = DeriveReport { rules: rules.len(), edges: edges.len(), derived: derivation.facts.len(), capped: derivation.capped.len(), + blocked: blocked.len(), ..Default::default() }; let mut wanted: HashMap = HashMap::new(); - for d in &derivation.facts { + for (i, d) in derivation.facts.iter().enumerate() { + if blocked.contains(&i) { + continue; + } let Some((from, to)) = utopia_reason::derive::validity(&d.premises, &spans) else { continue; }; @@ -776,9 +1080,9 @@ pub async fn open_defects( offset: i64, ) -> AppResult> { Ok(sqlx::query_as( - "SELECT d.id, d.kind, + "SELECT d.id, d.kind, d.detail, COALESCE(st.label, sr.label) AS subject_label, - ot.label AS other_label, + COALESCE(ot.label, orr.label) AS other_label, COALESCE( (SELECT array_agg(t.label ORDER BY x.ord) FROM unnest(d.path) WITH ORDINALITY AS x(id, ord) @@ -790,6 +1094,7 @@ pub async fn open_defects( LEFT JOIN entity_types st ON st.id = d.subject LEFT JOIN relation_types sr ON sr.id = d.subject LEFT JOIN entity_types ot ON ot.id = d.other + LEFT JOIN relation_types orr ON orr.id = d.other WHERE d.kb_id = $1 AND d.status = 'open' ORDER BY d.detected_at DESC LIMIT $2 OFFSET $3", diff --git a/crates/utopia-store/tests/a_contradiction_points_upstream.rs b/crates/utopia-store/tests/a_contradiction_points_upstream.rs new file mode 100644 index 000000000..2ff4dd13b --- /dev/null +++ b/crates/utopia-store/tests/a_contradiction_points_upstream.rs @@ -0,0 +1,341 @@ +//! 0017：派生撞上断言时，让路这件事从静默变成可见。 +//! +//! `ceo_of ⊑ works_at`，`works_at` functional。Mira `ceo_of` Acme 推出 Mira `works_at` +//! Acme，而账本里说她 `works_at` Globex。这里守四件事： +//! +//! 1. **派生不落地，而队列里有一行。** `run` 记一条 `derived_contradiction`，left 是被撞 +//! 的断言，right 是最后一条前提，detail 写着推出来的三元组；`materialize` 拦下它。 +//! 2. **修了就落。** 给旧断言一个结束日期，派生的区间与它不再重叠，下一轮落地， +//! 队列里那一行随之清掉。 +//! 3. **认可就落。** 人说两边都对，`accepted` 之后派生照常落地，那一行留着不再报。 +//! 4. **派生之间互撞按规则对聚合。** 两个 ceo 推出两条互斥的 works_at，进 +//! `ontology_defects` 一行 `rules_disagree`，两条派生都不落。 +//! +//! 没有 `UTOPIA_DATABASE_URL` 时跳过而不是失败。自建自拆，绝不碰已有的库。 + +use sqlx::PgPool; +use utopia_store::reasoning; +use uuid::Uuid; + +struct Fixture { + org: Uuid, + user: Uuid, + kb: Uuid, + ceo_of: Uuid, + works_at: Uuid, + mira: Uuid, + acme: Uuid, + globex: Uuid, + initech: Uuid, +} + +async fn seed(pool: &PgPool) -> anyhow::Result { + let (org, ws, kb, user) = ( + Uuid::now_v7(), + Uuid::now_v7(), + Uuid::now_v7(), + Uuid::now_v7(), + ); + let etype = Uuid::now_v7(); + let (ceo_of, works_at) = (Uuid::now_v7(), Uuid::now_v7()); + let (mira, acme, globex, initech) = ( + Uuid::now_v7(), + Uuid::now_v7(), + Uuid::now_v7(), + Uuid::now_v7(), + ); + + sqlx::query("INSERT INTO organizations (id, name) VALUES ($1, 'contradiction-test')") + .bind(org) + .execute(pool) + .await?; + sqlx::query("INSERT INTO workspaces (id, org_id, name) VALUES ($1, $2, 'contradiction-test')") + .bind(ws) + .bind(org) + .execute(pool) + .await?; + sqlx::query( + "INSERT INTO users (id, org_id, email, display_name, password_hash) + VALUES ($1, $2, $1 || '@contradiction.test', 'c', 'x')", + ) + .bind(user) + .bind(org) + .execute(pool) + .await?; + sqlx::query( + "INSERT INTO knowledge_bases (id, workspace_id, name, materialize_inferences) + VALUES ($1, $2, 'contradiction-test', TRUE)", + ) + .bind(kb) + .bind(ws) + .execute(pool) + .await?; + sqlx::query( + "INSERT INTO entity_types (id, kb_id, key, label) VALUES ($1, $2, 'thing', 'Thing')", + ) + .bind(etype) + .bind(kb) + .execute(pool) + .await?; + sqlx::query( + "INSERT INTO relation_types (id, kb_id, key, label, functional) + VALUES ($1, $2, 'works_at', 'works at', TRUE)", + ) + .bind(works_at) + .bind(kb) + .execute(pool) + .await?; + sqlx::query( + "INSERT INTO relation_types (id, kb_id, key, label, sub_property_of) + VALUES ($1, $2, 'ceo_of', 'CEO of', $3)", + ) + .bind(ceo_of) + .bind(kb) + .bind(works_at) + .execute(pool) + .await?; + for (id, name) in [ + (mira, "Mira"), + (acme, "Acme"), + (globex, "Globex"), + (initech, "Initech"), + ] { + sqlx::query( + "INSERT INTO entities (id, kb_id, type_id, canonical_name) VALUES ($1, $2, $3, $4)", + ) + .bind(id) + .bind(kb) + .bind(etype) + .bind(name) + .execute(pool) + .await?; + } + Ok(Fixture { + org, + user, + kb, + ceo_of, + works_at, + mira, + acme, + globex, + initech, + }) +} + +async fn asserted( + pool: &PgPool, + f: &Fixture, + subject: Uuid, + predicate: Uuid, + object: Uuid, + from: Option<&str>, +) -> anyhow::Result { + let id = Uuid::now_v7(); + sqlx::query( + "INSERT INTO facts (id, kb_id, subject_id, predicate_id, object_id, confidence, + valid_from, valid_from_precision) + VALUES ($1, $2, $3, $4, $5, 0.9, $6::timestamptz, CASE WHEN $6 IS NULL THEN NULL ELSE 'day' END)", + ) + .bind(id) + .bind(f.kb) + .bind(subject) + .bind(predicate) + .bind(object) + .bind(from) + .execute(pool) + .await?; + Ok(id) +} + +async fn live_derived(pool: &PgPool, f: &Fixture) -> anyhow::Result> { + Ok(sqlx::query_as( + "SELECT subject_id, object_id FROM derived_facts + WHERE kb_id = $1 AND invalidated_at IS NULL ORDER BY subject_id, object_id", + ) + .bind(f.kb) + .fetch_all(pool) + .await?) +} + +async fn open_contradictions( + pool: &PgPool, + f: &Fixture, +) -> anyhow::Result> { + Ok(sqlx::query_as( + "SELECT id, left_fact, detail FROM axiom_violations + WHERE kb_id = $1 AND kind = 'derived_contradiction' AND status = 'open'", + ) + .bind(f.kb) + .fetch_all(pool) + .await?) +} + +#[tokio::test] +async fn a_contradiction_points_upstream() -> anyhow::Result<()> { + let Ok(url) = std::env::var("UTOPIA_DATABASE_URL") else { + eprintln!("跳过：未设 UTOPIA_DATABASE_URL"); + return Ok(()); + }; + let pool = PgPool::connect(&url).await?; + let f = seed(&pool).await?; + + let run = async { + // Mira works_at Globex（没写结束日期）；Mira ceo_of Acme 自 2024 起 + let old = asserted(&pool, &f, f.mira, f.works_at, f.globex, Some("2020-01-01")).await?; + let ceo = asserted(&pool, &f, f.mira, f.ceo_of, f.acme, Some("2024-01-01")).await?; + + // 1. 派生不落地，队列里有一行 + let m = reasoning::materialize(&pool, f.kb).await?; + assert_eq!(m.derived, 1); + assert_eq!( + m.blocked, 1, + "the derivation that hits an assertion stays out" + ); + assert_eq!(m.inserted, 0); + assert!(live_derived(&pool, &f).await?.is_empty()); + + let r = reasoning::run(&pool, f.kb).await?; + assert_eq!(r.contradictions, 1); + assert_eq!(r.rules_disagree, 0); + let rows = open_contradictions(&pool, &f).await?; + assert_eq!(rows.len(), 1); + let (vid, left, detail) = &rows[0]; + assert_eq!(*left, old, "left is the assertion that was hit"); + assert_eq!(detail["axiom"], "functional"); + assert_eq!(detail["rule"], "sub_property"); + assert_eq!(detail["subject"], "Mira"); + assert_eq!(detail["predicate"], "works at"); + assert_eq!(detail["object"], "Acme"); + assert_eq!(detail["via_label"], "CEO of"); + assert_eq!(detail["premises"][0], serde_json::json!(ceo)); + let (right,): (Uuid,) = + sqlx::query_as("SELECT right_fact FROM axiom_violations WHERE id = $1") + .bind(vid) + .fetch_one(&pool) + .await?; + assert_eq!(right, ceo, "right is the last premise"); + + // Review 给的线索：旧断言没写结束日期、派生起得更晚 → stale + let page = reasoning::open_violations(&pool, f.kb, 50, 0).await?; + let card = page + .iter() + .find(|v| v.id == *vid) + .expect("card on the page"); + assert_eq!(card.hint.as_deref(), Some("stale")); + assert_eq!(card.detail["subject"], "Mira"); + + // 重跑幂等：还是那一行 + reasoning::run(&pool, f.kb).await?; + assert_eq!(open_contradictions(&pool, &f).await?.len(), 1); + + // 2. 修了就落：给旧断言一个结束日期，区间不再重叠 + sqlx::query( + "UPDATE facts SET valid_to = '2023-06-30'::timestamptz, valid_to_precision = 'day' + WHERE id = $1", + ) + .bind(old) + .execute(&pool) + .await?; + let m = reasoning::materialize(&pool, f.kb).await?; + assert_eq!(m.blocked, 0); + assert_eq!( + m.inserted, 1, + "once the assertion ends, the derivation lands" + ); + assert_eq!(live_derived(&pool, &f).await?, vec![(f.mira, f.acme)]); + reasoning::run(&pool, f.kb).await?; + assert!( + open_contradictions(&pool, &f).await?.is_empty(), + "the queue row clears with the contradiction" + ); + + // 3. 认可就落：把结束日期拿掉，矛盾回来；人说两边都对，派生照常落地 + sqlx::query("UPDATE facts SET valid_to = NULL, valid_to_precision = NULL WHERE id = $1") + .bind(old) + .execute(&pool) + .await?; + let m = reasoning::materialize(&pool, f.kb).await?; + assert_eq!(m.blocked, 1); + assert_eq!(m.invalidated, 1, "the landed derivation is withdrawn again"); + reasoning::run(&pool, f.kb).await?; + let rows = open_contradictions(&pool, &f).await?; + assert_eq!(rows.len(), 1); + reasoning::decide(&pool, f.kb, rows[0].0, "accepted", f.user).await?; + let m = reasoning::materialize(&pool, f.kb).await?; + assert_eq!(m.blocked, 0, "an accepted pair lands"); + assert_eq!(live_derived(&pool, &f).await?, vec![(f.mira, f.acme)]); + let r = reasoning::run(&pool, f.kb).await?; + assert_eq!(r.contradictions, 1, "still counted"); + assert!( + open_contradictions(&pool, &f).await?.is_empty(), + "but the accepted row stays resolved and nothing new is opened" + ); + + // 4. 派生之间互撞：先把旧断言闭合掉，让断言不再参与；再来一个 ceo_of Initech， + // 两条 works_at 由同一条规则推出、互斥——按规则对报一次，两条都不落 + sqlx::query( + "UPDATE facts SET valid_to = '2023-06-30'::timestamptz, valid_to_precision = 'day' + WHERE id = $1", + ) + .bind(old) + .execute(&pool) + .await?; + let ceo2 = asserted(&pool, &f, f.mira, f.ceo_of, f.initech, Some("2024-01-01")).await?; + let m = reasoning::materialize(&pool, f.kb).await?; + assert_eq!(m.derived, 2); + assert_eq!(m.blocked, 2, "both sides of a rule clash stay out"); + assert_eq!(m.invalidated, 1, "the one that had landed is withdrawn"); + assert!(live_derived(&pool, &f).await?.is_empty()); + let r = reasoning::run(&pool, f.kb).await?; + assert_eq!(r.contradictions, 0); + assert_eq!(r.rules_disagree, 1); + let defects: Vec<(Uuid, Option, serde_json::Value)> = sqlx::query_as( + "SELECT subject, other, detail FROM ontology_defects + WHERE kb_id = $1 AND kind = 'rules_disagree' AND status = 'open'", + ) + .bind(f.kb) + .fetch_all(&pool) + .await?; + assert_eq!(defects.len(), 1); + assert_eq!(defects[0].0, f.ceo_of); + assert_eq!(defects[0].1, Some(f.ceo_of)); + assert_eq!(defects[0].2["count"], 1); + assert_eq!(defects[0].2["rules"][0]["axiom"], "functional"); + assert_eq!(defects[0].2["rules"][0]["rule_a"], "sub_property"); + assert_eq!(defects[0].2["rules"][0]["via_a"], "CEO of"); + let page = reasoning::open_defects(&pool, f.kb, 50, 0).await?; + let card = page + .iter() + .find(|d| d.kind == "rules_disagree") + .expect("the rule clash is on the page"); + assert_eq!(card.subject_label.as_deref(), Some("CEO of")); + assert_eq!(card.other_label.as_deref(), Some("CEO of")); + + // 撤掉第二个 ceo：规则对的那一行清掉，第一条派生重新落地 + sqlx::query("UPDATE facts SET invalidated_at = now() WHERE id = $1") + .bind(ceo2) + .execute(&pool) + .await?; + reasoning::run(&pool, f.kb).await?; + let (n,): (i64,) = sqlx::query_as( + "SELECT count(*) FROM ontology_defects + WHERE kb_id = $1 AND kind = 'rules_disagree' AND status = 'open'", + ) + .bind(f.kb) + .fetch_one(&pool) + .await?; + assert_eq!(n, 0, "a rule clash clears when its derivations go"); + let m = reasoning::materialize(&pool, f.kb).await?; + assert_eq!(m.blocked, 0); + assert_eq!(live_derived(&pool, &f).await?, vec![(f.mira, f.acme)]); + anyhow::Ok(()) + } + .await; + + let _ = sqlx::query("DELETE FROM organizations WHERE id = $1") + .bind(f.org) + .execute(&pool) + .await; + run +} diff --git a/docs/decisions/0002-reasoning-engine.md b/docs/decisions/0002-reasoning-engine.md index 976eb23fb..d18a742bf 100644 --- a/docs/decisions/0002-reasoning-engine.md +++ b/docs/decisions/0002-reasoning-engine.md @@ -75,6 +75,8 @@ CREATE TABLE fact_derivations ( > **修订记录（2026-09-02）**：表格三行里只有第一行的前半兑现了——`asserted` 硬性优先，已断言的三元组不再派生（`derive.rs`）。 > 「记一条规则与事实矛盾的信号」**没有**，「派生 vs 派生进 Review」**没有**（同一三元组的多条推导只留第一条证明）。两者都还是待做。 +> +> **修订记录（2026-09-03）**：两行都兑现了，方案见 [0017](0017-a-contradiction-points-upstream.md)。派生撞断言：`derive::contradictions` 逐条算出，`run` 记成 `axiom_violations` 一种 `derived_contradiction`（单谓词封顶 50），`materialize` 用同一个函数拦下不落地；卡片给线索（旧断言没结束日期、同名实体、置信度低）与修法（闭合、撤回、认可）。派生撞派生：按规则对聚合进 `ontology_defects` 一种 `rules_disagree`，两边都不落——根子是那两条声明，不是哪条事实。 ### 3. 前提撤回时——双时态是最优解，不是负担 diff --git a/docs/decisions/0016-close-the-open-seams-before-cutting-new-ones.md b/docs/decisions/0016-close-the-open-seams-before-cutting-new-ones.md index 02fff13e2..e695fd251 100644 --- a/docs/decisions/0016-close-the-open-seams-before-cutting-new-ones.md +++ b/docs/decisions/0016-close-the-open-seams-before-cutting-new-ones.md @@ -67,7 +67,7 @@ Chat memory 与 MCP 两处在 A1 / A2 落地前标 in development。中英两份 ### B · 推理机补完——A 之后，与 C 并行 **B1 · R2 证明树。**〔已做，`feat/proof-tree`；实际是链不是树，理由见 0002 R2 的修订〕递归展开到叶子 chunk 的 API + 实体面板里可展开的树。数据结构（`fact_derivations`）已够。 -**B2 · 派生 vs 断言矛盾要有信号。** `axiom_violations` 加一种 kind（`derived_contradiction`），进 Review 同一档——0002 写了没做的那一行。 +**B2 · 派生 vs 断言矛盾要有信号。** `axiom_violations` 加一种 kind（`derived_contradiction`），进 Review 同一档——0002 写了没做的那一行。（完整方案见 [0017](0017-a-contradiction-points-upstream.md)；B2a 引擎与队列已做，B2b 图与面板上的可见性待做。） **B3 · `disjointWith` 进消解，合并路径复核签名。** `classify_type_drift` 改从 `entity_type_disjoint` 读（没声明就退回今天的行为，不硬编码）； `merge_entities` 搬事实前跑一遍与写入时相同的 domain / range 检查，违反的进 `axiom_violations` 而不是静默搬过去。这是 0009 与 0012 各自待做的同一件事。 〔**签名那一半已提前做了**（#190 / #196 逼出来的，A 线里插队）：`ontology::judge_direction` 一处判断，抽取与采纳共用；合并后对搬动过的事实报 `signature` 违规；R0 多一类。剩下 `disjointWith` 进消解那一半仍在这里。〕 diff --git a/docs/decisions/0017-a-contradiction-points-upstream.md b/docs/decisions/0017-a-contradiction-points-upstream.md index 82cd813fb..faecada80 100644 --- a/docs/decisions/0017-a-contradiction-points-upstream.md +++ b/docs/decisions/0017-a-contradiction-points-upstream.md @@ -1,6 +1,6 @@ # 0017 · A contradiction points at an error upstream -- **Status**: planned · B2 of 0016, wider than the one line written there: contradictions become visible everywhere, not only as a new kind in the queue +- **Status**: B2a implemented (engine and queue: `derive::contradictions`, migration 0020, the Review card with clues and repairs) · B2b (visibility in the graph and the entity panel) still planned · B2 of 0016, wider than the one line written there: contradictions become visible everywhere, not only as a new kind in the queue - **Written**: 2026-09-03 (conventions in [README](README.md)) - **Related**: the two unbuilt rows of the "derived vs asserted" table in [0002](0002-reasoning-engine.md) §2; [0016](0016-close-the-open-seams-before-cutting-new-ones.md) B2; the proof chain (B1, #227) supplies the "premises expand to the sentence" half of the card below diff --git a/docs/decisions/README.md b/docs/decisions/README.md index 264bce745..a32bd2d47 100644 --- a/docs/decisions/README.md +++ b/docs/decisions/README.md @@ -42,7 +42,7 @@ | 0014 | [身份跟着人，范围跟着令牌](0014-identity-from-the-person-scope-from-the-token.md) | 已实施（#180）· MCP 只读五工具 · 令牌页在账户层（A2）· 误导性的占位 crate 已删 | | 0015 | [记下一句话，不等于断言一个事实](0015-recording-a-sentence-is-not-asserting-a-fact.md) | 已实施 · 记忆抽出的事实进 `pending_facts`，Review 新档 + 跟在 remember 步骤后的确认卡 · `remember` 重新打开 · MCP 放开写是下一刀 | | 0016 | [先把开着的口子收上，再开新的](0016-close-the-open-seams-before-cutting-new-ones.md) | 规划中 · v0.1.0 之后的排期：A 收口 → B 推理机 ∥ C 尺子与本体 → D 语义层 → E 企业交付；模拟引擎后置 | -| 0017 | [A contradiction points at an error upstream](0017-a-contradiction-points-upstream.md) | 规划中 · 0016 B2 的完整方案：派生撞断言逐条封顶、派生撞派生按规则聚合、卡片给线索与修法、争议在图和面板上原地可见（新警戒色）| +| 0017 | [A contradiction points at an error upstream](0017-a-contradiction-points-upstream.md) | B2a 已实现（引擎与队列：逐条封顶、按规则对聚合、卡片给线索与修法）· B2b 待做：争议在图和面板上原地可见（新警戒色）| ## 不是决策记录的那些 diff --git a/migrations/0020_a_contradiction_points_upstream.sql b/migrations/0020_a_contradiction_points_upstream.sql new file mode 100644 index 000000000..f893e5564 --- /dev/null +++ b/migrations/0020_a_contradiction_points_upstream.sql @@ -0,0 +1,34 @@ +-- 派生撞上断言时，让路这件事从静默变成可见（docs/decisions/0017）。 +-- +-- 0002 定了 asserted > derived：推出来的事实撞上账本里的断言就不落地。此前那一步 +-- 什么都不留——`ceo_of ⊑ works_at` 推出的 works_at 没了，人不知道有过这回事，也就 +-- 不知道该去看看是抽取错了、旧断言该闭合、还是两个「Mira」其实是一个人。 +-- +-- 一致性检查多一种 `derived_contradiction`：left 是被撞的断言，right 是派生的最后一条 +-- 前提，path 是全部前提；推出来的三元组本身没有落库、没有 id 可指，放进 `detail`。 +-- 出路多一条 `fact_closed`——最常见的修法是给旧断言一个结束日期。 +-- +-- 派生之间互撞（两条规则加在一起产出互斥的结论）按规则对聚合进 `ontology_defects`， +-- 一种 `rules_disagree`，`detail` 记规则对与几个例子。逐对进 Review 只会淹掉队列。 + +ALTER TABLE axiom_violations + DROP CONSTRAINT axiom_violations_kind_check, + ADD CONSTRAINT axiom_violations_kind_check CHECK (kind IN ( + 'self_loop', 'asymmetry', 'cycle', 'functional', 'signature', + 'derived_contradiction' + )), + DROP CONSTRAINT axiom_violations_resolution_check, + ADD CONSTRAINT axiom_violations_resolution_check CHECK (resolution IN ( + 'fact_retracted', 'fact_closed', 'axiom_relaxed', 'accepted' + )), + ADD COLUMN detail JSONB NOT NULL DEFAULT '{}'::jsonb; + +ALTER TABLE ontology_defects + DROP CONSTRAINT ontology_defects_kind_check, + ADD CONSTRAINT ontology_defects_kind_check CHECK (kind IN ( + 'symmetric_and_asymmetric', 'transitive_and_functional', 'subclass_cycle', + 'disjoint_with_ancestor', 'inherits_disjoint', + 'inverse_of_itself', 'inverse_not_mutual', 'sub_property_cycle', + 'rules_disagree' + )), + ADD COLUMN detail JSONB NOT NULL DEFAULT '{}'::jsonb; diff --git a/web/src/api.ts b/web/src/api.ts index 9fa6adf77..05d28ed1d 100644 --- a/web/src/api.ts +++ b/web/src/api.ts @@ -473,9 +473,33 @@ export interface MappingRevision { changed_at: string; } /** 一处公理违规（0002 R0）。判据来自本体自己声明的公理，没声明就不报 */ +/** derived_contradiction 独有（0017）：推出来的那条三元组——它没有落库， + * 只能在这里写出来。其它种类是 `{}` */ +export interface ViolationDetail { + axiom?: "functional" | "asymmetry" | "self_loop"; + rule?: "transitive" | "symmetric" | "inverse" | "sub_property"; + via_label?: string; + subject?: string; + predicate?: string; + object?: string; + valid_from?: string | null; + valid_to?: string | null; + premises?: string[]; +} +export type ViolationResolution = + | "fact_retracted" + | "fact_closed" + | "axiom_relaxed" + | "accepted"; export interface AxiomViolation { id: string; - kind: "self_loop" | "asymmetry" | "cycle" | "functional"; + kind: + | "self_loop" + | "asymmetry" + | "cycle" + | "functional" + | "signature" + | "derived_contradiction"; /** 判据来自哪条关系。判「公理写错了」时从这里进本体去改 */ predicate: string | null; left_fact: string; @@ -486,6 +510,10 @@ export interface AxiomViolation { /** 环的长度；其余三类为 0 */ path_len: number; detected_at: string; + detail: ViolationDetail; + /** 审核线索（0017 §2），一次只给一条：旧断言没写结束日期、有同名实体、 + * 抽取置信度低。没有就空 */ + hint: "stale" | "duplicate" | "unsure" | null; } /** 本体自己的一处自相矛盾。**与 AxiomViolation 不是一回事**：那个说 * 「事实与定义抵触」，这个说「定义自己站不住」，后者更根本 */ @@ -500,11 +528,27 @@ export interface OntologyDefect { // 0017 加的三类：都在谓词上，前两类关于逆，第三类是子属性成环 | "inverse_of_itself" | "inverse_not_mutual" - | "sub_property_cycle"; + | "sub_property_cycle" + // 0017：两条规则加在一起产出互斥的派生，按规则对聚合报一次 + | "rules_disagree"; subject_label: string | null; other_label: string | null; path_labels: string[]; detected_at: string; + detail: DefectDetail; +} +/** rules_disagree 独有：哪两条规则、撞在哪条公理上、几对、几个例子 */ +export interface DefectDetail { + count?: number; + rules?: { + rule_a: string; + via_a: string; + rule_b: string; + via_b: string; + axiom: string; + count: number; + examples: [string, string][]; + }[]; } export interface FactReviewItem { id: string; @@ -1720,11 +1764,15 @@ export const api = { decideViolation: ( kbId: string, violationId: string, - resolution: "fact_retracted" | "axiom_relaxed" | "accepted", + resolution: ViolationResolution, + closeAt?: string, ) => request<{ ok: boolean }>( `/api/v1/kbs/${kbId}/review/violations/${violationId}`, - { method: "POST", body: JSON.stringify({ resolution }) }, + { + method: "POST", + body: JSON.stringify({ resolution, close_at: closeAt ?? null }), + }, ), confirmFact: (kbId: string, factId: string) => request<{ ok: boolean }>(`/api/v1/kbs/${kbId}/facts/${factId}/confirm`, { diff --git a/web/src/i18n/en.ts b/web/src/i18n/en.ts index c2cce2958..367e56994 100644 --- a/web/src/i18n/en.ts +++ b/web/src/i18n/en.ts @@ -1303,6 +1303,16 @@ export const en = { defectInverseSelf: "Its own inverse — say symmetric instead", defectInverseNotMutual: "The inverse does not point back", defectSubPropertyCycle: "subPropertyOf runs in a circle", + defectRulesDisagree: "Two rules produce contradicting derivations", + rulesDisagreeCount: (n: number) => + `${n} pair(s) of derivations held back until this is settled`, + rulesDisagreeRule: ( + a: string, + va: string, + b: string, + vb: string, + axiom: string, + ) => `${a} on ${va} with ${b} on ${vb}, against ${axiom}`, defectNeverInstantiable: "no instance can ever satisfy it", defectFixed: "I fixed the ontology", defectAccepted: "Leave it", @@ -1325,6 +1335,24 @@ export const en = { /** 签名违规（#190 / #196）：一条事实的主语或宾语落在谓词声明的类型之外—— * 抽取时会掰正，采纳与合并这两条路从前绕过了检查 */ violationSignature: "Subject or object outside the declared types", + /** 0017：派生撞上断言。卡片是一次审核，线索指向上游的错 */ + violationDerived: "A derivation contradicts an assertion", + derivedLine: (s: string, p: string, o: string) => + `Derived: ${s} · ${p} · ${o}`, + derivedBy: (rule: string, via: string) => `by ${rule} on ${via}`, + assertedLine: (t: string) => `Asserted: ${t}`, + hintStale: + "The assertion has no end date and the derivation starts later. It may simply have ended.", + hintDuplicate: + "Two entities share this name. They may be the same one.", + hintUnsure: + "The assertion was extracted with low confidence. Read its sentence.", + hintReadBoth: "Read both sentences and decide which one is wrong.", + closeAssertion: "Give the assertion an end date", + retractAssertion: "Retract the assertion", + seeDuplicates: "See duplicates", + openOntology: "Open the ontology", + letBothStand: "Let both stand", violationVia: (p: string) => `via ${p}`, violationPath: (n: number) => `${n} facts in the cycle`, retractFact: "Data is wrong", diff --git a/web/src/i18n/zh.ts b/web/src/i18n/zh.ts index c5915ed25..f30986c00 100644 --- a/web/src/i18n/zh.ts +++ b/web/src/i18n/zh.ts @@ -1177,6 +1177,15 @@ export const zh: Strings = { defectInverseSelf: "自己是自己的逆——写成「对称」更直白", defectInverseNotMutual: "逆关系没有指回来", defectSubPropertyCycle: "子属性绕成了环", + defectRulesDisagree: "两条规则推出互相抵触的结论", + rulesDisagreeCount: (n: number) => `${n} 对派生等这里定了再落地`, + rulesDisagreeRule: ( + a: string, + va: string, + b: string, + vb: string, + axiom: string, + ) => `${va} 上的 ${a} 与 ${vb} 上的 ${b}，撞在 ${axiom} 上`, defectNeverInstantiable: "这个类永远不可能有实例", defectFixed: "已去本体里改了", defectAccepted: "先放着", @@ -1195,6 +1204,20 @@ export const zh: Strings = { violationCycle: "传递链绕成了环", violationFunctional: "该只有一个值，却有两个", violationSignature: "主语或宾语不在关系声明的类型里", + violationDerived: "推出来的与断言相抵触", + derivedLine: (s: string, p: string, o: string) => + `推出：${s} · ${p} · ${o}`, + derivedBy: (rule: string, via: string) => `由 ${via} 上的 ${rule}`, + assertedLine: (t: string) => `断言：${t}`, + hintStale: "这条断言没写结束日期，而推出来的那条起得更晚——它可能只是结束了。", + hintDuplicate: "有两个同名实体，它们可能是同一个。", + hintUnsure: "这条断言抽取时把握不大，去读一下原句。", + hintReadBoth: "读一下两边的原句，判断哪条错了。", + closeAssertion: "给断言一个结束日期", + retractAssertion: "撤掉断言", + seeDuplicates: "去看重复实体", + openOntology: "去本体页", + letBothStand: "两边都成立", violationVia: (p: string) => `依据 ${p}`, violationPath: (n: number) => `环上 ${n} 条事实`, retractFact: "数据错了", diff --git a/web/src/pages/Review.tsx b/web/src/pages/Review.tsx index 5c73892ac..6ca977c25 100644 --- a/web/src/pages/Review.tsx +++ b/web/src/pages/Review.tsx @@ -14,6 +14,7 @@ import { type ReviewHistoryEvent, type ReviewItem, type ReviewSide, + type ViolationResolution, } from "../api"; import { PendingFactRow, useCanDecide } from "./PendingFacts"; import { S } from "../i18n"; @@ -481,7 +482,9 @@ function DefectRow({ inverse_of_itself: S.review.defectInverseSelf, inverse_not_mutual: S.review.defectInverseNotMutual, sub_property_cycle: S.review.defectSubPropertyCycle, + rules_disagree: S.review.defectRulesDisagree, }[d.kind]; + const rules = d.kind === "rules_disagree" ? (d.detail.rules ?? []) : []; // 后两类的后果值得写出来：不可满足的类不会报错，它只是永远空着 const unsatisfiable = d.kind === "disjoint_with_ancestor" || d.kind === "inherits_disjoint"; @@ -506,6 +509,23 @@ function DefectRow({ {S.review.defectNeverInstantiable}

)} + {rules.length > 0 && ( +
+
{S.review.rulesDisagreeCount(d.detail.count ?? 0)}
+ {rules.map((r, i) => ( +
+
+ {S.review.rulesDisagreeRule(r.rule_a, r.via_a, r.rule_b, r.via_b, r.axiom)} +
+ {r.examples.map(([x, y], j) => ( +
+ {x} · {y} +
+ ))} +
+ ))} +
+ )}
+ + + + +
+ + ); +} + /* ---------- 页面：左栏分类 + 单类内容区 ---------- */ type Sel = @@ -788,10 +917,12 @@ export function Review() { mutationFn: ({ id, resolution, + closeAt, }: { id: string; - resolution: "fact_retracted" | "axiom_relaxed" | "accepted"; - }) => api.decideViolation(kb!.id, id, resolution), + resolution: ViolationResolution; + closeAt?: string; + }) => api.decideViolation(kb!.id, id, resolution, closeAt), onSettled: invalidate, }); // 检查是同步的纯计算,所以直接 mutate 不排队。跑完把报告留在按钮旁边—— @@ -1177,9 +1308,11 @@ export function Review() { violationAction.isPending && violationAction.variables?.id === v.id } - onDecide={(resolution) => - violationAction.mutate({ id: v.id, resolution }) + onDecide={(resolution, closeAt) => + violationAction.mutate({ id: v.id, resolution, closeAt }) } + onDuplicates={() => select("duplicates")} + onOntology={() => navigate({ to: "/ontology" })} /> ))} diff --git a/web/src/styles.css b/web/src/styles.css index 40cdb6aa6..85397ce83 100644 --- a/web/src/styles.css +++ b/web/src/styles.css @@ -31,6 +31,8 @@ --u-warn: #f2b66d; /* 浅玫瑰：深底上的危险"文字/描边/点"专用（够亮才可读） */ --u-danger: #ff9daf; + /* 0017：争议色。派生撞上断言、被挡下的派生——警告与危险之外的第三种 */ + --u-contest: #ff6a3d; /* 深红：危险"实底按钮"专用（浅玫瑰做底会发粉；亮红在单色 chrome 上嗓门过大），配白字 */ --u-danger-solid: #c9353a; --u-violet: #c4a5ff;