Skip to content

Commit 0f7bdc0

Browse files
jeswrclaude
andauthored
feat(owl2dl): data properties and datatypes in the hypertableau (ALCHIQ(D)) (#7089)
* feat(owl2dl): data properties and datatypes in the hypertableau (#7031) The (D) of ALCHIQ(D): data properties become roles whose edges end in concrete nodes (never blocked, never a clause's central node), and data ranges become atoms over the data-range oracle. Domain, range, sub / equivalent / disjoint data properties, functionality, the data restrictions (some, all, has-value, qualified cardinality), positive and negative data property assertions, facet restrictions, DataOneOf, the data booleans and acyclic DatatypeDefinitions are decided. At-most over a data range puts the complement range in the clause head; DisjointDataProperties gives a value inequality. The datatype check runs over the components of the inequality graph: per-node emptiness, peeling of nodes with more values than neighbours, exact backtracking over enumerated (OneOf) nodes and clique counting for the rest. Any other shape, or any Unknown from the oracle, closes the branch as undecided, and a run whose closed branches include an undecided one answers the new Unknown(DatatypeUnknown { source }) instead of Inconsistent. Ill-typed literals in assertions, has-value and one-of make the ontology inconsistent. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CKVo4KMh5saxramziiEiBc * test(owl2dl): HermiT differential corpus for data properties and datatypes A seeded generator of data property axioms, data restrictions over integer, decimal, string and boolean ranges (facets, one-of, the data booleans, a datatype definition) and data assertions whose literals denote one value in several datatypes and lexical forms, with answers recorded from HermiT. Every verdict must agree; Unknown answers are counted and capped. The constructs HermiT departs from the Direct Semantics on are kept out of the generator and documented there: ill-typed literals, single-value intervals at zero, data booleans under data cardinalities, float zeros and NegativeDataPropertyAssertion (used in its by-value class-assertion form instead); the hand-written tests cover them. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CKVo4KMh5saxramziiEiBc * fix(owl2dl): refuse datatype definitions that may have no model, even unused A DatatypeDefinition constrains every model whether or not the datatype is used: a cyclic definition (DT ≡ ¬DT), two different definitions of one datatype, or a redefined built-in can leave no model, so ignoring an unused one could report Consistent. Each definition is now expanded up front and those three cases answer Unknown(OutOfFragment). Also pins, by hand-written tests, each case the HermiT differential corpus leaves out because HermiT departs from the Direct Semantics. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CKVo4KMh5saxramziiEiBc * docs(inference): owl2dl reasoner decides ALCHIQ(D) The owl2dl reasoner paragraph now lists the data properties and data ranges in the decided fragment, literal identity by value, ill-typed literals as Inconsistent, the new Unknown(DatatypeUnknown) reason, what still answers Unknown(OutOfFragment), and the HermiT deviations kept out of the differential corpus. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CKVo4KMh5saxramziiEiBc * feat(js): checkOwlDl decides data properties; DatatypeUnknown reason The npm types and docs now describe the ALCHIQ(D) fragment: data properties are decided, and an undecided datatype question answers DatatypeUnknown with its triples. maxNodes is bounded to the wasm32 usize range in JS, option values are read from the property descriptors, and the same-realm requirement is documented. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CKVo4KMh5saxramziiEiBc --------- Co-authored-by: Claude <noreply@anthropic.com>
1 parent a36171b commit 0f7bdc0

15 files changed

Lines changed: 2961 additions & 143 deletions

File tree

‎crates/sparq-dl-wasm/README.md‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -39,6 +39,7 @@ Most callers want the typed wrapper instead: `import { checkOwlDl } from '@sparq
3939
{ "consistent": true | false | "unknown",
4040
"reason": null | { "kind": "OutOfFragment", "construct", "triples" }
4141
| { "kind": "NotInDl", "violations" } | { "kind": "ResourceBudget" }
42+
| { "kind": "DatatypeUnknown", "triples" }
4243
| { "kind": "ImportsNotLoaded", "imports" }
4344
| { "kind": "Unparsed" | "Malformed" | "Ambiguous" | "Unsupported", "detail", "triples" },
4445
"profile": { "dl": true | false | "unknown", "violations": [{ "kind", "detail", "triples" }],
@@ -51,8 +52,9 @@ Most callers want the typed wrapper instead: `import { checkOwlDl } from '@sparq
5152
[`skills/javascript-wasm/references/owl-dl.md`](../../skills/javascript-wasm/references/owl-dl.md).
5253
- **Fail-closed.** An ontology the reverse mapping refuses is a result
5354
(`"consistent": "unknown"` with the refusal as `reason`), not an error; only a parse error
54-
or malformed options throw. Data properties, datatypes and nominals are outside the
55-
decided fragment and answer `"unknown"` with reason `OutOfFragment`.
55+
or malformed options throw. Nominals, keys and other chains are outside the decided
56+
fragment and answer `"unknown"` with reason `OutOfFragment`; an undecided datatype question
57+
answers `DatatypeUnknown`.
5658
- **No serde.** The JSON is written (and the options object parsed) by a small hand-written,
5759
unit-tested JSON module; all logic is the plain-Rust `check_owl_dl_json`, tested natively
5860
with `cargo test -p sparq-dl-wasm`. The `#[wasm_bindgen]` export only maps the error;

‎crates/sparq-dl-wasm/src/lib.rs‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -184,6 +184,7 @@ fn reason_kind(reason: &UnknownReason) -> &'static str {
184184
UnknownReason::NotInDl(_) => "NotInDl",
185185
UnknownReason::ResourceBudget => "ResourceBudget",
186186
UnknownReason::ImportsNotLoaded(_) => "ImportsNotLoaded",
187+
UnknownReason::DatatypeUnknown { .. } => "DatatypeUnknown",
187188
}
188189
}
189190

@@ -262,6 +263,11 @@ impl Writer<'_> {
262263
self.key("imports");
263264
json::push_str_array(&mut self.out, iris.iter().map(String::as_str));
264265
}
266+
UnknownReason::DatatypeUnknown { source } => {
267+
self.raw(",");
268+
self.key("triples");
269+
self.triples(source);
270+
}
265271
UnknownReason::ResourceBudget => {}
266272
}
267273
self.raw("}");

‎crates/sparq-dl-wasm/src/tests.rs‎

Lines changed: 39 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -156,25 +156,56 @@ fn unsatisfiable_class_and_inferred_subclass() {
156156
}
157157

158158
#[test]
159-
fn data_properties_are_out_of_fragment_with_the_offending_triple() {
159+
fn data_properties_are_decided_and_ill_typed_literals_are_inconsistent() {
160+
let age = format!(
161+
"{ALCHIQ} :age a owl:DatatypeProperty , owl:FunctionalProperty ; rdfs:domain :Person ; rdfs:range xsd:nonNegativeInteger ."
162+
);
163+
let r = run(&age);
164+
assert_eq!(get(&r, "consistent"), &Value::Bool(true));
165+
assert_eq!(s(get(&r, "classification")), "complete");
166+
let r = run_with(&age, Some(":ann :age 16 ."), None);
167+
assert_eq!(get(&r, "consistent"), &Value::Bool(true));
168+
let r = run_with(&age, Some(":ann :age -1 ."), None);
169+
assert_eq!(get(&r, "consistent"), &Value::Bool(false));
170+
let r = run_with(
171+
&age,
172+
Some(":ann :age \"sixteen\"^^xsd:nonNegativeInteger ."),
173+
None,
174+
);
175+
assert_eq!(get(&r, "consistent"), &Value::Bool(false));
176+
}
177+
178+
#[test]
179+
fn nominals_are_out_of_fragment_with_the_offending_triple() {
160180
let r = run(&format!(
161-
"{ALCHIQ} :age a owl:DatatypeProperty ; rdfs:domain :Person ; rdfs:range xsd:integer ."
181+
"{ALCHIQ} :ann a owl:NamedIndividual . :Ann owl:equivalentClass [ a owl:Class ; owl:oneOf ( :ann ) ] ."
162182
));
163183
assert_eq!(s(get(&r, "consistent")), "unknown");
164184
let reason = get(&r, "reason");
165185
assert_eq!(s(get(reason, "kind")), "OutOfFragment");
166186
assert!(!s(get(reason, "construct")).is_empty());
167187
let triples = strs(get(reason, "triples"));
168188
assert!(!triples.is_empty());
169-
assert!(
170-
triples.iter().all(|t| t.contains("<http://ex/age>")),
171-
"{triples:?}"
172-
);
173189
for t in &triples {
174190
assert!(t.ends_with(" ."), "{t}");
175191
}
176-
// The profile check still ran and the ontology is in OWL 2 DL; only reasoning abstains.
177-
assert_eq!(get(get(&r, "profile"), "dl"), &Value::Bool(true));
192+
assert_eq!(get(&r, "classification"), &Value::Null);
193+
}
194+
195+
#[test]
196+
fn an_undecided_datatype_question_is_datatype_unknown_with_its_triples() {
197+
let r = run(&format!(
198+
"{ALCHIQ} :d a owl:DatatypeProperty ; rdfs:range [ a rdfs:Datatype ; owl:onDatatype xsd:string ; owl:withRestrictions ( [ xsd:pattern \"\\\\p{{IsBasicLatin}}+\" ] ) ] . :a :d \"x\" ."
199+
));
200+
assert_eq!(s(get(&r, "consistent")), "unknown");
201+
let reason = get(&r, "reason");
202+
assert_eq!(keys(reason), ["kind", "triples"]);
203+
assert_eq!(s(get(reason, "kind")), "DatatypeUnknown");
204+
let triples = strs(get(reason, "triples"));
205+
assert!(!triples.is_empty());
206+
for t in &triples {
207+
assert!(t.ends_with(" ."), "{t}");
208+
}
178209
assert_eq!(get(&r, "classification"), &Value::Null);
179210
}
180211

0 commit comments

Comments
 (0)