Handbook of Automated Reasoning

4.4 Logic programming

Logic programming offers a different approach to meta-programming in a logical framework than ML or a separate strategy language. Rather than meta-programming in a language in which the logical framework itself is implemented (typically ML), we endow the logical framework with an operational interpretation in the spirit of Prolog. It should be clear that a specification of a logic under this approach does not automatically give rise to a theorem prover, but that theorem provers may be programmed in the meta-language. Two frameworks to date have pursued this approach: λProlog [λProlog 1997, Nadathur and Miller 1988], which gives an operational interpretation of hereditary Harrop formulas, and Elf [Pfenning and Schürmann ...