diff options
| author | Petri Hienonen <petri.hienonen@gmail.com> | 2026-02-15 15:59:37 +0200 |
|---|---|---|
| committer | Petri Hienonen <petri.hienonen@gmail.com> | 2026-02-15 15:59:37 +0200 |
| commit | 8ebc1b0ebb7244f73ace1407ccb672a151c3a052 (patch) | |
| tree | 1f3d3e58eee3e6ed21d49b3b70d40d3086e0cbd3 /AGENT.md | |
| parent | 5f787f25cc5caf4ba388734d96ff9205739504cb (diff) | |
| download | kb-8ebc1b0ebb7244f73ace1407ccb672a151c3a052.tar.zst | |
Update
Diffstat (limited to '')
| -rw-r--r-- | AGENT.md | 165 |
1 files changed, 165 insertions, 0 deletions
diff --git a/AGENT.md b/AGENT.md new file mode 100644 index 0000000..f7bc695 --- /dev/null +++ b/AGENT.md @@ -0,0 +1,165 @@ +# Lean-Based Knowledge Base Agent Instructions + +You are an AI agent with access to a persistent, formally verified knowledge base built in Lean 4. The knowledge base is stored as a Git repository of Lean files. You interact with it using the `kb` command-line tool. Every addition is type-checked by Lean's kernel, ensuring logical consistency. + +--- + +## 1. Key Design Principle: Explicit Domains + +Every declaration belongs to a **domain** that you name explicitly using `in <Domain>`. Each domain is stored as a separate `<Domain>.lean` file in the KB root. There is no automatic classification. + +**Choose domains based on what you want an agent to load together.** For example: +- `Ontology` — base types (`Entity`, `Person`, `Place`, …) that everything else depends on +- `People` — instances, properties, and facts about specific people +- `Geography` — instances and facts about places +- `Finance` — financial formulas and data +- `Physics` — physical constants and laws + +An agent loading only `People` facts into its context window would run: `kb list all of People`. + +--- + +## 2. Session Start Protocol + +```bash +# Orient yourself: see what domains and declarations exist +kb list all +kb domains stats + +# Recall declarations in a specific domain +kb list all of Ontology +kb list all of People +``` + +--- + +## 3. Adding Knowledge + +Every `add` command requires `in <Domain>` at the end. + +| Command | Purpose | Example | +|---------|---------|---------| +| `kb add type <n> [extends <Parent>] in <D>` | Declare a type | `kb add type Person extends Entity in Ontology` | +| `kb add instance <n> : <Type> in <D>` | Declare an individual | `kb add instance socrates : Person in People` | +| `kb add prop <n> : <DomType> -> <Range> in <D>` | Declare a property | `kb add prop birthYear : Person -> Nat in People` | +| `kb add rel <n> : <D1> -> <D2> -> Prop in <D>` | Declare a relation | `kb add rel bornIn : Person -> Place -> Prop in People` | +| `kb add fact <fact> in <D>` | Assert a fact | `kb add fact birthYear(socrates) = 470 in People` | +| `kb add rule <n> : <statement> in <D>` | Add a logical rule | `kb add rule ancestors_transitive : ∀ x y z, parentOf x y → parentOf y z → ancestorOf x z in Ontology` | +| `kb add def <n> <params> : <Type> := <body> in <D>` | Define a shortcut | `kb add def yearsToDouble (r : Float) : Float := Float.log 2 / r in Finance` | + +### Notes + +- Both `→` (Unicode) and `->` (ASCII) are accepted as type arrows. +- Fact syntax: `prop(inst) = value` or `rel(inst1, inst2)`. +- Domains are created automatically when first used — no `create domain` step needed. +- Put base types in a shared domain (e.g. `Ontology`) that other domains can depend on. + +--- + +## 4. Querying the Knowledge Base + +| Command | Description | Example | +|---------|-------------|---------| +| `kb eval <expr>` | Compute a value | `kb eval "yearsToDouble 0.05"` | +| `kb query <prop>` | Ask if a proposition is provable | `kb query "even (2 + 2)"` | +| `kb list all of <Domain>` | List all declarations in a domain | `kb list all of People` | + +### Query semantics + +- `kb eval` runs Lean's `#eval` on the expression. +- `kb query` attempts to prove the proposition using `decide`, `aesop`, or `simp`. Returns `Yes`, `No`, or `Unknown`. + +--- + +## 5. Checking Consistency and Committing + +Add all facts first, then verify and commit in one step: + +```bash +kb check +kb commit "Added Socrates and basic ontology" +``` + +`kb check` rewrites `KnowledgeBase.lean` to import every domain file on disk, injects cross-domain imports where needed, then runs `lake build`. `kb commit` does the same before committing to Git. + +**Do not check after each individual fact.** Batch your additions, then check once. + +--- + +## 6. Example Workflow + +```bash +# Base ontology (shared types everything else depends on) +kb add type Entity in Ontology +kb add type Person extends Entity in Ontology +kb add type Place extends Entity in Ontology +kb add type City extends Place in Ontology + +# Domain-specific properties and relations +kb add prop birthYear : Person -> Nat in People +kb add rel bornIn : Person -> Place -> Prop in People + +# Instances +kb add instance socrates : Person in People +kb add instance athens : City in People + +# Facts +kb add fact birthYear(socrates) = 470 in People +kb add fact bornIn(socrates, athens) in People + +# Verify and commit everything at once +kb check +kb commit "Added Socrates and basic person/place ontology" +``` + +--- + +## 7. Removing Declarations + +```bash +kb rm <name> +``` + +The tool warns if other declarations depend on the one being removed. Remove dependents first. + +--- + +## 8. Reusable Definitions + +```bash +kb add def yearsToDouble (r : Float) : Float := Float.log 2 / r in Finance +kb eval "yearsToDouble 0.05" +kb list defs +kb show def yearsToDouble +``` + +--- + +## 9. Best Practices + +- **Put base types in one domain** (e.g. `Ontology`) so all other domains can import it cleanly. +- **Group by agent-loadable context**: a domain should contain what an agent needs for a specific task. +- **Use meaningful domain names**: `People`, `Physics`, `Finance`, `Geography` — not `Domain1`. +- **Prefer `def` over `axiom` for computed facts** — definitions are safer and evaluable. +- **Run `kb check` once after a batch** of additions, not after each one. +- **Commit with descriptive messages** so the KB history is readable. + +--- + +## 10. Session End Protocol + +```bash +kb commit "Session summary: what was added" +kb list all # Review final state +kb domains stats # Confirm counts are as expected +``` + +--- + +## 11. Need Help? + +```bash +kb help +``` + +Lean error messages are forwarded directly. A typical error like `unknown identifier 'Person'` means the type was declared in another domain file that hasn't been imported yet — run `kb check` to sync imports, or check that you added the base type before its dependents. |