stellogen-proof-search
Installation
SKILL.md
Stellogen Proof Search
Category: Formal Verification - Automated Theorem Proving
Status: Production Ready (21 verified test cases)
Dependencies: theorem-prover-orchestration
Overview
Stellogen is a resolution-based prover using stellar resolution - bidirectional proof search with:
- Positive rays = axioms (covariant, "what we know")
- Negative rays = goals (contravariant, "what we want")
- Interaction = cut elimination as color-matching (GF(3) conservation)
21 test files covering automata, linear logic, Prolog, unification, and boolean logic.