Free On-line Dictionary of Computing:
qu-prolog
An extension of
Prolog which performs {meta-level computations} over object languages, such as predicate calculi and {lambda-calculi}, which have object-level
variables, and quantifiers that create local scopes for
those variables. Qu-Prolog is well suited as an implementation
language for theorem provers and support notations typically
found in texts on mathematics and logic.
