From be6d0691311ad6bfeb35a17b52ad6580a56c9b65 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 24 Nov 2025 18:08:48 +0000 Subject: [PATCH 1/8] Initial plan From 6ac5f7e3475cd68025ceed38bd0a9f8a06973391 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 24 Nov 2025 18:11:51 +0000 Subject: [PATCH 2/8] Add comprehensive README.md for multi-language deductive system Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com> --- README.md | 303 +++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 302 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 3122eea..271c011 100644 --- a/README.md +++ b/README.md @@ -1,2 +1,303 @@ -# A Deductive System. +# DS - A Deductive System + +A multi-language implementation of a deductive system for logical inference and automated reasoning. This library provides implementations in C++, Python, and TypeScript/JavaScript (via WebAssembly), allowing you to work with logical terms, rules, and perform automated deduction across different platforms. + +## Features + +- **Multi-Language Support**: Use the same deductive system in C++, Python, or TypeScript/JavaScript +- **Logical Terms**: Work with variables, items (constants/functors), and lists +- **Rule-Based Inference**: Define rules and facts, perform logical deduction +- **Unification and Matching**: Unify terms and match rules automatically +- **Search Engine**: Built-in search mechanism for automated theorem proving +- **WebAssembly**: Run deductive reasoning in the browser or Node.js environments +- **Type-Safe**: Strong typing support in TypeScript and Python + +## Installation + +### TypeScript/JavaScript (npm) + +```bash +npm install atsds +``` + +The package includes WebAssembly binaries and TypeScript type definitions. + +### Python (pip) + +```bash +pip install apyds +``` + +Requires Python 3.10-3.13. + +### C++ (from source) + +```bash +git clone https://github.com/USTC-KnowledgeComputingLab/ds.git +cd ds +cmake -B build +cmake --build build +``` + +Include the headers from `include/ds/` in your C++ project. + +## Quick Start + +### TypeScript/JavaScript Example + +```typescript +import { rule_t, search_t, buffer_size } from "atsds"; + +// Set buffer size for internal operations +buffer_size(1000); + +// Create a search engine +const search = new search_t(1000, 10000); + +// Add logical rules (modus ponens) +search.add("(`P -> `Q) `P `Q"); + +// Add axioms +search.add("(`p -> (`q -> `p))"); + +// Add a premise +search.add("(! (! X))"); + +// Define target +const target = new rule_t("X"); + +// Execute search +search.execute((candidate) => { + if (candidate.key() === target.key()) { + console.log("Found:", candidate.toString()); + return true; // Stop search + } + return false; // Continue searching +}); +``` + +### Python Example + +```python +import pyds + +# Set buffer size for internal operations +pyds.buffer_size(1000) + +# Create a search engine +search = pyds.Search(1000, 10000) + +# Add logical rules (modus ponens) +search.add("(`P -> `Q) `P `Q") + +# Add axioms +search.add("(`p -> (`q -> `p))") + +# Add a premise +search.add("(! (! X))") + +# Define target +target = pyds.Rule("X") + +# Execute search +def callback(candidate): + if candidate == target: + print("Found:", candidate) + return True # Stop search + return False # Continue searching + +search.execute(callback) +``` + +### C++ Example + +```cpp +#include +#include + +int main() { + const size_t temp_data_size = 1000; + const size_t buffer_size = 10000; + + ds::search_t search(temp_data_size, buffer_size); + + // Add logical rules + search.add("(`P -> `Q) `P `Q"); + search.add("(`p -> (`q -> `p))"); + search.add("(! (! X))"); + + // Execute search + search.execute([](ds::rule_t* candidate) { + std::cout << "Found rule" << std::endl; + return false; // Continue searching + }); + + return 0; +} +``` + +## Core Concepts + +### Terms + +Terms are the basic building blocks of the deductive system: + +- **Variables**: Prefixed with backtick `` `X ``, e.g., `` `P ``, `` `Q `` +- **Items**: Constants or functors, e.g., `a`, `father`, `!` +- **Lists**: Ordered sequences enclosed in parentheses, e.g., `(a b c)`, `(father john mary)` + +### Rules + +Rules consist of zero or more premises (above the line) and a conclusion (below the line): + +``` +premise1 +premise2 +---------- +conclusion +``` + +A fact is a rule without premises: + +``` +---------- +(parent john mary) +``` + +### Grounding + +Grounding substitutes variables with values using a dictionary: + +```typescript +const a = new term_t("`a"); +const dict = new term_t("((`a b))"); // Substitute `a with b +const result = a.ground(dict); +console.log(result.toString()); // "b" +``` + +### Matching + +Matching unifies two terms or rules to find variable substitutions. + +## API Overview + +### TypeScript/JavaScript + +- `buffer_size(size?: number)`: Get/set buffer size for internal operations +- `string_t`: String wrapper class +- `variable_t`: Logical variable class +- `item_t`: Item (constant/functor) class +- `list_t`: List class +- `term_t`: General term class (variable, item, or list) +- `rule_t`: Logical rule class +- `search_t`: Search engine for inference + +### Python + +- `buffer_size(size: int)`: Set buffer size +- `scoped_buffer_size(size: int)`: Context manager for temporary buffer size +- `String`: String wrapper class +- `Variable`: Logical variable class +- `Item`: Item (constant/functor) class +- `List`: List class +- `Term`: General term class +- `Rule`: Logical rule class +- `Search`: Search engine for inference + +### C++ + +All classes are in the `ds` namespace: + +- `string_t`: String handling +- `variable_t`: Logical variables +- `item_t`: Items (constants/functors) +- `list_t`: Lists +- `term_t`: General terms +- `rule_t`: Logical rules +- `search_t`: Search engine + +See header files in `include/ds/` for detailed API documentation (comments in Chinese). + +## Building from Source + +### Prerequisites + +- C++20 compatible compiler +- CMake 3.15+ +- For TypeScript: Emscripten SDK +- For Python: Python 3.10-3.13, scikit-build-core, pybind11 + +### Build All Components + +```bash +# Clone repository +git clone https://github.com/USTC-KnowledgeComputingLab/ds.git +cd ds + +# Build C++ library +cmake -B build +cmake --build build + +# Build TypeScript/JavaScript (requires Emscripten) +npm install +npm run build + +# Build Python package +pip install -e ".[dev]" +``` + +### Running Tests + +```bash +# TypeScript/JavaScript tests +npm test + +# Python tests +pytest + +# C++ tests (if available) +cd build && ctest +``` + +## Examples + +Example programs are provided in the `examples/` directory: + +- `examples/main.mjs`: TypeScript/JavaScript example +- `examples/main.py`: Python example +- `examples/main.cc`: C++ example + +Each example demonstrates automated theorem proving using propositional logic axioms to derive results. + +## Development + +### Code Formatting + +The project uses code formatting tools for consistency: + +- C++: clang-format (`.clang-format` config provided) +- Python: ruff (configured in `pyproject.toml`) +- TypeScript: Biome (configured in `biome.json`) + +### Pre-commit Hooks + +Pre-commit hooks are configured in `.pre-commit-config.yaml`. + +## License + +This project is licensed under the GNU General Public License v3.0 or later. See [LICENSE.md](LICENSE.md) for details. + +## Repository + +- **GitHub**: [USTC-KnowledgeComputingLab/ds](https://github.com/USTC-KnowledgeComputingLab/ds) +- **npm package**: [atsds](https://www.npmjs.com/package/atsds) +- **PyPI package**: [apyds](https://pypi.org/project/apyds/) + +## Author + +Hao Zhang + +## Contributing + +Contributions are welcome! Please feel free to submit issues or pull requests. From fa5d65b35bb3c2a90871b9e57073841d763a7f7b Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 24 Nov 2025 18:12:56 +0000 Subject: [PATCH 3/8] Clarify Python package import and improve variable syntax formatting Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com> --- README.md | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 271c011..13ca1e0 100644 --- a/README.md +++ b/README.md @@ -28,6 +28,12 @@ The package includes WebAssembly binaries and TypeScript type definitions. pip install apyds ``` +Then import as `pyds`: + +```python +import pyds +``` + Requires Python 3.10-3.13. ### C++ (from source) @@ -142,7 +148,7 @@ int main() { Terms are the basic building blocks of the deductive system: -- **Variables**: Prefixed with backtick `` `X ``, e.g., `` `P ``, `` `Q `` +- **Variables**: Prefixed with backtick, e.g., `` `X``, `` `P``, `` `Q`` - **Items**: Constants or functors, e.g., `a`, `father`, `!` - **Lists**: Ordered sequences enclosed in parentheses, e.g., `(a b c)`, `(father john mary)` From 72d34bf0a13c06f90701452a814a943e608b8252 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 24 Nov 2025 23:26:55 +0000 Subject: [PATCH 4/8] Address feedback: emphasize C++ core, tone down claims, clarify architecture Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com> --- README.md | 30 +++++++++++++++++++++--------- 1 file changed, 21 insertions(+), 9 deletions(-) diff --git a/README.md b/README.md index 13ca1e0..276fb07 100644 --- a/README.md +++ b/README.md @@ -1,21 +1,29 @@ # DS - A Deductive System -A multi-language implementation of a deductive system for logical inference and automated reasoning. This library provides implementations in C++, Python, and TypeScript/JavaScript (via WebAssembly), allowing you to work with logical terms, rules, and perform automated deduction across different platforms. +A deductive system for logical inference, implemented in C++ with bindings for Python and TypeScript/JavaScript. The core library is written in C++, with Python bindings via pybind11 and TypeScript/JavaScript bindings via Emscripten (WebAssembly). + +## Architecture + +- **C++ Core**: The core implementation in `src/` and `include/ds/` provides the fundamental data structures and algorithms +- **Python Bindings**: Built with pybind11, wrapping the C++ core (see `pyds/`) +- **TypeScript/JavaScript Bindings**: Built with Emscripten, compiling C++ to WebAssembly (see `tsds/`) ## Features - **Multi-Language Support**: Use the same deductive system in C++, Python, or TypeScript/JavaScript - **Logical Terms**: Work with variables, items (constants/functors), and lists - **Rule-Based Inference**: Define rules and facts, perform logical deduction -- **Unification and Matching**: Unify terms and match rules automatically -- **Search Engine**: Built-in search mechanism for automated theorem proving -- **WebAssembly**: Run deductive reasoning in the browser or Node.js environments +- **Unification and Matching**: Unify terms and match rules +- **Search Engine**: Built-in search mechanism for iterative inference +- **WebAssembly**: Run inference in the browser or Node.js environments - **Type-Safe**: Strong typing support in TypeScript and Python ## Installation ### TypeScript/JavaScript (npm) +The TypeScript/JavaScript package wraps the C++ core via WebAssembly. + ```bash npm install atsds ``` @@ -24,6 +32,8 @@ The package includes WebAssembly binaries and TypeScript type definitions. ### Python (pip) +The Python package wraps the C++ core via pybind11. + ```bash pip install apyds ``` @@ -36,7 +46,9 @@ import pyds Requires Python 3.10-3.13. -### C++ (from source) +### C++ (Core Library) + +The C++ library is the core implementation. Both Python and TypeScript bindings are built on top of it. ```bash git clone https://github.com/USTC-KnowledgeComputingLab/ds.git @@ -210,7 +222,7 @@ Matching unifies two terms or rules to find variable substitutions. - `Rule`: Logical rule class - `Search`: Search engine for inference -### C++ +### C++ (Core) All classes are in the `ds` namespace: @@ -220,9 +232,9 @@ All classes are in the `ds` namespace: - `list_t`: Lists - `term_t`: General terms - `rule_t`: Logical rules -- `search_t`: Search engine +- `search_t`: Search engine (in ``) -See header files in `include/ds/` for detailed API documentation (comments in Chinese). +See header files in `include/ds/` for detailed API documentation. ## Building from Source @@ -273,7 +285,7 @@ Example programs are provided in the `examples/` directory: - `examples/main.py`: Python example - `examples/main.cc`: C++ example -Each example demonstrates automated theorem proving using propositional logic axioms to derive results. +Each example demonstrates logical inference using propositional logic axioms. ## Development From 8d6cd4b2af2d8bea0024b555c1cf7312a20bb252 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 24 Nov 2025 23:27:45 +0000 Subject: [PATCH 5/8] Improve README intro readability Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com> --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 276fb07..14e73c6 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ # DS - A Deductive System -A deductive system for logical inference, implemented in C++ with bindings for Python and TypeScript/JavaScript. The core library is written in C++, with Python bindings via pybind11 and TypeScript/JavaScript bindings via Emscripten (WebAssembly). +A deductive system for logical inference, implemented in C++. The library provides bindings for Python (via pybind11) and TypeScript/JavaScript (via Emscripten/WebAssembly). ## Architecture From a1a215142e107ab5f63273e99842bd892054ecf3 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 24 Nov 2025 23:41:13 +0000 Subject: [PATCH 6/8] Fix README examples: add all required axioms, remove unnecessary buffer_size, add match example Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com> --- README.md | 104 +++++++++++++++++++++++++++++++++--------------------- 1 file changed, 64 insertions(+), 40 deletions(-) diff --git a/README.md b/README.md index 14e73c6..7ac1092 100644 --- a/README.md +++ b/README.md @@ -64,34 +64,39 @@ Include the headers from `include/ds/` in your C++ project. ### TypeScript/JavaScript Example ```typescript -import { rule_t, search_t, buffer_size } from "atsds"; - -// Set buffer size for internal operations -buffer_size(1000); +import { rule_t, search_t } from "atsds"; // Create a search engine const search = new search_t(1000, 10000); -// Add logical rules (modus ponens) +// Modus ponens: P -> Q, P |- Q search.add("(`P -> `Q) `P `Q"); - -// Add axioms +// Axiom schema 1: p -> (q -> p) search.add("(`p -> (`q -> `p))"); +// Axiom schema 2: (p -> (q -> r)) -> ((p -> q) -> (p -> r)) +search.add("((`p -> (`q -> `r)) -> ((`p -> `q) -> (`p -> `r)))"); +// Axiom schema 3: (!p -> !q) -> (q -> p) +search.add("(((! `p) -> (! `q)) -> (`q -> `p))"); -// Add a premise +// Premise: !!X search.add("(! (! X))"); -// Define target +// Target: X (double negation elimination) const target = new rule_t("X"); -// Execute search -search.execute((candidate) => { - if (candidate.key() === target.key()) { - console.log("Found:", candidate.toString()); - return true; // Stop search - } - return false; // Continue searching -}); +// Execute 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; // Stop search + } + return false; // Continue searching + }); + if (found) break; +} ``` ### Python Example @@ -99,54 +104,64 @@ search.execute((candidate) => { ```python import pyds -# Set buffer size for internal operations -pyds.buffer_size(1000) - # Create a search engine search = pyds.Search(1000, 10000) -# Add logical rules (modus ponens) +# Modus ponens: P -> Q, P |- Q search.add("(`P -> `Q) `P `Q") - -# Add axioms +# Axiom schema 1: p -> (q -> p) search.add("(`p -> (`q -> `p))") +# Axiom schema 2: (p -> (q -> r)) -> ((p -> q) -> (p -> r)) +search.add("((`p -> (`q -> `r)) -> ((`p -> `q) -> (`p -> `r)))") +# Axiom schema 3: (!p -> !q) -> (q -> p) +search.add("(((! `p) -> (! `q)) -> (`q -> `p))") -# Add a premise +# Premise: !!X search.add("(! (! X))") -# Define target +# Target: X (double negation elimination) target = pyds.Rule("X") -# Execute search -def callback(candidate): - if candidate == target: - print("Found:", candidate) - return True # Stop search - return False # Continue searching - -search.execute(callback) +# Execute search until target is found +while True: + found = False + def callback(candidate): + global found + if candidate == target: + print("Found:", candidate) + found = True + return True # Stop search + return False # Continue searching + search.execute(callback) + if found: + break ``` ### C++ Example ```cpp #include +#include #include int main() { - const size_t temp_data_size = 1000; - const size_t buffer_size = 10000; - - ds::search_t search(temp_data_size, buffer_size); + ds::search_t search(1000, 10000); - // Add logical rules + // Modus ponens: P -> Q, P |- Q search.add("(`P -> `Q) `P `Q"); + // Axiom schema 1: p -> (q -> p) search.add("(`p -> (`q -> `p))"); + // Axiom schema 2: (p -> (q -> r)) -> ((p -> q) -> (p -> r)) + search.add("((`p -> (`q -> `r)) -> ((`p -> `q) -> (`p -> `r)))"); + // Axiom schema 3: (!p -> !q) -> (q -> p) + search.add("(((! `p) -> (! `q)) -> (`q -> `p))"); + + // Premise: !!X search.add("(! (! X))"); // Execute search search.execute([](ds::rule_t* candidate) { - std::cout << "Found rule" << std::endl; + // Process each derived rule return false; // Continue searching }); @@ -195,7 +210,16 @@ console.log(result.toString()); // "b" ### Matching -Matching unifies two terms or rules to find variable substitutions. +Matching unifies the first premise of a rule with a fact to produce a new rule. For example, applying modus ponens to double negation elimination: + +```typescript +// Modus ponens rule: (p -> q), p |- q +const mp = new rule_t("(`p -> `q)\n`p\n`q\n"); +// Double negation elimination axiom: !!x -> x +const pq = new rule_t("((! (! `x)) -> `x)"); +// Match produces: !!x |- x +console.log(mp.match(pq).toString()); // "(! (! `x))\n----------\n`x\n" +``` ## API Overview From 5c4ffed9e2f8b48bf097a2bf739493ce7296bf20 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 24 Nov 2025 23:53:08 +0000 Subject: [PATCH 7/8] Add target checking and termination to C++ example in README Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com> --- README.md | 25 +++++++++++++++++++------ 1 file changed, 19 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index 7ac1092..dc9de46 100644 --- a/README.md +++ b/README.md @@ -140,9 +140,10 @@ while True: ### C++ Example ```cpp +#include #include #include -#include +#include int main() { ds::search_t search(1000, 10000); @@ -159,11 +160,23 @@ int main() { // Premise: !!X search.add("(! (! X))"); - // Execute search - search.execute([](ds::rule_t* candidate) { - // Process each derived rule - return false; // Continue searching - }); + // Target: X (double negation elimination) + auto target = ds::text_to_rule("X", 1000); + + // Execute search until target is found + 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: %s", ds::rule_to_text(candidate, 1000).get()); + found = true; + return true; // Stop search + } + return false; // Continue searching + }); + if (found) break; + } return 0; } From f90b44d751426da8b2a78447463adad32dd0a1f6 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 25 Nov 2025 00:00:32 +0000 Subject: [PATCH 8/8] Add missing cstdio include to C++ example in README Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com> --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index dc9de46..73b4615 100644 --- a/README.md +++ b/README.md @@ -140,6 +140,7 @@ while True: ### C++ Example ```cpp +#include #include #include #include