| from backend.core.universe_generator import UniverseGenerator | |
| from backend.core.theorem_engine import TheoremEngine | |
| from backend.db.session import SessionLocal | |
| def test_theorem_derivation(): | |
| db = SessionLocal() | |
| generator = UniverseGenerator(db) | |
| universe = generator.create_universe("Thm Universe", "For theorem derivation", "generic", ["Closure", "Associativity"]) | |
| axiom1 = generator.add_axiom(universe.id, "Closure") | |
| axiom2 = generator.add_axiom(universe.id, "Associativity") | |
| engine = TheoremEngine(db) | |
| theorem = engine.derive_theorem(universe.id, [axiom1.id, axiom2.id], "Closure Associativity") | |
| assert theorem.statement == "Closure Associativity" | |
| assert "Derived from axioms" in theorem.proof | |
| db.close() | |