Re: Avoiding variable clashes

[Hans Aberg]

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