Logic programming
Most of the articles and examples on this wiki are focused towards using STELF as a specification language, useful for encoding an object logic and then stating and proving metatheorems about that object logic. However, STELF originated from Elf, and like Elf it is a dependently-typed, higher-order logic programming language based on the logic LF.
A STELF signature may contain, among other things, some type family declarations and some constants inhabiting those type families. A logic programming language takes a type as an input, and it then uses a simple search strategy to try and discover a term that has that type using the constants that have been defined. By the judgments as types principle, this means that STELF is searching for a derivation - a proof witness - of a particular judgment.
STELF’s logic programming engine is activated by %solve and %query directives. It can also be activated directly inside ML; see the section on interactive queries (guide §5.22) for more information. STELF’s tabled logic programming engine is activated by the %querytabled directive.
Uses of logic programming in STELF
Section titled “Uses of logic programming in STELF”- Implementing a reference typechecker/evaluator - If the static and dynamic semantics of a programming language are written correctly, then the specification of the static semantics can be . This was a component to the The POPLmark Challenge challenge; the case study of a language with references, among other examples, demonstarte STELF in this capacity.
- Writing programs and then proving things about them: The TALT project includes a code checker written as a STELF logic program, along with a proof in STELF that code that passes the checker is safe according to a safety policy.
- Tactical theorem proving - in the style described by Appel and Felty in .
See also
Section titled “See also”- Logic Programming (guide §5.22)
- Logic programming at Wikipedia