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.