[FOM] Question about "fresh" variables/objects in logics
obua at in.tum.de
Sat Nov 26 09:23:44 EST 2005
Divianszky Peter wrote:
>Does anybody know of a formal description of the concept of "fresh"
>variable/object in logic?
>This concept is used in theoretical computer science quite often, but I
>have never seen a formal description of it.
You might be interested in the work of Christian Urban. He is developing
a system to reason about proofs in higher-order logic that takes
special care of the treatment of fresh variables. This is work along
the lines of the "nominal approach" introduced by Andrew Pitts.
See http://www.mathematik.uni-muenchen.de/~urban/publications.html, for
example "Nominal Reasoning Techniques in Isabelle/HOL".
More information about the FOM