@@ -3,9 +3,9 @@ SPDX-License-Identifier: MIT AND Palimpsest-0.6
33SPDX-FileCopyrightText: 2024-2025 ECHIDNA Project Contributors
44-->
55
6- # ECHIDNA
6+ = ECHIDNA
77
8- ** E ** xtensible ** C ** ognitive ** H ** ybrid ** I ** ntelligence for ** D ** eductive ** N ** eural ** A * * ssistance
8+ *E* xtensible *C* ognitive *H* ybrid *I* ntelligence for *D* eductive *N* eural *A *ssistance
99
1010[](LICENSES/MIT.txt)
1111[](LICENSES/Palimpsest-0.6.txt)
@@ -14,93 +14,93 @@ SPDX-FileCopyrightText: 2024-2025 ECHIDNA Project Contributors
1414
1515A neurosymbolic theorem proving platform that transforms Quill (Agda-only neural solver) into a universal multi-prover system supporting 12 theorem provers with aspect tagging, OpenCyc integration, and DeepProbLog probabilistic logic.
1616
17- ## Features
17+ == Features
1818
19- - ** 12 Theorem Prover Support* * : Universal backend supporting Agda, Coq/Rocq, Lean, Isabelle, Z3, CVC5, Metamath, HOL Light, Mizar, PVS, ACL2, and HOL4
20- - ** Neurosymbolic AI* * : Neural proof synthesis combined with symbolic verification
21- - ** Aspect Tagging* * : Intelligent proof categorization and analysis
22- - ** OpenCyc Integration* * : Common sense reasoning with ontological knowledge
23- - ** DeepProbLog* * : Probabilistic logic programming for uncertain reasoning
24- - ** 4-Language Architecture* * : Rust (core), Julia (ML), ReScript (UI), Mercury/Logtalk (logic)
19+ - *12 Theorem Prover Support*: Universal backend supporting Agda, Coq/Rocq, Lean, Isabelle, Z3, CVC5, Metamath, HOL Light, Mizar, PVS, ACL2, and HOL4
20+ - *Neurosymbolic AI*: Neural proof synthesis combined with symbolic verification
21+ - *Aspect Tagging*: Intelligent proof categorization and analysis
22+ - *OpenCyc Integration*: Common sense reasoning with ontological knowledge
23+ - *DeepProbLog*: Probabilistic logic programming for uncertain reasoning
24+ - *4-Language Architecture*: Rust (core), Julia (ML), ReScript (UI), Mercury/Logtalk (logic)
2525
26- ## Quick Start
26+ == Quick Start
2727
28- ### Prerequisites
28+ === Prerequisites
2929
30- - ** Rust* * 1.75 or later
31- - ** Julia* * 1.10 or later
32- - ** Deno* * 1.40 or later (for ReScript)
33- - ** Podman* * (NOT Docker)
34- - ** Just* * command runner
30+ - *Rust* 1.75 or later
31+ - *Julia* 1.10 or later
32+ - *Deno* 1.40 or later (for ReScript)
33+ - *Podman* (NOT Docker)
34+ - *Just* command runner
3535
36- ### Installation
36+ === Installation
3737
3838```bash
39- # Clone the repository
39+ = Clone the repository
4040git clone https://gitlab.com/non-initiate/rhodinised/quill.git
4141cd quill
4242
43- # Build the project
43+ = Build the project
4444just build
4545
46- # Run tests
46+ = Run tests
4747just test
4848
49- # Run ECHIDNA
49+ = Run ECHIDNA
5050just run
5151```
5252
53- ### Using Podman Container
53+ === Using Podman Container
5454
5555```bash
56- # Build container
56+ = Build container
5757podman build -f Containerfile -t echidna:latest .
5858
59- # Run container
59+ = Run container
6060podman run -it echidna:latest
6161```
6262
63- ## Architecture
63+ == Architecture
6464
65- ### Prover Tiers
65+ === Prover Tiers
6666
67- ** Tier 1* * (6 provers - Months 2-4):
67+ *Tier 1* (6 provers - Months 2-4):
6868- Agda - Dependent type theory
6969- Coq/Rocq - Interactive theorem prover
7070- Lean - Functional programming and proving
7171- Isabelle - Higher-order logic
7272- Z3 - SMT solver
7373- CVC5 - SMT solver
7474
75- ** Tier 2* * (3 provers - Months 5-7):
75+ *Tier 2* (3 provers - Months 5-7):
7676- Metamath - Plain text verifier (easiest, start here!)
7777- HOL Light - Classical higher-order logic
7878- Mizar - Mathematical vernacular
7979
80- ** Tier 3* * (2 provers - Months 8-10):
80+ *Tier 3* (2 provers - Months 8-10):
8181- PVS - Specification and verification
8282- ACL2 - Applicative Common Lisp
8383
84- ** Tier 4* * (1 prover - Months 11-12):
84+ *Tier 4* (1 prover - Months 11-12):
8585- HOL4 - Higher-order logic
8686
87- ### Technology Stack
87+ === Technology Stack
8888
89- - ** Rust* * : Core logic, FFI, WASM compilation
90- - ** Julia* * : Machine learning components (NO Python allowed!)
91- - ** ReScript + Deno* * : User interface
92- - ** Mercury/Logtalk* * : Optional logic reservoir
89+ - *Rust*: Core logic, FFI, WASM compilation
90+ - *Julia*: Machine learning components (NO Python allowed!)
91+ - *ReScript + Deno*: User interface
92+ - *Mercury/Logtalk*: Optional logic reservoir
9393
94- ### Key Components
94+ === Key Components
9595
96- - ** ` echidna_provers.rs ` * * : Complete Rust trait system (600+ lines)
97- - ** Aspect Tagging System* * : Proof classification and analysis
98- - ** Neural Solver* * : Integration from original Quill project
99- - ** Universal Prover Abstraction* * : Unified interface for all 12 provers
96+ - *`echidna_provers.rs`*: Complete Rust trait system (600+ lines)
97+ - *Aspect Tagging System*: Proof classification and analysis
98+ - *Neural Solver*: Integration from original Quill project
99+ - *Universal Prover Abstraction*: Unified interface for all 12 provers
100100
101- ## Usage
101+ == Usage
102102
103- ### Basic Theorem Proving
103+ === Basic Theorem Proving
104104
105105```rust
106106use echidna::prover::{Prover, AgdaProver};
@@ -110,7 +110,7 @@ let result = prover.prove("∀ (n : ℕ) → n + 0 ≡ n")?;
110110println!("Proof: {}", result);
111111```
112112
113- ### Using Multiple Provers
113+ === Using Multiple Provers
114114
115115```rust
116116use echidna::prover::{ProverBackend, lean, coq, z3};
@@ -125,69 +125,69 @@ for backend in backends {
125125}
126126```
127127
128- ### Neural Proof Synthesis
128+ === Neural Proof Synthesis
129129
130130```julia
131131using ECHIDNA
132132
133- # Train neural model
133+ = Train neural model
134134model = train_proof_synthesizer(training_data)
135135
136- # Generate proof candidates
136+ = Generate proof candidates
137137candidates = synthesize_proofs(model, theorem)
138138
139- # Verify with symbolic prover
139+ = Verify with symbolic prover
140140for candidate in candidates
141141 if verify_proof(candidate)
142142 return candidate
143143 end
144144end
145145```
146146
147- ## Development
147+ == Development
148148
149- ### Building from Source
149+ === Building from Source
150150
151151```bash
152- # Install dependencies
152+ = Install dependencies
153153just deps
154154
155- # Build all components
155+ = Build all components
156156just build
157157
158- # Build specific component
158+ = Build specific component
159159just build-rust
160160just build-julia
161161just build-rescript
162162```
163163
164- ### Running Tests
164+ === Running Tests
165165
166166```bash
167- # Run all tests
167+ = Run all tests
168168just test
169169
170- # Run specific language tests
170+ = Run specific language tests
171171just test-rust
172172just test-julia
173173
174- # Run integration tests
174+ = Run integration tests
175175just test-integration
176176```
177177
178- ### Quality Checks
178+ === Quality Checks
179179
180180```bash
181- # Run all quality checks
181+ = Run all quality checks
182182just check
183183
184- # Individual checks
184+ = Individual checks
185185just lint # REUSE, rustfmt, clippy
186186just security # Trivy, cargo-audit
187187just coverage # Test coverage
188188```
189189
190- ## Documentation
190+ == Documentation
191191
192192- [Contributing Guidelines](CONTRIBUTING.md)
193193- [Code of Conduct](CODE_OF_CONDUCT.md)
@@ -196,49 +196,49 @@ just coverage # Test coverage
196196- [API Documentation](docs/)
197197- [Prover Backend Guides](docs/)
198198
199- ## Roadmap
199+ == Roadmap
200200
201- ### 12-Month Implementation Plan
201+ === 12-Month Implementation Plan
202202
203- ** Months 1-2* * : Foundation
203+ *Months 1-2*: Foundation
204204- Deploy RSR/CCCP compliance templates
205205- Migrate Python code to Julia
206206- Complete Tier 1 infrastructure
207207
208- ** Months 2-4* * : Tier 1 Provers
208+ *Months 2-4*: Tier 1 Provers
209209- Coq/Rocq implementation
210210- Lean implementation
211211- Isabelle implementation
212212- Z3 and CVC5 integration
213213
214- ** Months 5-7* * : Tier 2 Provers
214+ *Months 5-7*: Tier 2 Provers
215215- Metamath (start here - easiest!)
216216- HOL Light
217217- Mizar
218218
219- ** Months 8-10* * : Tier 3 Provers
219+ *Months 8-10*: Tier 3 Provers
220220- PVS
221221- ACL2
222222
223- ** Months 11-12* * : Tier 4 and Polish
223+ *Months 11-12*: Tier 4 and Polish
224224- HOL4 implementation
225225- Performance optimization
226226- Documentation completion
227227
228- ## Contributing
228+ == Contributing
229229
230230We welcome contributions! Please see [CONTRIBUTING.md](CONTRIBUTING.md) for guidelines.
231231
232- ### Critical Constraints
232+ === Critical Constraints
233233
234- - ❌ ** NO PYTHON* * - Use Julia for all ML code
235- - ✅ ** RSR/CCCP Compliance* * - Follow Rhodium Standard Repository guidelines
236- - ✅ ** Justfile PRIMARY* * - Use Just, not Make
237- - ✅ ** GitLab-first* * - This is a GitLab project
238- - ✅ ** Podman not Docker* * - Always use Podman
239- - ✅ ** Dual Licensing* * - MIT + Palimpsest v0.6
234+ - ❌ *NO PYTHON* - Use Julia for all ML code
235+ - ✅ *RSR/CCCP Compliance* - Follow Rhodium Standard Repository guidelines
236+ - ✅ *Justfile PRIMARY* - Use Just, not Make
237+ - ✅ *GitLab-first* - This is a GitLab project
238+ - ✅ *Podman not Docker* - Always use Podman
239+ - ✅ *Dual Licensing* - MIT + Palimpsest v0.6
240240
241- ## License
241+ == License
242242
243243This project is dual-licensed under:
244244
@@ -247,7 +247,7 @@ This project is dual-licensed under:
247247
248248See [NOTICE](NOTICE) for complete license information.
249249
250- ## Citation
250+ == Citation
251251
252252If you use ECHIDNA in your research, please cite:
253253
@@ -261,20 +261,20 @@ If you use ECHIDNA in your research, please cite:
261261}
262262```
263263
264- ## Acknowledgments
264+ == Acknowledgments
265265
266266- Based on the Quill project (Agda neural solver)
267267- Built on the shoulders of the theorem proving community
268268- See [AUTHORS.md](AUTHORS.md) for contributor list
269269
270- ## Contact
270+ == Contact
271271
272- - ** GitLab Issues* * : https://gitlab.com/non-initiate/rhodinised/quill/-/issues
273- - ** Merge Requests* * : https://gitlab.com/non-initiate/rhodinised/quill/-/merge_requests
274- - ** Security* * : security@echidna-project.org
272+ - *GitLab Issues*: https://gitlab.com/non-initiate/rhodinised/quill/-/issues
273+ - *Merge Requests*: https://gitlab.com/non-initiate/rhodinised/quill/-/merge_requests
274+ - *Security*: security@echidna-project.org
275275
276276---
277277
278- ** Version* * : 0.1.0
279- ** Status* * : Active Development
280- ** Last Updated* * : 2025-11-22
278+ *Version*: 0.1.0
279+ *Status*: Active Development
280+ *Last Updated*: 2025-11-22
0 commit comments