![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
kickahaI spend a week trying to get a simple equational relationship working in the automated theorem prover, to no avail. It led to these horrendously complex inferred clauses that, while technically logically correct, were not at all what I wanted it to produce. (That's what I get for trying to use demodulation as term rewriting. But I digress.)
Was stumped and frustrated until I realized that because I normalized the entire object model into a simple assignment/call structure, I could actually enumerate all the instances of the Self construct and thereby force it into a first order logic by making explicit sigma-bindings for each permutation of where Self appeared in each of the relationships. Whoo-hoo!
Well, I finished the enumeration proof tonight.
304 equations. All similar, all slightly different, all have to be coded up and then tested.
Tomorrow.
*whimper*
(I'm seriously considering writing a tool to produce them by walking the permutation space. :P )
Was stumped and frustrated until I realized that because I normalized the entire object model into a simple assignment/call structure, I could actually enumerate all the instances of the Self construct and thereby force it into a first order logic by making explicit sigma-bindings for each permutation of where Self appeared in each of the relationships. Whoo-hoo!
Well, I finished the enumeration proof tonight.
304 equations. All similar, all slightly different, all have to be coded up and then tested.
Tomorrow.
*whimper*
(I'm seriously considering writing a tool to produce them by walking the permutation space. :P )