Ow.

[kickaha]

I 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 )

Comments

[madpiratebippy.livejournal.com]

I have faith in you, don't worry, you'll rock the code and get it to behave like a good little schoolgirl who knows that tentacle is coming later.

Or, erm, something like that.