Enhance documentation with detailed examples and explanations

README.md

@@ -336,9 +336,16 @@ Pre-commit hooks are configured in `.pre-commit-config.yaml`.
 
 This project is licensed under the GNU General Public License v3.0 or later. See [LICENSE.md](LICENSE.md) for details.
 
+## Documentation
+
+For comprehensive documentation including tutorials, API reference, and examples, visit:
+
+- **[DS Documentation](https://ustc-knowledgecomputinglab.github.io/ds)**
+
 ## Repository
 
 - **GitHub**: [USTC-KnowledgeComputingLab/ds](https://github.com/USTC-KnowledgeComputingLab/ds)
+- **Documentation**: [ustc-knowledgecomputinglab.github.io/ds](https://ustc-knowledgecomputinglab.github.io/ds)
 - **npm package**: [atsds](https://www.npmjs.com/package/atsds)
 - **PyPI package**: [apyds](https://pypi.org/project/apyds/)
 

docs/api/cpp.md

@@ -550,3 +550,73 @@ std::unique_ptr<char> rule_to_text(rule_t* rule, length_t length);
 - `length`: Maximum size for the resulting text
 
 **Returns:** A unique_ptr to the text, or nullptr if length exceeded.
+
+---
+
+## Complete Example
+
+Here's a complete example demonstrating the C++ API:
+
+```cpp
+#include <ds/ds.hh>
+#include <ds/search.hh>
+#include <ds/utility.hh>
+#include <cstring>
+#include <iostream>
+
+int main() {
+    const int buffer_size = 1000;
+
+    // Create terms using utility functions
+    auto term = ds::text_to_term("(f `x `y)", buffer_size);
+
+    std::cout << "Term: " << ds::term_to_text(term.get(), buffer_size).get() << std::endl;
+
+    // Work with rules
+    auto fact = ds::text_to_rule("(parent john mary)", buffer_size);
+    auto rule = ds::text_to_rule("(father `X `Y)\n----------\n(parent `X `Y)\n", buffer_size);
+
+    std::cout << "\nFact:\n" << ds::rule_to_text(fact.get(), buffer_size).get();
+    std::cout << "Rule premises: " << rule->premises_count() << std::endl;
+    std::cout << "Rule conclusion: " << ds::term_to_text(rule->conclusion(), buffer_size).get() << std::endl;
+
+    // Search engine
+    ds::search_t search(1000, 10000);
+
+    // Add rules and facts
+    search.add("p q");  // p implies q
+    search.add("q r");  // q implies r
+    search.add("p");    // fact: p
+
+    std::cout << "\nRunning inference:" << std::endl;
+
+    // Execute search
+    auto target = ds::text_to_rule("r", buffer_size);
+    bool found = false;
+
+    while (!found) {
+        auto count = search.execute([&](ds::rule_t* candidate) {
+            std::cout << "  Derived: " << ds::rule_to_text(candidate, buffer_size).get();
+
+            // Check if this is our target
+            if (candidate->data_size() == target->data_size() &&
+                memcmp(candidate->head(), target->head(), candidate->data_size()) == 0) {
+                found = true;
+                return true;  // Stop
+            }
+            return false;  // Continue
+        });
+
+        if (count == 0) {
+            std::cout << "  (no more inferences)" << std::endl;
+            break;
+        }
+    }
+
+    if (found) {
+        std::cout << "Target found!" << std::endl;
+    }
+
+    return 0;
+}
+```

docs/api/python.md

@@ -452,3 +452,63 @@ def callback(candidate):
 
 search.execute(callback)
 ```
+
+---
+
+## Complete Example
+
+Here's a complete example demonstrating most of the API:
+
+```python
+import apyds
+
+# Configure buffer size for operations
+apyds.buffer_size(2048)
+
+# Create terms
+var = apyds.Variable("`X")
+item = apyds.Item("hello")
+lst = apyds.List("(a b c)")
+term = apyds.Term("(f `x `y)")
+
+print(f"Variable: {var}, name: {var.name}")
+print(f"Item: {item}, name: {item.name}")
+print(f"List: {lst}, length: {len(lst)}")
+print(f"Term: {term}, type: {type(term.term)}")
+
+# Work with rules
+fact = apyds.Rule("(parent john mary)")
+rule = apyds.Rule("(father `X `Y)\n----------\n(parent `X `Y)\n")
+
+print(f"\nFact: {fact}")
+print(f"Rule premises: {len(rule)}, conclusion: {rule.conclusion}")
+
+# Grounding
+term_a = apyds.Term("`a")
+dictionary = apyds.Term("((`a hello))")
+grounded = term_a // dictionary
+print(f"\nGrounding `a with ((` hello)): {grounded}")
+
+# Matching
+mp = apyds.Rule("(`p -> `q)\n`p\n`q\n")
+axiom = apyds.Rule("((A) -> B)")
+matched = mp @ axiom
+print(f"\nMatching modus ponens with (A -> B):\n{matched}")
+
+# Search engine
+search = apyds.Search(1000, 10000)
+search.add("p q")  # p implies q
+search.add("q r")  # q implies r
+search.add("p")    # fact: p
+
+print("\nRunning inference:")
+for i in range(3):
+    count = search.execute(lambda r: print(f"  Derived: {r}") or False)
+    if count == 0:
+        break
+
+# Using context manager for buffer size
+with apyds.scoped_buffer_size(4096):
+    big_term = apyds.Term("(a b c d e f g h i j)")
+    print(f"\nBig term: {big_term}")
+```

docs/api/typescript.md

@@ -447,3 +447,79 @@ search.execute((candidate) => {
     return false;  // Continue searching
 });
 ```
+
+---
+
+## Complete Example
+
+Here's a complete example demonstrating most of the TypeScript API:
+
+```typescript
+import { 
+    buffer_size, 
+    string_t, 
+    variable_t, 
+    item_t, 
+    list_t, 
+    term_t, 
+    rule_t, 
+    search_t 
+} from "atsds";
+
+// Configure buffer size
+buffer_size(2048);
+
+// Create terms
+const varX = new variable_t("`X");
+const item = new item_t("hello");
+const lst = new list_t("(a b c)");
+const term = new term_t("(f `x `y)");
+
+console.log(`Variable: ${varX.toString()}, name: ${varX.name().toString()}`);
+console.log(`Item: ${item.toString()}, name: ${item.name().toString()}`);
+console.log(`List: ${lst.toString()}, length: ${lst.length()}`);
+console.log(`Term: ${term.toString()}`);
+
+// Work with rules
+const fact = new rule_t("(parent john mary)");
+const rule = new rule_t("(father `X `Y)\n----------\n(parent `X `Y)\n");
+
+console.log(`\nFact: ${fact.toString()}`);
+console.log(`Rule premises: ${rule.length()}, conclusion: ${rule.conclusion().toString()}`);
+
+// Grounding
+const termA = new term_t("`a");
+const dictionary = new term_t("((`a hello))");
+const grounded = termA.ground(dictionary);
+if (grounded) {
+    console.log(`\nGrounding \`a with ((\`a hello)): ${grounded.toString()}`);
+}
+
+// Matching
+const mp = new rule_t("(`p -> `q)\n`p\n`q\n");
+const axiom = new rule_t("((A) -> B)");
+const matched = mp.match(axiom);
+if (matched) {
+    console.log(`\nMatching modus ponens with (A -> B):\n${matched.toString()}`);
+}
+
+// Search engine
+const search = new search_t(1000, 10000);
+search.add("p q");  // p implies q
+search.add("q r");  // q implies r
+search.add("p");    // fact: p
+
+console.log("\nRunning inference:");
+for (let i = 0; i < 3; i++) {
+    const count = search.execute((r) => {
+        console.log(`  Derived: ${r.toString()}`);
+        return false;
+    });
+    if (count === 0) break;
+}
+
+// Copying and comparison
+const rule1 = new rule_t("(a b c)");
+const rule2 = rule1.copy();
+console.log(`\nRule comparison: ${rule1.key() === rule2.key()}`);  // true
+```

docs/concepts/rules.md

@@ -11,7 +11,7 @@ A rule consists of:
 
 ### Text Representation
 
-Rules are written with premises and conclusion separated by dashes:
+Rules are written with premises and conclusion separated by dashes (at least four dashes):
 
 ```
 premise1
@@ -33,6 +33,31 @@ Or explicitly:
 (parent john mary)
 ```
 
+!!! info "Rule Format Details"
+    - Premises are separated by newlines
+    - The separator line must contain at least 4 dashes (`----`) between premises and conclusion
+    - Whitespace around premises and conclusion is trimmed
+    - A rule without an premises is a fact
+
+### Compact Rule Format
+
+For rules with multiple premises, you can use space-separated terms on a single line:
+
+```
+(`P -> `Q) `P `Q
+```
+
+This is equivalent to:
+
+```
+(`P -> `Q)
+`P
+----------
+`Q
+```
+
+The last term is the conclusion, and all preceding terms are premises.
+
 ### Examples
 
 **Modus Ponens** (if P implies Q and P is true, then Q is true):

docs/concepts/search.md

@@ -9,6 +9,16 @@ The search engine:
 1. Maintains a collection of rules and facts
 2. Iteratively applies rules to generate new facts
 3. Notifies you of each new inference via a callback
+4. Automatically prevents duplicate inferences
+
+!!! info "How It Works"
+    The search engine uses a forward-chaining inference approach:
+
+    1. When you call `execute()`, the engine tries to match the first premise of each rule with existing facts
+    2. When a match is found, variables in the rule are substituted and a new rule (with one fewer premise) is created
+    3. If the new rule has no premises, it becomes a new fact
+    4. The callback is invoked for each newly derived rule
+    5. Duplicate rules are automatically filtered out
 
 ## Creating a Search Engine
 
@@ -21,7 +31,7 @@ The search engine:
     search = apyds.Search()
 
     # Create with custom sizes
-    search = apyds.Search(limit_size=2000, buffer_size=20000)
+    search = apyds.Search(limit_size=1000, buffer_size=10000)
     ```
 
 === "TypeScript"
@@ -33,7 +43,7 @@ The search engine:
     const search = new search_t();
 
     // Create with custom sizes
-    const search2 = new search_t(2000, 20000);
+    const search2 = new search_t(1000, 10000);
     ```
 
 === "C++"
@@ -47,8 +57,8 @@ The search engine:
 
 ### Parameters
 
-- **limit_size**: Maximum size (in bytes) for each stored rule/fact (default: 1000)
-- **buffer_size**: Size of the internal buffer for intermediate operations (default: 10000)
+- **limit_size**: Maximum size (in bytes) for each stored rule/fact (default: 1000). Rules or facts larger than this are rejected.
+- **buffer_size**: Size of the internal buffer for intermediate operations (default: 10000). Increase this if you work with complex rules.
 
 ## Adding Rules and Facts
 
@@ -66,11 +76,6 @@ Use the `add()` method to add rules and facts to the knowledge base.
 
     # Add a rule with premises
     search.add("(father `X `Y)\n----------\n(parent `X `Y)\n")
-
-    # Add multiple facts and rules
-    search.add("(father john mary)")
-    search.add("(father john bob)")
-    search.add("(mother mary alice)")
     ```
 
 === "TypeScript"
@@ -298,6 +303,7 @@ Clears all rules and facts:
 2. **Limit Size**: Restricts maximum rule/fact complexity - too small may reject valid rules
 3. **Iterative Execution**: Call `execute()` in a loop to continue inference until convergence
 4. **Early Termination**: Return `true` from callback to stop as soon as target is found
+5. **Deduplication**: The engine automatically deduplicates facts, avoiding redundant computation
 
 ## See Also