LOP

A language based on first-order logic.

"SETHEO - A High-Perormance Theorem Prover for First-Order Logic", Reinhold Letz et al, Journal of Automated Reasoning 8(2):183-212 (1992).