The following code is non-functional, just a sketch:

   class Subgroup : Definition
   {
   public:
      Set G;
      Set H;

   private:
      Assert[] given = [G in Grp("G"), H=subset(G, "H")];
      Assert[] input = [[a,b] in H >>> a*(b^(-1)) in H]];
      Assert[] output = [H ~ " is a subgroup of " ~ G];
      Notate[] denoted = [H ~ r"\leqslant " ~ G];
   }

There will be a gigantic brain-like graph. Nodes with I/O. For each new Definition/Assertion made by the user, I would like them to be automatically wired-into the brain graph up to variable substitution. So it's not as simple as using an AA to accomplish this. And I don't want to loop through all nodes and then check for all outputs that match the inputs, etc. So can you think of a way to accomplish this, especially that is D-friendly?

Up to variable substitution means there is a mechanism that knows that "A is a subgroup of B" is essentially the same thing as "H is a subgroup of G", you simply map the variables appropriately.