diff options
Diffstat (limited to '')
| -rw-r--r-- | README.md | 171 |
1 files changed, 95 insertions, 76 deletions
@@ -6,74 +6,92 @@ A persistent, formally verified knowledge base stored as a Git repository of Lea ## Core Concepts -- **Persistent**: stored as `.lean` files in a Git repository — survives across sessions. +- **Persistent**: state is stored as `--@kb` metadata comments in each domain file and reloaded automatically on startup — no state is lost between sessions. - **Formally verified**: every addition is type-checked by Lean's kernel at `kb check` / `kb commit` time. - **Domain-organised**: declarations are grouped into named domain files. Each domain is one `.lean` file. An agent can load a specific domain into its context without loading the entire KB. - **Version-controlled**: full history, branching, and reproducibility via Git. +- **Agent-friendly**: all commands return exit code `0` on success and `1` on error, with structured one-line error messages. + +--- + +## Persistence Model + +Every declaration written to disk is preceded by a metadata header: + +``` +--@kb kind=prop name=birthYear domain=People +opaque birthYear : Person → Nat +``` + +On startup, `kb` scans all `*.lean` domain files in the current directory, parses these headers, and reconstructs the full declaration list. This means: + +- Restarting `kb` is safe — all prior work is reloaded. +- The `--@kb` format is the source of truth; the Lean code is preserved exactly for the compiler. +- `rm` removes the entire `--@kb` block and its Lean source atomically, regardless of how many lines the source spans. --- ## Planned Domain Structure -The KB is organised into four top-level sections. Each subsection corresponds to one domain file — the natural unit an agent loads for a focused query. For example, an agent answering a chemistry question loads only `Chemistry`; one doing financial calculations loads only `MoneyFinance`. +The KB is organised into four top-level sections. Each subsection is one domain file — the natural unit an agent loads for a focused task. ### Mathematics | Domain file | Coverage | |-------------|----------| -| `LogicSetTheory` | Symbolic logic and foundations: Boolean algebra, set theory, transfinite numbers | -| `Probability` | Quantification of likelihood: games of chance, Bernoulli's trials, probability formulas, probability distributions | -| `AppliedMathematics` | Optimization, numerical analysis, dynamic systems, fractals, game theory, packing and covering objects | -| `ElementaryMath` | Arithmetic, fractions, percentages; reasoning about parity and sign of underspecified values | +| `LogicSetTheory` | Boolean algebra, set theory, transfinite numbers | +| `Probability` | Games of chance, Bernoulli's trials, probability formulas and distributions | +| `AppliedMathematics` | Optimization, numerical analysis, dynamic systems, fractals, game theory, packing | +| `ElementaryMath` | Arithmetic, fractions, percentages; parity and sign of underspecified values | | `Algebra` | Variables, number systems, algebraic operations and symbols | | `Geometry` | Plane, solid, coordinate, transformations, high-dimensional, packing, curves, polyforms, topology, tilings | | `Plotting` | Functions, equations, parametric plots, inequalities, number lines, polar plots | -| `Calculus` | Integrals, derivatives, limits, sequences, products, series, sums, vector analysis, transforms, continuity, domain & range | +| `Calculus` | Integrals, derivatives, limits, sequences, products, series, sums, vector analysis, transforms | | `DifferentialEquations` | Ordinary (ODE) and partial (PDE) differential equations | | `Statistics` | Descriptive statistics, inference, regression, random variables | -| `Functions` | Domain & range, injectivity, surjectivity, continuity, periodic, odd/even, special, number-theoretic, representation formulas | +| `Functions` | Domain & range, injectivity, surjectivity, continuity, periodic, odd/even, special functions | ### Science & Technology | Domain file | Coverage | |-------------|----------| -| `Physics` | Mechanics, oscillations & waves, statistical physics, thermodynamics, electricity & magnetism, optics, relativity, nuclear, quantum, particle, astrophysics, constants, principles, effects, fluid mechanics | -| `Chemistry` | Chemical elements, molecules, ions, quantities, reactions, thermodynamics, solutions, cheminformatics, quantum chemistry, functional groups, bonds & orbitals, nuclear chemistry | +| `Physics` | Mechanics, thermodynamics, electromagnetism, optics, relativity, nuclear, quantum, particle, astrophysics, fluid mechanics, physical constants | +| `Chemistry` | Elements, molecules, ions, quantities, reactions, thermodynamics, solutions, quantum chemistry, bonds & orbitals, nuclear chemistry | | `UnitsMeasures` | Conversion and analysis of scientific and everyday measurement systems | -| `Engineering` | Aerospace, energy, electrical, control systems, mechanical, civil, fluid mechanics, acoustics, steam tables, measurement devices | -| `HealthMedicine` | Physical exercise, human anatomy, medical codes, blood alcohol content, mortality data, diseases, medical computations, vision, medical tests, nuclear medicine, health-care statistics, drugs & prescriptions, public health | -| `TechnologicalWorld` | Communications, satellites, barcodes, space probes, photography, structures, nuclear power, nuclear explosions, carbon footprint, inventions, web & computer systems | -| `Materials` | Alloys, bulk materials, material hardness, minerals, plastics, woods, material chemistry | -| `ComputationalSciences` | Cellular automata, substitution systems, Turing machines, complexity, algebraic codes, fractals, image processing, hashing | +| `Engineering` | Aerospace, energy, electrical, control systems, mechanical, civil, fluid mechanics, acoustics, steam tables | +| `HealthMedicine` | Anatomy, medical codes, blood alcohol, mortality, diseases, medical computations, drugs, public health | +| `TechnologicalWorld` | Communications, satellites, barcodes, space probes, nuclear power, carbon footprint, inventions, web & computer systems | +| `Materials` | Alloys, bulk materials, hardness, minerals, plastics, woods, material chemistry | +| `ComputationalSciences` | Cellular automata, Turing machines, complexity, algebraic codes, fractals, image processing, hashing | | `EarthSciences` | Geology, geodesy & navigation, oceanography, atmospheric sciences, climate | | `LifeSciences` | Human anatomy, animal anatomy, neuroscience, genomics, molecular biology, animals and plants | | `SpaceAstronomy` | Phenomena and technology beyond Earth's atmosphere | -| `FoodScience` | Food composition, nutrition, dietary references & standards, food comparison & combinations, food physics | +| `FoodScience` | Food composition, nutrition, dietary standards, food physics | ### Society & Culture | Domain file | Coverage | |-------------|----------| -| `Education` | International education, universities, school districts, standardized tests, education statistics | +| `Education` | International education, universities, school districts, standardized tests | | `People` | Biographical and demographic data on notable individuals and public figures | -| `ArtsMedia` | Movies, television, video games, notable texts, periodicals, comics, fictional characters, popular curves, mythology, music | -| `History` | Historical numbers, historical periods, genealogy, historical events, historical countries, military conflicts, world leaders, inventions | -| `WordsLinguistics` | Word properties, languages, document length, notable texts, transliterations, Morse code, Soundex, encodings, emotions | -| `MoneyFinance` | Stock data, mortgages & loans, salaries, bonds, derivative valuation, income tax, sales tax | +| `ArtsMedia` | Movies, television, video games, notable texts, periodicals, comics, mythology, music | +| `History` | Historical periods, genealogy, events, countries, military conflicts, world leaders, inventions | +| `WordsLinguistics` | Word properties, languages, transliterations, Morse code, Soundex, encodings | +| `MoneyFinance` | Stock data, mortgages & loans, salaries, bonds, derivative valuation, income and sales tax | | `DatesTimes` | Dates, calendars, time systems | | `FoodNutrition` | Nutritional data and dietary guidelines | -| `Demographics` | Health care, age/sex, gender equality, business, citizenship, crime, education, income & employment, language, race, marriage, mobility, religion, military, HDI | +| `Demographics` | Health care, age/sex, gender, education, income, crime, marriage, religion, military, HDI | ### Everyday Life | Domain file | Coverage | |-------------|----------| | `PersonalHealth` | Physical exercise, food and nutrition, child growth & development | -| `PersonalFinance` | Mortgages & loans, stock data, currency conversion, cost of living, gasoline, food, electricity prices | +| `PersonalFinance` | Mortgages & loans, stock data, currency conversion, cost of living, prices | | `Entertainment` | Music, films, artworks, cultural productions | | `HouseholdScience` | Scientific reasoning applied to everyday physical phenomena | -| `DatesAnniversaries` | Calendar information, celebrations, time zone calculations, time math, anniversaries | -| `Travel` | Weather, cost of living, flight data, gasoline prices, points of interest, travel distances | +| `DatesAnniversaries` | Calendar information, celebrations, time zones, anniversaries | +| `Travel` | Weather, cost of living, flight data, gasoline prices, points of interest | | `HouseholdMath` | Everyday calculations and measurements | | `Programming` | Algorithms, data structures, programming concepts | | `Hobbies` | Recreational activities and personal projects | @@ -81,21 +99,6 @@ The KB is organised into four top-level sections. Each subsection corresponds to --- -## Knowledge Representation - -| Kind | Description | Lean form | -|------|-------------|-----------| -| **Type** | A category or class | `opaque Person : Type` | -| **Subtype** | A type extending another | `opaque Philosopher : Type` + coercion axiom | -| **Instance** | A named individual | `opaque socrates : Person` | -| **Property** | A function from a type to a value | `opaque birthYear : Person → Nat` | -| **Relation** | A binary predicate | `opaque bornIn : Person → Place → Prop` | -| **Fact** | An asserted value or relation | `axiom fact_birthYear_socrates : birthYear socrates = 470` | -| **Rule** | A universally quantified axiom | `axiom ancestors_transitive : ∀ x y z, …` | -| **Definition** | A named computable expression | `def yearsToDouble (r : Float) : Float := …` | - ---- - ## CLI Commands ### Adding knowledge *(all require `in <Domain>`)* @@ -112,21 +115,33 @@ The KB is organised into four top-level sections. Each subsection corresponds to Both `→` (Unicode) and `->` (ASCII) are accepted as type arrows. -### Inspecting knowledge +### Reading knowledge | Command | Description | |---------|-------------| -| `list <types\|instances\|props\|rels\|facts\|rules\|defs\|all> [of <Domain>]` | List declarations, optionally filtered by domain | +| `list <types\|instances\|props\|rels\|facts\|rules\|defs\|all> [of <Domain>]` | List declarations | | `show def <n>` | Print the Lean source of a declaration | -| `domains` | List all domains active this session with declaration counts | -| `domains stats` | Detailed breakdown per domain and kind | +| `get <prop>(<inst>)` | Retrieve a property value — runs `#eval prop inst` | +| `search <text>` | Full-text search across names, Lean source, and domain names | +| `deps <n>` | Show forward dependencies (what `<n>` uses) and reverse dependencies (what uses `<n>`) | +| `eval <expr>` | Evaluate a Lean expression via `#eval` | ### Querying | Command | Description | |---------|-------------| -| `eval <expr>` | Evaluate a computable Lean expression via `#eval` | -| `query <prop>` | Attempt to prove a proposition (Yes / No / Unknown) | +| `query <prop>` | Attempt to prove a proposition. Returns `Status: Yes/No/Unknown`. | +| `query <prop> using <tactic-script>` | Same with a custom tactic. On success, prints the proof term. | + +Default tactic sequence: `first | decide | aesop | simp`. + +Useful custom tactics: +- `decide` — fully decidable propositions +- `native_decide` — faster for large decidable computations +- `omega` — linear arithmetic over `Nat` and `Int` +- `norm_num` — numeric computations +- `ring` — ring equalities +- `simp [myLemma]` — simplification with specific lemmas ### Build and version control @@ -135,8 +150,15 @@ Both `→` (Unicode) and `->` (ASCII) are accepted as type arrows. | `init <dir>` | Create a new KB repository | | `check` | Sync imports and run `lake build` to verify the whole KB | | `commit <message>` | Verify then `git commit` all changes | -| `status` | Show `git status` and session summary | -| `rm <n>` | Remove a declaration (warns about dependents) | +| `status` | Show `git status` and domain summary | +| `rm <n>` | Remove a declaration and its metadata block (warns about dependents) | + +### Domain info + +| Command | Description | +|---------|-------------| +| `domains` | List all loaded domains with declaration counts | +| `domains stats` | Detailed breakdown per domain and kind | --- @@ -148,53 +170,50 @@ Both `→` (Unicode) and `->` (ASCII) are accepted as type arrows. 2. Inspects which domains reference names declared in other domains, and injects the necessary `import` lines. 3. Rewrites `KnowledgeBase.lean` to import all domain files so `lake build` compiles everything. -Add a batch of declarations, then run `check` once at the end rather than after each individual addition. +Add a batch of declarations, then run `check` once — not after each individual addition. + +--- + +## Exit Codes + +Every command exits with `0` on success and `1` on error (duplicate declaration, name not found, build failure, parse failure). This allows agent scripts to detect failure without parsing output: + +```bash +kb add type Person in People && echo "OK" || echo "FAILED" +``` --- ## Example Workflow ```bash -# Initialise -kb init ./myKB -cd myKB +kb init ./myKB && cd myKB -# Base types in the People domain +# Add a batch kb add type Entity in People kb add type Person extends Entity in People kb add type Place extends Entity in People kb add type City extends Place in People - -# Properties and relations kb add prop birthYear : Person -> Nat in People kb add rel bornIn : Person -> Place -> Prop in People - -# Instances and facts kb add instance socrates : Person in People kb add instance athens : City in People kb add fact birthYear(socrates) = 470 in People kb add fact bornIn(socrates, athens) in People -# Verify and commit +# Inspect +kb deps birthYear # forward and reverse dependency graph +kb search athens # full-text search +kb get birthYear(socrates) # → 470 + +# Query +kb query "birthYear socrates = 470" using decide +# Status: Yes +# Proof: ... + +# Verify and persist kb check kb commit "Added Socrates and basic person/place ontology" -# Agent loads only the People domain for a biographical query -kb list all of People +# Next run: all state reloads automatically from People.lean ``` - ---- - -## Query Capabilities - -- **Computational**: `kb eval "yearsToDouble 0.05"` — runs `#eval` on any computable Lean expression. -- **Logical**: `kb query "even (2 + 2)"` — attempts to prove the proposition using `decide`, `aesop`, or `simp`. -- **Selective loading**: `kb list all of Physics` — an agent pulls only the Physics domain into its context for a focused query. - ---- - -## Extensibility - -- Domain files from the planned structure are created on first use — no separate setup step needed. -- Definitions (`kb add def`) become permanent reusable shortcuts stored in Lean files. -- The KB grows incrementally across sessions — each `kb commit` is a checkpoint in Git history. |