Symbolically Guided Science

Einstein's famous equivalence e=mc² is a fairly simple symbol sequence. Given basic constraints such as unit agreement it could be discovered quickly using random search. The hard part is interpreting — the semantics. Assuming that some grand unified theory exists, one that's elegant, perhaps we can develop an automated search for it constrained by simple requiremenrs like unit agreement and some formal semantics describing observed behavior? The few theories that match observations but make unexpected predictions could be presented for further consideration by humans.