An extension of Prolog whICh performs {meta-level computation}s over {object language}s, 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.