On 13 Apr 2011, at 18:25, Noah Lavine wrote: > I think that mechanism is all that Guile uses at present. However, it > should be general enough to resolve all situations where variables of > the same name refer to different entities, assuming you set up the > environments correctly. > > Are you planning on implementing a theorem prover for Guile? That would be > cool.
Or at least having something to experiment with. From Andy's description, it seems one may merely have to disable the beta-rule. I wrote on a theorem prover that pushed comparison of clauses into the unification, admitting unification branching, and doing breadth-first search. The hard part was resolving variable clashes in substitution. Hans
