Capabilities
| Feature | Description |
|---|---|
| Satisfiability | Check if constraints have a solution |
| Model Finding | Find values that satisfy constraints |
| Proof Generation | Prove tautologies |
| Quantifiers | FORALL, EXISTS support |
| Arithmetic | Integer and real arithmetic |
Quick Start
QWED-Logic DSL
QWED uses a secure S-expression DSL for logic expressions.Operators
| Category | Operators | Example |
|---|---|---|
| Logic | AND, OR, NOT | (AND a b) |
| Comparison | GT, LT, EQ, GTE, LTE, NEQ | (GT x 5) |
| Implication | IMPLIES, IFF | (IMPLIES a b) |
| Quantifiers | FORALL, EXISTS | (FORALL x (GT x 0)) |
| Arithmetic | PLUS, MINUS, MULT, DIV | (PLUS x y) |
Examples
Satisfiability Checking
Basic Check
Finding All Solutions
Business Rules
Age Verification
Discount Eligibility
Approval Workflow
Quantifiers
Universal (FORALL)
Existential (EXISTS)
Security: Operator Whitelist
The DSL uses a strict whitelist - only approved operators are allowed:Error Handling
Performance
| Operation | Avg Latency |
|---|---|
| Simple constraint | 5ms |
| Complex (10+ clauses) | 20ms |
| Quantified | 50ms |
Next Steps
- DSL Reference - Complete operator documentation
- Code Engine - Verify code correctness
- SQL Engine - Verify SQL queries