Release 1.5.0 (#234)

Version to 1.5.0 and a CHANGELOG section for the tag: the induced-ontology
tool and its page, lean/Fo and lean/Lrat with their checkers, the mu verdict,
the HQDM two-renderings figure, the sixth beat, the SHACL node-level
evaluation, and the CI and Windows fixes. 1.4.0 and 1.4.1 had no section;
the note says so rather than pretending otherwise.

Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>

Author: fabio-rovai

CHANGELOG.md

@@ -4,6 +4,43 @@ All notable changes to Open Ontologies are documented here.
 
 ## [Unreleased]
 
+## [1.5.0] - 2026-09-20
+
+1.4.0 and 1.4.1 were tagged without a section of their own; their entries are among the ones
+below, which cover everything since 1.3.0. New in this tag:
+
+### Added
+- **One sheet in, one ontology out.** `onto_induce` (and `induce` in batch) reads one data sheet
+  and induces an OWL class with typed properties, a SHACL shape the rows satisfy by construction,
+  and a loading mapping, with a sentence of evidence per induced statement. Cardinality is a shape
+  and never `owl:FunctionalProperty`; observed ranges are reported, never constrained; numbered
+  columns are one multi-valued property. The row loader now mints a cell outside its datatype's
+  lexical space as a plain string, so an ill-typed literal cannot slip past `sh:datatype`. (#233)
+- **`web/try/`, the "try it here" page**: one function running the pinned release binary in batch
+  mode; drop a sheet, read the evidence, edit a cell, re-check. (#233)
+- **A verified first-order resolution calculus, `lean/Fo`, and `oo-fores`.** `onto_fol_prove`
+  sends OWL 2 RL ontologies to the prover as clauses, translates Vampire's refutation into the
+  certificate format and has it checked: the ninth verdict word `refutation_certified` rests on
+  `Fo.unsat_of_check`. (#224, #225, #226, #227; decision 0005, second addendum)
+- **A verified LRAT checker, `lean/Lrat` and `oo-lrat`**, so a SAT solver's `unsat` is a proof and
+  not an opinion; picosat traces are translated to LRAT. (#222)
+- **`mu`, the tenth verdict word.** A goal that puts in class position a term the ontology never
+  uses as a class is returned unasked before any prover runs, with the term, its position and what
+  the file does call it. (#232)
+- **The checker names the theorem.** A `Certified` token carries the theorem the checker printed,
+  never the caller's guess. (#220)
+- **HQDM audited, both shipped renderings**, drawn side by side with the evidence recomputed by a
+  test; the second panel intersects this engine's undetermined set with HermiT's list. (#219, #230)
+- **The front-page figure reads its prover run** and has a sixth beat for the unasked question. (#229)
+
+### Changed
+- **SHACL: a node shape's own value constraints are evaluated** against the focus node for all four
+  target forms (W3C core suite: pass 35 → 61, fail 17 → 15). (#231)
+- CI installs `hnswlib` with `--no-cache` and `HNSWLIB_NO_NATIVE=1`; the cross-runner built-wheel
+  cache was the source of the `python` job's SIGILL. (#223)
+- Windows: the fake checker used by the verdict tests survives cmd.exe's quoting. (#220)
+
+
 ### Added
 - **A module carries a theorem; a slice carries a measurement.** `onto_module_extract` computes a
   syntactic locality module over a signature: `⊥`, `⊤` or the iterated `⊥⊤*`, the standard OWL API

Cargo.lock

@@ -1,6 +1,6 @@
 [package]
 name = "open-ontologies"
-version = "1.4.1"
+version = "1.5.0"
 edition = "2024"
 description = "AI-native ontology engine: an MCP server and CLI for building, validating, querying and reasoning over RDF and OWL, with a native SHIQ tableaux reasoner, SHACL validation and SPARQL. Single binary, no JVM."
 license = "MIT"