An extension of Prolog which performs meta-levelcomputations over object languages, such as predicatecalculi 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.