LeanRDF

Documentation

How to install, run and use LeanRDF: the command-line tools, the library API of every package, the certificate format, testing and contributing. The book explains the ideas; these pages are the manual.

  1. Getting started
    Install Lean, build every package, run each tool once and check the examples, in about ten minutes.
  2. Packages and installation
    The five Lake packages, what each one contains and requires, and how to depend on them from your own project.
  3. Command-line tools
    Every executable, its arguments, input formats, output and exit codes.
  4. The core library
    Terms, literals, triples, graphs and datasets; parsing and writing N-Triples, Turtle, N-Quads and TriG; XSD values.
  5. Semantics and entailment
    Interpretations and the four entailment relations, rules as data, the Derives relation and the soundness theorems you call.
  6. Certificates and the checker
    The certificate data type and JSON format, what the verified checker accepts and rejects, the soundness theorems, and the CertifyingDatalog export.
  7. The Elpi search
    Saturating a graph in Elpi under any proven rule list, reading the closure, and cutting certificates out of it.
  8. SPARQL
    Parsing and running SPARQL 1.1 queries from Lean, the algebra and its semantics, the correctness theorems, result formats and coverage.
  9. OWL 2 RL and EL
    The OWL conditions, the OWL 2 RL and EL rule lists, the soundness theorems, certificates under OWL, and classification.
  10. SHACL
    Reading shapes, validating, the report, the theorems that turn a report into a fact about the data, and the supported constraint components.
  11. oxilite
    Certifying a live oxilite store: setup, the RDFS and OWL profiles, auditing the materialized closure, recording and replaying runs.
  12. Testing and CI
    What each package's test suite checks, the W3C suites, axiom guards, recorded fixtures, the examples script and the CI jobs.
  13. Contributing
    The rules for proofs, how changes are specified with OpenSpec, how design is recorded in the typed graph, and the checks to run before a pull request.
  14. FAQ and troubleshooting
    Answers to the questions people ask first, and fixes for the problems they hit first.