From c1ec58ed8933244c67ecad290aaf8473925b6b3b Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Wed, 26 Nov 2025 10:23:15 +0000 Subject: [PATCH 01/23] Initial plan From 1a640809c636e36a197c50e3244be6561d38d536 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Wed, 26 Nov 2025 10:32:17 +0000 Subject: [PATCH 02/23] Enhance documentation with detailed examples and explanations Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com> --- README.md | 7 + docs/api/cpp.md | 124 +++++++++++++++++ docs/api/python.md | 70 ++++++++++ docs/api/typescript.md | 94 +++++++++++++ docs/concepts/rules.md | 193 ++++++++++++++++++++++++++- docs/concepts/search.md | 193 ++++++++++++++++++++++++++- docs/concepts/terms.md | 153 ++++++++++++++++++++- docs/examples/basic.md | 168 +++++++++++++++++++++++ docs/getting-started/installation.md | 97 +++++++++++++- docs/getting-started/quickstart.md | 70 ++++++++++ docs/index.md | 84 ++++++++++-- 11 files changed, 1236 insertions(+), 17 deletions(-) diff --git a/README.md b/README.md index 05edfca..0c8d000 100644 --- a/README.md +++ b/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/) diff --git a/docs/api/cpp.md b/docs/api/cpp.md index eadc7be..7ffbfe5 100644 --- a/docs/api/cpp.md +++ b/docs/api/cpp.md @@ -550,3 +550,127 @@ std::unique_ptr 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 +#include +#include +#include +#include + +int main() { + const int buffer_size = 1000; + + // Create terms using utility functions + auto var = ds::text_to_variable("`X", buffer_size); + auto item = ds::text_to_item("hello", buffer_size); + auto list = ds::text_to_list("(a b c)", buffer_size); + auto term = ds::text_to_term("(f `x `y)", buffer_size); + + std::cout << "Variable: " << ds::variable_to_text(var.get(), buffer_size).get() << std::endl; + std::cout << "Item: " << ds::item_to_text(item.get(), buffer_size).get() << std::endl; + std::cout << "List: " << ds::list_to_text(list.get(), buffer_size).get() << std::endl; + 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; +} +``` + +## Memory Management Notes + +The C++ API uses a unique memory model: + +1. **Buffer-based allocation**: Most operations require pre-allocated buffers +2. **Utility functions**: `text_to_*` functions allocate and return `unique_ptr` +3. **In-place operations**: Methods like `ground()` and `match()` write to provided buffers + +### Example: Manual Buffer Management + +```cpp +#include +#include + +void manual_grounding() { + // Source term + auto term = ds::text_to_term("`a", 1000); + + // Dictionary + auto dict = ds::text_to_term("((`a hello))", 1000); + + // Allocate result buffer + std::byte buffer[1000]; + auto result = reinterpret_cast(buffer); + + // Ground the term into the buffer + result->ground(term.get(), dict.get(), nullptr, buffer + 1000); + + // Print result + printf("Result: %s\n", ds::term_to_text(result, 1000).get()); +} +``` + +### Example: Rule Comparison + +```cpp +#include +#include +#include + +bool rules_equal(ds::rule_t* r1, ds::rule_t* r2) { + if (r1->data_size() != r2->data_size()) { + return false; + } + return memcmp(r1->head(), r2->head(), r1->data_size()) == 0; +} +``` diff --git a/docs/api/python.md b/docs/api/python.md index ef49eb2..7b1e18a 100644 --- a/docs/api/python.md +++ b/docs/api/python.md @@ -452,3 +452,73 @@ 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}") +``` + +## Operator Reference + +| Operator | Operation | Example | +|----------|-----------|---------| +| `//` | Grounding (Term/Rule) | `term // dictionary` | +| `@` | Matching (Rule) | `rule @ fact` | +| `==` | Equality comparison | `rule1 == rule2` | +| `len()` | Length (List/Rule) | `len(list)` | +| `[]` | Indexing (List/Rule) | `list[0]`, `rule[0]` | diff --git a/docs/api/typescript.md b/docs/api/typescript.md index e1a74ff..5eeb012 100644 --- a/docs/api/typescript.md +++ b/docs/api/typescript.md @@ -447,3 +447,97 @@ 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 +``` + +## Method Reference + +| Method | Class | Description | +|--------|-------|-------------| +| `toString()` | All | Convert to string representation | +| `data()` | All | Get binary data as Buffer | +| `size()` | All | Get data size in bytes | +| `copy()` | All | Create a deep copy | +| `key()` | All | Get key for equality comparison | +| `name()` | variable_t, item_t | Get the name | +| `length()` | list_t, rule_t | Get number of elements/premises | +| `getitem(i)` | list_t, rule_t | Get element/premise by index | +| `conclusion()` | rule_t | Get the rule's conclusion | +| `ground(dict)` | term_t, rule_t | Substitute variables | +| `rename(spec)` | term_t, rule_t | Rename variables | +| `match(fact)` | rule_t | Match rule with a fact | +| `term()` | term_t | Get underlying variable/item/list | diff --git a/docs/concepts/rules.md b/docs/concepts/rules.md index a6e837d..68f2e45 100644 --- a/docs/concepts/rules.md +++ b/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,32 @@ Or explicitly: (parent john mary) ``` +!!! info "Rule Format Details" + - Premises are separated by newlines + - The separator line must contain at least 4 dashes (`----`) + - The conclusion comes after the separator + - Whitespace around premises and conclusion is trimmed + - A rule without an explicit separator is treated as a fact (no premises) + +### 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): @@ -52,6 +78,23 @@ Or explicitly: (parent `X `Y) ``` +**Transitivity of Implication** (if P implies Q and Q implies R, then P implies R): + +``` +(`P -> `Q) +(`Q -> `R) +---------- +(`P -> `R) +``` + +**Propositional Logic Axiom Schemas**: + +| Axiom | Formula | Description | +|-------|---------|-------------| +| Axiom 1 | `(`p -> (`q -> `p))` | If P then (Q implies P) | +| Axiom 2 | `((`p -> (`q -> `r)) -> ((`p -> `q) -> (`p -> `r)))` | Distribution of implication | +| Axiom 3 | `(((! `p) -> (! `q)) -> (`q -> `p))` | Contraposition | + ## Creating Rules === "TypeScript" @@ -361,6 +404,154 @@ Rules can be compared for equality. Two rules are equal if they have the same bi } ``` +## Practical Examples + +### Building a Knowledge Base + +Here's how to build a simple family relationship knowledge base: + +=== "Python" + + ```python + import apyds + + # Define rules for family relationships + rules = [ + # If X is father of Y, then X is parent of Y + apyds.Rule("(father `X `Y)\n----------\n(parent `X `Y)\n"), + # If X is mother of Y, then X is parent of Y + apyds.Rule("(mother `X `Y)\n----------\n(parent `X `Y)\n"), + # If X is parent of Y and Y is parent of Z, then X is grandparent of Z + apyds.Rule("(parent `X `Y)\n(parent `Y `Z)\n----------\n(grandparent `X `Z)\n"), + ] + + # Define facts + facts = [ + apyds.Rule("(father john mary)"), + apyds.Rule("(mother mary alice)"), + ] + + for rule in rules: + print(f"Rule with {len(rule)} premise(s):") + print(rule) + ``` + +=== "TypeScript" + + ```typescript + import { rule_t } from "atsds"; + + // Define rules for family relationships + const rules = [ + new rule_t("(father `X `Y)\n----------\n(parent `X `Y)\n"), + new rule_t("(mother `X `Y)\n----------\n(parent `X `Y)\n"), + new rule_t("(parent `X `Y)\n(parent `Y `Z)\n----------\n(grandparent `X `Z)\n"), + ]; + + // Define facts + const facts = [ + new rule_t("(father john mary)"), + new rule_t("(mother mary alice)"), + ]; + + for (const rule of rules) { + console.log(`Rule with ${rule.length()} premise(s):`); + console.log(rule.toString()); + } + ``` + +### Implementing Inference Steps Manually + +You can manually apply matching to simulate inference: + +=== "Python" + + ```python + import apyds + + # Modus ponens: (P -> Q), P |- Q + modus_ponens = apyds.Rule("(`P -> `Q)\n`P\n----------\n`Q\n") + print(f"Modus Ponens:\n{modus_ponens}") + + # An implication fact: A -> B + implication = apyds.Rule("(A -> B)") + print(f"Implication:\n{implication}") + + # Match to get: A |- B + step1 = modus_ponens @ implication + print(f"After matching implication:\n{step1}") + + # Now we need fact A to complete the inference + fact_a = apyds.Rule("A") + print(f"Fact A:\n{fact_a}") + + # Match again to derive B + step2 = step1 @ fact_a + print(f"Final result (B):\n{step2}") + ``` + +=== "TypeScript" + + ```typescript + import { rule_t } from "atsds"; + + // Modus ponens: (P -> Q), P |- Q + const modusPonens = new rule_t("(`P -> `Q)\n`P\n----------\n`Q\n"); + console.log("Modus Ponens:", modusPonens.toString()); + + // An implication fact: A -> B + const implication = new rule_t("(A -> B)"); + console.log("Implication:", implication.toString()); + + // Match to get: A |- B + const step1 = modusPonens.match(implication); + if (step1) { + console.log("After matching implication:", step1.toString()); + + // Match with fact A to derive B + const factA = new rule_t("A"); + const step2 = step1.match(factA); + if (step2) { + console.log("Final result (B):", step2.toString()); + } + } + ``` + +### Working with Rule Premises + +You can iterate over a rule's premises: + +=== "Python" + + ```python + import apyds + + # A rule with multiple premises + rule = apyds.Rule("(p -> q)\n(q -> r)\n----------\n(p -> r)\n") + + print(f"Number of premises: {len(rule)}") + print(f"Conclusion: {rule.conclusion}") + + # Iterate over premises + for i in range(len(rule)): + print(f"Premise {i}: {rule[i]}") + ``` + +=== "TypeScript" + + ```typescript + import { rule_t } from "atsds"; + + const rule = new rule_t("(p -> q)\n(q -> r)\n----------\n(p -> r)\n"); + + console.log(`Number of premises: ${rule.length()}`); + console.log(`Conclusion: ${rule.conclusion().toString()}`); + + for (let i = 0; i < rule.length(); i++) { + console.log(`Premise ${i}: ${rule.getitem(i).toString()}`); + } + ``` + ## See Also - [Terms](terms.md) - Building blocks for rules diff --git a/docs/concepts/search.md b/docs/concepts/search.md index 75fd747..a2342b3 100644 --- a/docs/concepts/search.md +++ b/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 fact + 5. Duplicate facts are automatically filtered out ## Creating a Search Engine @@ -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 @@ -298,6 +308,185 @@ 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 + +!!! tip "Choosing Buffer Sizes" + - For simple propositional logic: `limit_size=1000`, `buffer_size=10000` + - For complex first-order logic: `limit_size=2000`, `buffer_size=50000` + - If you get truncated results, increase the buffer sizes + +## Practical Examples + +### Complete Double Negation Elimination + +This example demonstrates proving that from `!!X` we can derive `X`: + +=== "Python" + + ```python + import apyds + + search = apyds.Search(1000, 10000) + + # Modus ponens: P -> Q, P |- Q + search.add("(`P -> `Q) `P `Q") + + # Propositional logic axioms + search.add("(`p -> (`q -> `p))") # Axiom 1 + search.add("((`p -> (`q -> `r)) -> ((`p -> `q) -> (`p -> `r)))") # Axiom 2 + search.add("(((! `p) -> (! `q)) -> (`q -> `p))") # Axiom 3 + + # Premise: !!X (double negation of X) + search.add("(! (! X))") + + # Target: X + target = apyds.Rule("X") + + # Run until we find X + iterations = 0 + while True: + found = False + def callback(candidate): + nonlocal found + if candidate == target: + print(f"✓ Found target after {iterations + 1} iteration(s)!") + print(f" Result: {candidate}") + found = True + return True # Stop + return False # Continue + + count = search.execute(callback) + iterations += 1 + + if found: + break + if count == 0: + print("No more inferences possible") + break + ``` + +=== "TypeScript" + + ```typescript + import { rule_t, search_t } from "atsds"; + + const search = new search_t(1000, 10000); + + // Modus ponens: P -> Q, P |- Q + search.add("(`P -> `Q) `P `Q"); + + // Propositional logic axioms + search.add("(`p -> (`q -> `p))"); + search.add("((`p -> (`q -> `r)) -> ((`p -> `q) -> (`p -> `r)))"); + search.add("(((! `p) -> (! `q)) -> (`q -> `p))"); + + // Premise: !!X + search.add("(! (! X))"); + + const target = new rule_t("X"); + + let iterations = 0; + while (true) { + let found = false; + const count = search.execute((candidate) => { + if (candidate.key() === target.key()) { + console.log(`✓ Found target after ${iterations + 1} iteration(s)!`); + console.log(` Result: ${candidate.toString()}`); + found = true; + return true; + } + return false; + }); + iterations++; + + if (found) break; + if (count === 0) { + console.log("No more inferences possible"); + break; + } + } + ``` + +### Family Relationship Inference + +This example shows how to derive family relationships: + +=== "Python" + + ```python + import apyds + + search = apyds.Search(1000, 10000) + + # Rules: father/mother implies parent + search.add("(father `X `Y) (parent `X `Y)") + search.add("(mother `X `Y) (parent `X `Y)") + + # Rule: parent of parent is grandparent + search.add("(parent `X `Y) (parent `Y `Z) (grandparent `X `Z)") + + # Facts + search.add("(father john mary)") + search.add("(mother mary alice)") + + # Collect all derived facts + derived = [] + + # Run multiple iterations + for i in range(5): + def callback(fact): + derived.append(str(fact)) + return False # Continue + + count = search.execute(callback) + if count == 0: + break + + print("Derived facts:") + for fact in derived: + print(f" {fact}") + ``` + +### Monitoring Inference Progress + +Track what the search engine is discovering: + +=== "Python" + + ```python + import apyds + + search = apyds.Search(1000, 10000) + + # Simple inference rules + search.add("p q") # p implies q + search.add("q r") # q implies r + search.add("p") # fact: p + + iteration = 0 + total_facts = 0 + + while True: + iteration += 1 + print(f"Iteration {iteration}:") + + new_facts = [] + def callback(fact): + new_facts.append(str(fact).strip()) + return False + + count = search.execute(callback) + total_facts += count + + for fact in new_facts: + print(f" + {fact}") + + if count == 0: + print(f" (no new facts)") + break + + print(f"\nTotal facts derived: {total_facts}") + ``` ## See Also diff --git a/docs/concepts/terms.md b/docs/concepts/terms.md index 89a9547..ac1dab1 100644 --- a/docs/concepts/terms.md +++ b/docs/concepts/terms.md @@ -17,7 +17,10 @@ Variables are placeholders that can be unified with other terms during inference `Q ``` -Variables are used in rules to represent any term that can match during unification. +Variables are used in rules to represent any term that can match during unification. During the inference process, variables can be bound to specific terms through unification. + +!!! tip "Variable Naming" + Variable names can contain any characters except whitespace and parentheses. By convention, single uppercase letters like `` `X``, `` `P``, `` `Q`` are often used for simple logic, while descriptive names like `` `person`` or `` `result`` improve readability in complex rules. ### Items @@ -35,6 +38,10 @@ Items can represent: - **Constants**: Atomic values like `john`, `mary`, `42` - **Functors**: Symbols that combine other terms, like `father`, `->`, `!` +- **Operators**: Special symbols used in logical expressions, like `->` for implication or `!` for negation + +!!! note "Item Characters" + Items can contain any characters except whitespace and parentheses. Special symbols like `->`, `!`, `<-`, `&&`, `||` are commonly used as logical operators. ### Lists @@ -47,7 +54,19 @@ Lists are ordered sequences of terms enclosed in parentheses. They can contain a (! (! X)) ``` -Lists are the primary way to build complex structures in the deductive system. +Lists are the primary way to build complex structures in the deductive system. They can represent: + +- **Relations**: `(father john mary)` - "John is the father of Mary" +- **Logical expressions**: `(-> P Q)` - "P implies Q" +- **Nested structures**: `(! (! X))` - "not not X" (double negation) +- **Data collections**: `(1 2 3 4 5)` - a list of numbers + +!!! example "List Nesting" + Lists can be nested to any depth: + ``` + ((a b) (c d) (e f)) + (if (> `x 0) (positive `x) (non-positive `x)) + ``` ## Creating Terms @@ -288,6 +307,136 @@ Operations like grounding and renaming require buffer space for intermediate res # Buffer size restored to previous value ``` +## Practical Examples + +### Building Logical Expressions + +Here's how to build common logical expressions using terms: + +=== "Python" + + ```python + import apyds + + # Implication: P -> Q + implication = apyds.Term("(-> P Q)") + print(f"Implication: {implication}") + + # Negation: !P + negation = apyds.Term("(! P)") + print(f"Negation: {negation}") + + # Double negation: !!X + double_neg = apyds.Term("(! (! X))") + print(f"Double negation: {double_neg}") + + # Complex formula: (P -> Q) -> ((Q -> R) -> (P -> R)) + # This is the hypothetical syllogism + syllogism = apyds.Term("(-> (-> P Q) (-> (-> Q R) (-> P R)))") + print(f"Hypothetical syllogism: {syllogism}") + ``` + +=== "TypeScript" + + ```typescript + import { term_t } from "atsds"; + + // Implication: P -> Q + const implication = new term_t("(-> P Q)"); + console.log(`Implication: ${implication.toString()}`); + + // Negation: !P + const negation = new term_t("(! P)"); + console.log(`Negation: ${negation.toString()}`); + + // Double negation: !!X + const doubleNeg = new term_t("(! (! X))"); + console.log(`Double negation: ${doubleNeg.toString()}`); + ``` + +### Working with Scoped Grounding + +Scoped grounding allows you to control which variables get substituted based on a scope prefix: + +=== "Python" + + ```python + import apyds + + # Create a term with a variable + term = apyds.Term("`a") + + # Create a dictionary with scoped entries + # Format: ((scope1 scope2 variable value) ...) + dictionary = apyds.Term("((x y `a `b) (y x `b `c))") + + # Ground with scope "x" - follows the chain: `a -> `b -> `c + result = term.ground(dictionary, "x") + print(f"Result with scope 'x': {result}") # `c + ``` + +=== "TypeScript" + + ```typescript + import { term_t } from "atsds"; + + const term = new term_t("`a"); + const dictionary = new term_t("((x y `a `b) (y x `b `c))"); + + const result = term.ground(dictionary, "x"); + if (result !== null) { + console.log(`Result with scope 'x': ${result.toString()}`); // `c + } + ``` + +### Checking Term Types + +You can inspect the type of a term and access its underlying value: + +=== "Python" + + ```python + import apyds + + # Create terms of different types + var_term = apyds.Term("`variable") + item_term = apyds.Term("constant") + list_term = apyds.Term("(a b c)") + + # Check types using the term property + print(f"Variable type: {type(var_term.term)}") # Variable + print(f"Item type: {type(item_term.term)}") # Item + print(f"List type: {type(list_term.term)}") # List + + # Access type-specific properties + if isinstance(var_term.term, apyds.Variable): + print(f"Variable name: {var_term.term.name}") + + if isinstance(list_term.term, apyds.List): + print(f"List length: {len(list_term.term)}") + for i in range(len(list_term.term)): + print(f" Element {i}: {list_term.term[i]}") + ``` + +=== "TypeScript" + + ```typescript + import { term_t, variable_t, item_t, list_t } from "atsds"; + + const varTerm = new term_t("`variable"); + const itemTerm = new term_t("constant"); + const listTerm = new term_t("(a b c)"); + + // Access underlying types + const inner = listTerm.term(); + if (inner instanceof list_t) { + console.log(`List length: ${inner.length()}`); + for (let i = 0; i < inner.length(); i++) { + console.log(` Element ${i}: ${inner.getitem(i).toString()}`); + } + } + ``` + ## See Also - [Rules](rules.md) - How to create and work with inference rules diff --git a/docs/examples/basic.md b/docs/examples/basic.md index 64960d5..de6b2d1 100644 --- a/docs/examples/basic.md +++ b/docs/examples/basic.md @@ -13,6 +13,15 @@ The classic example demonstrates double negation elimination using propositional Given the premise ¬¬X (double negation of X), we can derive X. +### How It Works + +1. The search engine starts with the axiom schemas and modus ponens rule +2. Each `execute()` call applies matching to derive new facts +3. The engine iteratively discovers intermediate results +4. Eventually, `X` is derived from `!!X` + +The proof involves several steps of applying axioms and modus ponens, demonstrating how a simple set of rules can derive complex theorems. + === "Python" ```python @@ -164,3 +173,162 @@ cmake -B build cmake --build build ./build/main ``` + +## Additional Examples + +### Simple Chained Inference + +This example shows simple chained reasoning: + +=== "Python" + + ```python + import apyds + + search = apyds.Search(1000, 10000) + + # Define chain: a -> b, b -> c, c -> d + search.add("a b") # a implies b + search.add("b c") # b implies c + search.add("c d") # c implies d + search.add("a") # fact: a is true + + # Run until we derive d + target = apyds.Rule("d") + + for iteration in range(10): + found = False + def callback(candidate): + nonlocal found + print(f" Derived: {candidate}") + if candidate == target: + found = True + return True + return False + + print(f"Iteration {iteration + 1}:") + count = search.execute(callback) + + if count == 0: + print(" (no new facts)") + if found: + print("Target found!") + break + ``` + +=== "TypeScript" + + ```typescript + import { rule_t, search_t } from "atsds"; + + const search = new search_t(1000, 10000); + + // Define chain: a -> b, b -> c, c -> d + search.add("a b"); + search.add("b c"); + search.add("c d"); + search.add("a"); + + const target = new rule_t("d"); + + for (let iteration = 0; iteration < 10; iteration++) { + let found = false; + console.log(`Iteration ${iteration + 1}:`); + + const count = search.execute((candidate) => { + console.log(` Derived: ${candidate.toString()}`); + if (candidate.key() === target.key()) { + found = true; + return true; + } + return false; + }); + + if (count === 0) { + console.log(" (no new facts)"); + } + if (found) { + console.log("Target found!"); + break; + } + } + ``` + +### Working with Variables + +This example demonstrates how variables unify during inference: + +=== "Python" + + ```python + import apyds + + search = apyds.Search(1000, 10000) + + # Rule: (double `x) implies (`x `x`) + # When we have (double a), we derive (a a) + search.add("(double `x) (`x `x)") + + # Facts + search.add("(double hello)") + search.add("(double 42)") + + # See what gets derived + search.execute(lambda r: print(f"Derived: {r}") or False) + # Output: (hello hello), (42 42) + ``` + +=== "TypeScript" + + ```typescript + import { search_t } from "atsds"; + + const search = new search_t(1000, 10000); + + // Rule: (double `x) implies (`x `x`) + search.add("(double `x) (`x `x)"); + + // Facts + search.add("(double hello)"); + search.add("(double 42)"); + + // See what gets derived + search.execute((r) => { + console.log(`Derived: ${r.toString()}`); + return false; + }); + ``` + +### Collecting All Results + +Sometimes you want to collect all derived facts: + +=== "Python" + + ```python + import apyds + + search = apyds.Search(1000, 10000) + + # Setup + search.add("(parent `X `Y) (ancestor `X `Y)") + search.add("(ancestor `X `Y) (parent `Y `Z) (ancestor `X `Z)") + search.add("(parent a b)") + search.add("(parent b c)") + search.add("(parent c d)") + + # Collect all derived facts + all_facts = [] + + for _ in range(10): + def collect(fact): + all_facts.append(str(fact).strip()) + return False + + if search.execute(collect) == 0: + break + + print("All derived facts:") + for fact in sorted(set(all_facts)): + print(f" {fact}") + ``` diff --git a/docs/getting-started/installation.md b/docs/getting-started/installation.md index 3e59aac..2cf5ee9 100644 --- a/docs/getting-started/installation.md +++ b/docs/getting-started/installation.md @@ -20,6 +20,19 @@ The package includes: - Node.js 20+ or a modern browser with WebAssembly support +### Browser Usage + +The package works in browsers that support WebAssembly: + +```html + +``` + ## Python The Python package `apyds` wraps the C++ core via pybind11. @@ -31,7 +44,17 @@ pip install apyds ### Requirements - Python 3.10-3.14 -- Pre-built wheels are available for common platforms +- Pre-built wheels are available for common platforms (Linux, macOS, Windows) + +### Virtual Environment (Recommended) + +It's recommended to use a virtual environment: + +```bash +python -m venv venv +source venv/bin/activate # On Windows: venv\Scripts\activate +pip install apyds +``` ### Development Installation @@ -49,7 +72,7 @@ The C++ library is the core implementation. Both Python and TypeScript bindings ### Prerequisites -- C++20 compatible compiler +- C++20 compatible compiler (GCC 10+, Clang 10+, MSVC 2019+) - CMake 3.30+ ### Building from Source @@ -72,6 +95,15 @@ Include the headers from `include/ds/` in your C++ project: Link against the `ds` static library produced by the build. +### CMake Integration + +You can add DS as a subdirectory in your CMake project: + +```cmake +add_subdirectory(path/to/ds) +target_link_libraries(your_target PRIVATE ds) +``` + ## Building All Components To build all language bindings from source: @@ -99,6 +131,30 @@ cmake -B build cmake --build build ``` +## Running Tests + +After installation, you can verify everything works by running the tests: + +### Python Tests + +```bash +pip install pytest +pytest +``` + +### TypeScript/JavaScript Tests + +```bash +npm test +``` + +### C++ Tests + +```bash +cd build +ctest +``` + ## Verifying Installation === "TypeScript" @@ -108,17 +164,24 @@ cmake --build build const term = new term_t("(hello world)"); console.log(term.toString()); + // Output: (hello world) ``` === "Python" ```python import apyds - print(apyds.__version__) + print(f"Version: {apyds.__version__}") # Create a simple term term = apyds.Term("(hello world)") - print(term) + print(term) # (hello world) + + # Try a simple inference + search = apyds.Search() + search.add("p q") + search.add("p") + search.execute(lambda r: print(f"Derived: {r}") or False) ``` === "C++" @@ -134,3 +197,29 @@ cmake --build build return 0; } ``` + +## Troubleshooting + +### Python: "Could not find pybind11" + +Install pybind11 first: + +```bash +pip install pybind11 +``` + +### TypeScript: WebAssembly errors + +Ensure your environment supports WebAssembly. In Node.js, this should work out of the box. In browsers, ensure you're using HTTPS or localhost. + +### C++: CMake version too old + +Update CMake to version 3.30 or newer: + +```bash +# On Ubuntu/Debian +pip install cmake --upgrade + +# On macOS +brew install cmake +``` diff --git a/docs/getting-started/quickstart.md b/docs/getting-started/quickstart.md index 3f612c1..b0577f1 100644 --- a/docs/getting-started/quickstart.md +++ b/docs/getting-started/quickstart.md @@ -240,6 +240,76 @@ The search engine performs logical inference by matching rules with facts. } ``` +## Understanding the Output + +When you run the search examples, the engine will: + +1. Start with your axioms and premises +2. Apply modus ponens to derive new conclusions +3. Continue until it finds the target (X) + +The double negation elimination proof typically requires several iterations as the engine: + +- Applies axiom schemas to create new implications +- Uses modus ponens to derive intermediate results +- Eventually proves `X` from `!!X` + +## Common Patterns + +### Pattern 1: Simple Rule Application + +```python +import apyds + +search = apyds.Search() +search.add("p q") # Rule: p implies q +search.add("p") # Fact: p is true + +# After execute(), we can derive q +search.execute(lambda r: print(f"Derived: {r}") or False) +``` + +### Pattern 2: Chained Inference + +```python +import apyds + +search = apyds.Search() +search.add("a b") # a implies b +search.add("b c") # b implies c +search.add("a") # fact: a + +# Run multiple iterations to get all derivations +for _ in range(3): + search.execute(lambda r: print(f"Derived: {r}") or False) +# Output: b, then c +``` + +### Pattern 3: Target Search + +```python +import apyds + +search = apyds.Search() +# ... add rules and facts ... + +target = apyds.Rule("my_goal") + +while True: + found = False + def check(candidate): + nonlocal found + if candidate == target: + found = True + return True # Stop search + return False + + search.execute(check) + if found: + print("Goal achieved!") + break +``` + ## Next Steps - Learn more about [Terms](../concepts/terms.md) diff --git a/docs/index.md b/docs/index.md index 9895fc4..e6c1aa4 100644 --- a/docs/index.md +++ b/docs/index.md @@ -18,6 +18,22 @@ A deductive system for logical inference, implemented in C++. The library provid - **[Quick Start](getting-started/quickstart.md)** - Get up and running in minutes - **[Core Concepts](concepts/terms.md)** - Learn about terms, rules, and inference - **[API Reference](api/python.md)** - Complete API documentation +- **[Examples](examples/basic.md)** - Working code examples + +## What is a Deductive System? + +A deductive system is a formal framework for deriving conclusions from a set of premises using inference rules. DS implements a forward-chaining inference engine that: + +1. **Stores knowledge** as rules and facts +2. **Applies rules** to derive new facts through pattern matching +3. **Continues inference** until a target is found or no new facts can be derived + +This is useful for: + +- **Theorem proving**: Automatically proving logical statements +- **Knowledge reasoning**: Deriving implicit facts from explicit knowledge +- **Expert systems**: Building rule-based decision systems +- **Educational tools**: Learning about formal logic and inference ## Supported Languages @@ -31,7 +47,20 @@ A deductive system for logical inference, implemented in C++. The library provid search.add("(! (! X))") # Premise: !!X target = apyds.Rule("X") - # ... execute search + + # Search until target is found + while True: + found = False + def callback(candidate): + nonlocal found + if candidate == target: + print(f"Found: {candidate}") + found = True + return True + return False + search.execute(callback) + if found: + break ``` === "TypeScript" @@ -44,7 +73,20 @@ A deductive system for logical inference, implemented in C++. The library provid search.add("(! (! X))"); // Premise: !!X const target = new rule_t("X"); - // ... execute search + + // Search until target is found + while (true) { + let found = false; + search.execute((candidate) => { + if (candidate.key() === target.key()) { + console.log(`Found: ${candidate.toString()}`); + found = true; + return true; + } + return false; + }); + if (found) break; + } ``` === "C++" @@ -52,14 +94,40 @@ A deductive system for logical inference, implemented in C++. The library provid ```cpp #include #include + #include + #include + + int main() { + ds::search_t search(1000, 10000); + search.add("(`P -> `Q) `P `Q"); // Modus ponens + search.add("(! (! X))"); // Premise: !!X + + auto target = ds::text_to_rule("X", 1000); + + while (true) { + bool found = false; + search.execute([&](ds::rule_t* candidate) { + if (candidate->data_size() == target->data_size() && + memcmp(candidate->head(), target->head(), + candidate->data_size()) == 0) { + printf("Found!\n"); + found = true; + return true; + } + return false; + }); + if (found) break; + } + return 0; + } + ``` - ds::search_t search(1000, 10000); - search.add("(`P -> `Q) `P `Q"); // Modus ponens - search.add("(! (! X))"); // Premise: !!X +## Getting Started - auto target = ds::text_to_rule("X", 1000); - // ... execute search - ``` +1. **Install** the package for your language: [Installation Guide](getting-started/installation.md) +2. **Learn** the basics: [Quick Start](getting-started/quickstart.md) +3. **Understand** the concepts: [Terms](concepts/terms.md), [Rules](concepts/rules.md), [Search](concepts/search.md) +4. **Explore** examples: [Basic Examples](examples/basic.md), [Sudoku Solver](examples/sudoku.md) ## License From 6f64e5601435679ba6406f277f340ec105db4599 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Wed, 26 Nov 2025 10:34:09 +0000 Subject: [PATCH 03/23] Address code review feedback for documentation Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com> --- docs/concepts/terms.md | 10 +++++++--- docs/getting-started/installation.md | 5 ++++- docs/index.md | 1 + 3 files changed, 12 insertions(+), 4 deletions(-) diff --git a/docs/concepts/terms.md b/docs/concepts/terms.md index ac1dab1..2f75cbc 100644 --- a/docs/concepts/terms.md +++ b/docs/concepts/terms.md @@ -356,7 +356,9 @@ Here's how to build common logical expressions using terms: ### Working with Scoped Grounding -Scoped grounding allows you to control which variables get substituted based on a scope prefix: +Scoped grounding is an advanced feature that allows controlling variable substitution based on scope prefixes. The dictionary entries contain scope information that determines when a substitution applies. This is useful when working with rules that have variables from different contexts that need to be kept separate. + +The dictionary format for scoped grounding is `((scope_from scope_to variable value) ...)`, where the substitution only happens when transitioning from `scope_from` to `scope_to`. === "Python" @@ -367,10 +369,12 @@ Scoped grounding allows you to control which variables get substituted based on term = apyds.Term("`a") # Create a dictionary with scoped entries - # Format: ((scope1 scope2 variable value) ...) + # Format: ((scope_from scope_to variable value) ...) + # Entry 1: from scope "x" to "y", substitute `a with `b + # Entry 2: from scope "y" to "x", substitute `b with `c dictionary = apyds.Term("((x y `a `b) (y x `b `c))") - # Ground with scope "x" - follows the chain: `a -> `b -> `c + # Ground with scope "x" - the grounding follows the chain: `a -> `b -> `c result = term.ground(dictionary, "x") print(f"Result with scope 'x': {result}") # `c ``` diff --git a/docs/getting-started/installation.md b/docs/getting-started/installation.md index 2cf5ee9..d8bb732 100644 --- a/docs/getting-started/installation.md +++ b/docs/getting-started/installation.md @@ -218,7 +218,10 @@ Update CMake to version 3.30 or newer: ```bash # On Ubuntu/Debian -pip install cmake --upgrade +sudo apt-get update && sudo apt-get install cmake + +# Or download from official website: +# https://cmake.org/download/ # On macOS brew install cmake diff --git a/docs/index.md b/docs/index.md index e6c1aa4..4b12aae 100644 --- a/docs/index.md +++ b/docs/index.md @@ -107,6 +107,7 @@ This is useful for: while (true) { bool found = false; search.execute([&](ds::rule_t* candidate) { + // Compare binary representations for equality if (candidate->data_size() == target->data_size() && memcmp(candidate->head(), target->head(), candidate->data_size()) == 0) { From 9a9a5c8e1bc31f4cfc6877af605dc5072ede0a23 Mon Sep 17 00:00:00 2001 From: Hao Zhang Date: Wed, 26 Nov 2025 18:42:16 +0800 Subject: [PATCH 04/23] Remove a unproper paragraph. --- docs/index.md | 110 -------------------------------------------------- 1 file changed, 110 deletions(-) diff --git a/docs/index.md b/docs/index.md index 4b12aae..a980199 100644 --- a/docs/index.md +++ b/docs/index.md @@ -20,116 +20,6 @@ A deductive system for logical inference, implemented in C++. The library provid - **[API Reference](api/python.md)** - Complete API documentation - **[Examples](examples/basic.md)** - Working code examples -## What is a Deductive System? - -A deductive system is a formal framework for deriving conclusions from a set of premises using inference rules. DS implements a forward-chaining inference engine that: - -1. **Stores knowledge** as rules and facts -2. **Applies rules** to derive new facts through pattern matching -3. **Continues inference** until a target is found or no new facts can be derived - -This is useful for: - -- **Theorem proving**: Automatically proving logical statements -- **Knowledge reasoning**: Deriving implicit facts from explicit knowledge -- **Expert systems**: Building rule-based decision systems -- **Educational tools**: Learning about formal logic and inference - -## Supported Languages - -=== "Python" - - ```python - import apyds - - search = apyds.Search(1000, 10000) - search.add("(`P -> `Q) `P `Q") # Modus ponens - search.add("(! (! X))") # Premise: !!X - - target = apyds.Rule("X") - - # Search until target is found - while True: - found = False - def callback(candidate): - nonlocal found - if candidate == target: - print(f"Found: {candidate}") - found = True - return True - return False - search.execute(callback) - if found: - break - ``` - -=== "TypeScript" - - ```typescript - import { rule_t, search_t } from "atsds"; - - const search = new search_t(1000, 10000); - search.add("(`P -> `Q) `P `Q"); // Modus ponens - search.add("(! (! X))"); // Premise: !!X - - const target = new rule_t("X"); - - // Search until target is found - while (true) { - let found = false; - search.execute((candidate) => { - if (candidate.key() === target.key()) { - console.log(`Found: ${candidate.toString()}`); - found = true; - return true; - } - return false; - }); - if (found) break; - } - ``` - -=== "C++" - - ```cpp - #include - #include - #include - #include - - int main() { - ds::search_t search(1000, 10000); - search.add("(`P -> `Q) `P `Q"); // Modus ponens - search.add("(! (! X))"); // Premise: !!X - - auto target = ds::text_to_rule("X", 1000); - - while (true) { - bool found = false; - search.execute([&](ds::rule_t* candidate) { - // Compare binary representations for equality - if (candidate->data_size() == target->data_size() && - memcmp(candidate->head(), target->head(), - candidate->data_size()) == 0) { - printf("Found!\n"); - found = true; - return true; - } - return false; - }); - if (found) break; - } - return 0; - } - ``` - -## Getting Started - -1. **Install** the package for your language: [Installation Guide](getting-started/installation.md) -2. **Learn** the basics: [Quick Start](getting-started/quickstart.md) -3. **Understand** the concepts: [Terms](concepts/terms.md), [Rules](concepts/rules.md), [Search](concepts/search.md) -4. **Explore** examples: [Basic Examples](examples/basic.md), [Sudoku Solver](examples/sudoku.md) - ## License This project is licensed under the GNU General Public License v3.0 or later. From f5d81425229aced0133c6b207443559aae5cf1bf Mon Sep 17 00:00:00 2001 From: Hao Zhang Date: Wed, 26 Nov 2025 18:45:20 +0800 Subject: [PATCH 05/23] Fix an example. --- docs/getting-started/installation.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/getting-started/installation.md b/docs/getting-started/installation.md index d8bb732..3b6679c 100644 --- a/docs/getting-started/installation.md +++ b/docs/getting-started/installation.md @@ -26,7 +26,7 @@ The package works in browsers that support WebAssembly: ```html