QU-PROLOG

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 quantifier s that create local scope s for those variables. Qu-Prolog is well suited as an implementation language for theorem prover s and support notations typically found in texts on mathematics and logic.