Skip to content

Commit a540bb5

Browse files
hyperpolymathhyperpolymath
committed
docs(schema): add theorem-alignment RDF/SHACL model for cross-prover phase
1 parent 9b4aaa9 commit a540bb5

3 files changed

Lines changed: 292 additions & 0 deletions

File tree

‎README.adoc‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -467,6 +467,7 @@ ZKP proofs and dependent types enable tamper-evident knowledge exchange. VCL-DT
467467
* link:docs/drift-handling.adoc[Drift Handling] — Detection, repair, federation drift
468468
* link:docs/safety-and-fault-tolerance.adoc[Safety & Fault Tolerance] — Memory, kernel, platform, supply chain safety
469469
* link:docs/deployment-modes.adoc[Deployment Modes] — Standalone, federated, hybrid
470+
* link:docs/theorem-alignment-schema.adoc[Theorem Alignment Schema] — RDF/SHACL model for cross-prover theorem identity and alignment
470471
* link:docs/getting-started.adoc[Getting Started] — Step-by-step setup guide
471472
* link:docs/adoption-strategy.adoc[Adoption Strategy] — Target domains and rollout plan
472473
* link:docs/VCL-SPEC.adoc[VCL Specification] — 2785-line normative language spec

‎docs/theorem-alignment-schema.adoc‎

Lines changed: 122 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,122 @@
1+
= Theorem Alignment Schema (Phase 3)
2+
3+
This document defines the RDF landing target for cross-prover theorem alignment in VeriSimDB.
4+
It is intended to unblock ECHIDNA Phase 3 bulk alignment ingestion.
5+
6+
== Scope
7+
8+
The schema covers:
9+
10+
* Stable theorem identity per prover.
11+
* Equivalence and translation predicates across provers.
12+
* Provenance for translation artefacts.
13+
* Confidence scoring in `[0, 1]`.
14+
* Explicit negative alignment edges.
15+
16+
Normative schema file:
17+
18+
* `schemas/theorem-alignment.ttl`
19+
20+
== URI Model
21+
22+
=== Theorem identity URI
23+
24+
Format:
25+
26+
`https://hyperpolymath.org/verisimdb/theorem/{prover}/{url-encoded-theorem-name}`
27+
28+
Example:
29+
30+
`https://hyperpolymath.org/verisimdb/theorem/lean4/Mathlib.Algebra.Group.basic.mul_assoc`
31+
32+
=== Canonical form URI
33+
34+
Format:
35+
36+
`https://hyperpolymath.org/verisimdb/canonical/{sha256-hex}`
37+
38+
Each theorem identity must carry:
39+
40+
* `verisim:inProver`
41+
* `verisim:theoremName`
42+
* `verisim:canonicalHash`
43+
* `verisim:hasCanonicalForm`
44+
45+
== Canonical Form Rules
46+
47+
The canonical hash is computed from a canonical theorem representation with deterministic normalization.
48+
49+
Algorithm (v1):
50+
51+
1. Parse prover theorem term into an AST.
52+
2. Desugar syntax sugar to core forms.
53+
3. Alpha-normalize binders in encounter order (`v0`, `v1`, ...).
54+
4. Normalize implicit argument order and universe annotations.
55+
5. Normalize associative/commutative operator trees where semantics permit.
56+
6. Serialize to canonical s-expression UTF-8 text with LF newlines.
57+
7. Compute SHA-256 and store as `sha256:<64-lower-hex>`.
58+
59+
The canonicalizer version must be recorded in `verisim:canonicalVersion`.
60+
61+
== Required Predicates
62+
63+
The schema defines the required draft predicates from issue #3:
64+
65+
* `verisim:alignsTo`
66+
* `verisim:isTranslationOf`
67+
* `verisim:hasCanonicalForm`
68+
* `verisim:provedBy`
69+
* `verisim:portedVia`
70+
* `verisim:alignmentConfidence`
71+
* `verisim:cannotAlignTo`
72+
73+
Additionally, provenance is anchored with:
74+
75+
* `verisim:translationArtifactHash`
76+
* `verisim:alignmentTimestamp`
77+
78+
== Triple Shape
79+
80+
Alignments are modelled as a reified node (`verisim:AlignmentAssertion`) so confidence and provenance can be attached per edge.
81+
82+
Minimum required fields for each assertion:
83+
84+
* `verisim:sourceTheorem`
85+
* `verisim:targetTheorem`
86+
* `verisim:portedVia` (`verisim:Dedukti` | `verisim:OpenTheory` | `verisim:Manual`)
87+
* `verisim:translationArtifactHash`
88+
* `verisim:alignmentConfidence` (`0 <= x <= 1`)
89+
* `verisim:alignmentTimestamp`
90+
91+
SHACL constraints for these fields are included in `schemas/theorem-alignment.ttl`.
92+
93+
== Example (Turtle)
94+
95+
[source,turtle]
96+
----
97+
@prefix verisim: <https://hyperpolymath.org/verisimdb/schema/theorem-alignment#> .
98+
@prefix xsd: <http://www.w3.org/2001/XMLSchema#> .
99+
100+
<https://hyperpolymath.org/verisimdb/theorem/lean4/Mathlib.Algebra.Group.basic.mul_assoc>
101+
a verisim:TheoremIdentity ;
102+
verisim:inProver "lean4" ;
103+
verisim:theoremName "Mathlib.Algebra.Group.basic.mul_assoc" ;
104+
verisim:canonicalHash "sha256:4c7d11f0f2de7d0ef2f4f888c95c7556836af8f1df20f36f09aa7668ff77f597" .
105+
106+
<https://hyperpolymath.org/verisimdb/theorem/hol4/groupTheory$ASSOC>
107+
a verisim:TheoremIdentity ;
108+
verisim:inProver "hol4" ;
109+
verisim:theoremName "groupTheory$ASSOC" ;
110+
verisim:canonicalHash "sha256:4c7d11f0f2de7d0ef2f4f888c95c7556836af8f1df20f36f09aa7668ff77f597" ;
111+
verisim:isTranslationOf <https://hyperpolymath.org/verisimdb/theorem/lean4/Mathlib.Algebra.Group.basic.mul_assoc> ;
112+
verisim:alignsTo <https://hyperpolymath.org/verisimdb/theorem/lean4/Mathlib.Algebra.Group.basic.mul_assoc> .
113+
114+
<https://hyperpolymath.org/verisimdb/alignment/assertion/6f57f31e>
115+
a verisim:AlignmentAssertion ;
116+
verisim:sourceTheorem <https://hyperpolymath.org/verisimdb/theorem/lean4/Mathlib.Algebra.Group.basic.mul_assoc> ;
117+
verisim:targetTheorem <https://hyperpolymath.org/verisimdb/theorem/hol4/groupTheory$ASSOC> ;
118+
verisim:portedVia verisim:OpenTheory ;
119+
verisim:translationArtifactHash "sha256:bdd6a9f1f2b5951f0b0c8559cb27f152be6b7ccb3b1cc4aeb8fcf9e36a580f59" ;
120+
verisim:alignmentConfidence "0.98"^^xsd:decimal ;
121+
verisim:alignmentTimestamp "2026-04-18T15:00:00Z"^^xsd:dateTime .
122+
----

‎schemas/theorem-alignment.ttl‎

Lines changed: 169 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,169 @@
1+
@prefix verisim: <https://hyperpolymath.org/verisimdb/schema/theorem-alignment#> .
2+
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
3+
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
4+
@prefix owl: <http://www.w3.org/2002/07/owl#> .
5+
@prefix xsd: <http://www.w3.org/2001/XMLSchema#> .
6+
@prefix sh: <http://www.w3.org/ns/shacl#> .
7+
8+
verisim:TheoremIdentity a rdfs:Class ;
9+
rdfs:label "Theorem identity" ;
10+
rdfs:comment "A theorem in a specific prover namespace with a stable canonical hash." .
11+
12+
verisim:CanonicalForm a rdfs:Class ;
13+
rdfs:label "Canonical form" ;
14+
rdfs:comment "Canonical normal form used to produce a stable theorem hash." .
15+
16+
verisim:AlignmentAssertion a rdfs:Class ;
17+
rdfs:label "Alignment assertion" ;
18+
rdfs:comment "An explicit relation between two theorem identities with confidence and provenance." .
19+
20+
verisim:AlignmentMethod a rdfs:Class ;
21+
rdfs:label "Alignment method" ;
22+
rdfs:comment "Method used for theorem transfer (Dedukti, OpenTheory, manual)." .
23+
24+
verisim:Dedukti a verisim:AlignmentMethod .
25+
verisim:OpenTheory a verisim:AlignmentMethod .
26+
verisim:Manual a verisim:AlignmentMethod .
27+
28+
verisim:inProver a rdf:Property ;
29+
rdfs:domain verisim:TheoremIdentity ;
30+
rdfs:range xsd:string ;
31+
rdfs:comment "Prover name, for example Coq, Lean4, Isabelle, HOL4." .
32+
33+
verisim:theoremName a rdf:Property ;
34+
rdfs:domain verisim:TheoremIdentity ;
35+
rdfs:range xsd:string .
36+
37+
verisim:canonicalHash a rdf:Property ;
38+
rdfs:domain verisim:TheoremIdentity ;
39+
rdfs:range xsd:string ;
40+
rdfs:comment "Stable canonical-form digest (sha256:<hex>)." .
41+
42+
verisim:hasCanonicalForm a rdf:Property ;
43+
rdfs:domain verisim:TheoremIdentity ;
44+
rdfs:range verisim:CanonicalForm .
45+
46+
verisim:canonicalFormText a rdf:Property ;
47+
rdfs:domain verisim:CanonicalForm ;
48+
rdfs:range xsd:string .
49+
50+
verisim:canonicalVersion a rdf:Property ;
51+
rdfs:domain verisim:CanonicalForm ;
52+
rdfs:range xsd:string ;
53+
rdfs:comment "Canonicaliser version used for hash derivation." .
54+
55+
verisim:alignsTo a rdf:Property, owl:SymmetricProperty ;
56+
rdfs:domain verisim:TheoremIdentity ;
57+
rdfs:range verisim:TheoremIdentity ;
58+
rdfs:comment "Theorems are semantically equivalent up to translation." .
59+
60+
verisim:isTranslationOf a rdf:Property ;
61+
rdfs:domain verisim:TheoremIdentity ;
62+
rdfs:range verisim:TheoremIdentity ;
63+
rdfs:comment "Direction-aware theorem translation relation." .
64+
65+
verisim:provedBy a rdf:Property ;
66+
rdfs:domain verisim:TheoremIdentity ;
67+
rdfs:range xsd:string ;
68+
rdfs:comment "Prover engine that validated this theorem instance." .
69+
70+
verisim:cannotAlignTo a rdf:Property ;
71+
rdfs:domain verisim:TheoremIdentity ;
72+
rdfs:range verisim:TheoremIdentity ;
73+
rdfs:comment "Known impossible alignment (for example classical to constructive mismatch)." .
74+
75+
verisim:sourceTheorem a rdf:Property ;
76+
rdfs:domain verisim:AlignmentAssertion ;
77+
rdfs:range verisim:TheoremIdentity .
78+
79+
verisim:targetTheorem a rdf:Property ;
80+
rdfs:domain verisim:AlignmentAssertion ;
81+
rdfs:range verisim:TheoremIdentity .
82+
83+
verisim:portedVia a rdf:Property ;
84+
rdfs:domain verisim:AlignmentAssertion ;
85+
rdfs:range verisim:AlignmentMethod ;
86+
rdfs:comment "Translation route used to derive the alignment." .
87+
88+
verisim:translationArtifactHash a rdf:Property ;
89+
rdfs:domain verisim:AlignmentAssertion ;
90+
rdfs:range xsd:string ;
91+
rdfs:comment "Digest for translation artefact proving provenance of the edge." .
92+
93+
verisim:alignmentConfidence a rdf:Property ;
94+
rdfs:domain verisim:AlignmentAssertion ;
95+
rdfs:range xsd:decimal ;
96+
rdfs:comment "Confidence in [0, 1] for the alignment assertion." .
97+
98+
verisim:alignmentTimestamp a rdf:Property ;
99+
rdfs:domain verisim:AlignmentAssertion ;
100+
rdfs:range xsd:dateTime .
101+
102+
verisim:AlignmentAssertionShape a sh:NodeShape ;
103+
sh:targetClass verisim:AlignmentAssertion ;
104+
sh:property [
105+
sh:path verisim:sourceTheorem ;
106+
sh:minCount 1 ;
107+
sh:maxCount 1 ;
108+
sh:class verisim:TheoremIdentity ;
109+
] ;
110+
sh:property [
111+
sh:path verisim:targetTheorem ;
112+
sh:minCount 1 ;
113+
sh:maxCount 1 ;
114+
sh:class verisim:TheoremIdentity ;
115+
] ;
116+
sh:property [
117+
sh:path verisim:portedVia ;
118+
sh:minCount 1 ;
119+
sh:maxCount 1 ;
120+
sh:class verisim:AlignmentMethod ;
121+
] ;
122+
sh:property [
123+
sh:path verisim:translationArtifactHash ;
124+
sh:minCount 1 ;
125+
sh:maxCount 1 ;
126+
sh:datatype xsd:string ;
127+
] ;
128+
sh:property [
129+
sh:path verisim:alignmentConfidence ;
130+
sh:minCount 1 ;
131+
sh:maxCount 1 ;
132+
sh:datatype xsd:decimal ;
133+
sh:minInclusive 0 ;
134+
sh:maxInclusive 1 ;
135+
] ;
136+
sh:property [
137+
sh:path verisim:alignmentTimestamp ;
138+
sh:minCount 1 ;
139+
sh:maxCount 1 ;
140+
sh:datatype xsd:dateTime ;
141+
] .
142+
143+
verisim:TheoremIdentityShape a sh:NodeShape ;
144+
sh:targetClass verisim:TheoremIdentity ;
145+
sh:property [
146+
sh:path verisim:inProver ;
147+
sh:minCount 1 ;
148+
sh:maxCount 1 ;
149+
sh:datatype xsd:string ;
150+
] ;
151+
sh:property [
152+
sh:path verisim:theoremName ;
153+
sh:minCount 1 ;
154+
sh:maxCount 1 ;
155+
sh:datatype xsd:string ;
156+
] ;
157+
sh:property [
158+
sh:path verisim:canonicalHash ;
159+
sh:minCount 1 ;
160+
sh:maxCount 1 ;
161+
sh:datatype xsd:string ;
162+
sh:pattern "^sha256:[0-9a-f]{64}$" ;
163+
] ;
164+
sh:property [
165+
sh:path verisim:hasCanonicalForm ;
166+
sh:minCount 1 ;
167+
sh:maxCount 1 ;
168+
sh:class verisim:CanonicalForm ;
169+
] .

0 commit comments

Comments
 (0)