Add BNF package documentation and support packages section

README.md

@@ -344,6 +344,10 @@ Example programs are provided in the `examples/` directory:
 
 Each example demonstrates logical inference using propositional logic axioms.
 
+## Support Packages
+
+- **BNF Conversion Library** ([apyds-bnf](https://pypi.org/project/apyds-bnf/), [atsds-bnf](https://www.npmjs.com/package/atsds-bnf)): Bidirectional conversion between DS syntax formats. See [/bnf](/bnf) for details.
+
 ## Development
 
 ### Code Formatting

bnf/README.md

@@ -1,6 +1,193 @@
 # BNF Support Package for DS
 
-This package provides bidirectional conversion between two syntax formats for the DS deductive system:
+A bidirectional conversion library for the DS deductive system, providing seamless translation between two syntax formats:
 
-- **Ds**: The lisp-like syntax currently used in DS
-- **Dsp**: A traditional readable syntax with infix operators
+- **Ds**: The S-expression (lisp-like) syntax used internally by DS
+- **Dsp**: A traditional, human-readable syntax with infix operators
+
+This package enables you to write logical rules in a more natural, mathematical notation and convert them to the DS internal format, or vice versa.
+
+## Features
+
+- **Bidirectional Conversion**: Convert between Ds and Dsp syntax formats
+- **Multi-Language Support**: Available for both Python and JavaScript/TypeScript
+- **Parse**: Convert from readable Dsp syntax to DS internal format
+- **Unparse**: Convert from DS internal format to readable Dsp syntax
+- **Comprehensive Operator Support**: Functions, subscripts, unary and binary operators
+- **ANTLR-Based**: Built on ANTLR 4.13.2 for robust parsing
+
+## Installation
+
+### Python (pip)
+
+```bash
+pip install apyds-bnf
+```
+
+Requires Python 3.10-3.14.
+
+### JavaScript/TypeScript (npm)
+
+```bash
+npm install atsds-bnf
+```
+
+## Quick Start
+
+### Python Example
+
+```python
+from apyds_bnf import parse, unparse
+
+# Parse: Convert from readable Dsp to DS format
+dsp_input = "a, b -> c"
+ds_output = parse(dsp_input)
+print(ds_output)
+# Output:
+# a
+# b
+# ----
+# c
+
+# Unparse: Convert from DS format to readable Dsp
+ds_input = "a\nb\n----\nc"
+dsp_output = unparse(ds_input)
+print(dsp_output)
+# Output: a, b -> c
+```
+
+### JavaScript Example
+
+```javascript
+import { parse, unparse } from "atsds-bnf";
+
+// Parse: Convert from readable Dsp to DS format
+const dsp_input = "a, b -> c";
+const ds_output = parse(dsp_input);
+console.log(ds_output);
+// Output:
+// a
+// b
+// ----
+// c
+
+// Unparse: Convert from DS format to readable Dsp
+const ds_input = "a\nb\n----\nc";
+const dsp_output = unparse(ds_input);
+console.log(dsp_output);
+// Output: a, b -> c
+```
+
+## Syntax Formats
+
+### Ds Format (Internal)
+
+The Ds format uses S-expressions (lisp-like syntax) for representing logical rules:
+
+```
+premise1
+premise2
+----------
+conclusion
+```
+
+For structured terms:
+- Functions: `(function f a b)`
+- Subscripts: `(subscript a i j)`
+- Binary operators: `(binary + a b)`
+- Unary operators: `(unary ~ a)`
+
+### Dsp Format (Human-Readable)
+
+The Dsp format uses traditional mathematical notation:
+
+```
+premise1, premise2 -> conclusion
+```
+
+For structured terms:
+- Functions: `f(a, b)`
+- Subscripts: `a[i, j]`
+- Binary operators: `(a + b)` (parenthesized)
+- Unary operators: `(~ a)` (parenthesized)
+
+### Syntax Comparison Table
+
+| Description | Dsp Format (parse input / unparse output) | Ds Format |
+|-------------|-------------------|-------------------|
+| Simple rule | `a, b -> c` | `a\nb\n----\nc` |
+| Axiom | `a` | `----\na` |
+| Function call | `f(a, b) -> c` | `(function f a b)\n----------------\nc` |
+| Subscript | `a[i, j] -> b` | `(subscript a i j)\n-----------------\nb` |
+| Binary operator | `(a + b) -> c` | `(binary + a b)\n--------------\nc` |
+| Unary operator | `~ a -> b` | `(unary ~ a)\n-----------\nb` |
+| Complex expression | `((a + b) * c), d[i] -> f(g, h)` | `(binary * (binary + a b) c)\n(subscript d i)\n---------------------------\n(function f g h)` |
+
+## Building from Source
+
+### Prerequisites
+
+- Python 3.10-3.14 (for Python package)
+- Node.js (for JavaScript package)
+- Java (for ANTLR parser generation)
+- ANTLR 4.13.2
+
+### Python Package
+
+```bash
+cd bnf
+
+# Install dependencies
+uv sync --extra dev
+
+# Build package
+uv build
+
+# Run tests
+pytest
+
+# Run with coverage
+pytest --cov
+```
+
+### JavaScript Package
+
+```bash
+cd bnf
+
+# Install dependencies
+npm install
+
+# Build package
+npm run build
+
+# Run tests
+npm test
+```
+
+## Grammar Files
+
+The conversion is based on ANTLR grammars:
+
+- **Ds.g4**: Grammar for the Ds format (S-expression syntax)
+- **Dsp.g4**: Grammar for the Dsp format (human-readable syntax)
+
+These grammars are used to generate parsers for both Python and JavaScript.
+
+## License
+
+This project is licensed under the GNU Affero General Public License v3.0 or later (AGPL-3.0-or-later).
+
+## Repository
+
+- **GitHub**: [USTC-KnowledgeComputingLab/ds](https://github.com/USTC-KnowledgeComputingLab/ds) (in `/bnf` directory)
+- **Python Package**: [apyds-bnf](https://pypi.org/project/apyds-bnf/)
+- **npm Package**: [atsds-bnf](https://www.npmjs.com/package/atsds-bnf)
+
+## Author
+
+Hao Zhang <[email protected]>
+
+## Related
+
+This package is a support library for the [DS (Deductive System)](https://github.com/USTC-KnowledgeComputingLab/ds) project. For the main DS library with C++ core and bindings, see the [main repository](https://github.com/USTC-KnowledgeComputingLab/ds).