File size: 763 Bytes
63d3857 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 | 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()
|