[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Avoiding variable clashes

From: Hans Aberg
Subject: Re: Avoiding variable clashes
Date: Wed, 13 Apr 2011 18:33:13 +0200

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.


reply via email to

[Prev in Thread] Current Thread [Next in Thread]