# Logical framework

In logic, a **logical framework** provides a means to define (or present) a logic as a signature in a higher-order type theory in such a way that provability of a formula in the original logic reduces to a type inhabitation problem in the framework type theory.^{[1]}^{[2]} This approach has been used successfully for (interactive) automated theorem proving. The first logical framework was Automath; however, the name of the idea comes from the more widely known Edinburgh Logical Framework, **LF**. Several more recent proof tools like Isabelle are based on this idea.^{[1]} Unlike a direct embedding, the logical framework approach allows many logics to be embedded in the same type system.^{[3]}

## Overview

A logical framework is based on a general treatment of syntax, rules and proofs by means of a dependently typed lambda calculus. Syntax is treated in a style similar to, but more general than Per Martin-Löf's system of arities.

To describe a logical framework, one must provide the following:

- A characterization of the class of object-logics to be represented;
- An appropriate meta-language;
- A characterization of the mechanism by which object-logics are represented.

This is summarized by:

*‘Framework = Language + Representation’*.

## LF

In the case of the **LF logical framework**, the meta-language is the λΠ-calculus. This is a system of first-order dependent function types which are related by the propositions as types principle to first-order minimal logic. The key features of the λΠ-calculus are that it consists of entities of three levels: objects, types and families of types. It is predicative, all well-typed terms are strongly normalizing and Church-Rosser and the property of being well-typed is decidable. However, type inference is undecidable.

A logic is represented in the **LF logical framework** by the judgements-as-types representation mechanism. This is inspired by Per Martin-Löf's development of Kant's notion of judgement, in the 1983 Siena Lectures. The two higher-order judgements, the hypothetical and the general, , correspond to the ordinary and dependent function space, respectively. The methodology of judgements-as-types is that judgements are represented as the types of their proofs. A logical system is represented by its signature which assigns kinds and types to a finite set of constants that represents its syntax, its judgements and its rule schemes. An object-logic's rules and proofs are seen as primitive proofs of hypothetico-general judgements .

An implementation of the LF logical framework is provided by the Twelf system at Carnegie Mellon University. Twelf includes

- a logic programming engine
- meta-theoretic reasoning about logic programs (termination, coverage, etc.)
- an inductive meta-logical theorem prover

## See also

## References

- 1 2 Bart Jacobs (2001).
*Categorical Logic and Type Theory*. Elsevier. p. 598. ISBN 978-0-444-50853-9. - ↑ Dov M. Gabbay, ed. (1994).
*What is a logical system?*. Clarendon Press. p. 382. ISBN 978-0-19-853859-2. - ↑ Ana Bove; Luis Soares Barbosa; Alberto Pardo (2009).
*Language Engineering and Rigourous (sic) Software Development: International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24 - March 1, 2008, Revised, Selected Papers*. Springer. p. 48. ISBN 978-3-642-03152-6.

## Further reading

- Frank Pfenning (2002). "Logical frameworks – a brief introduction". In Helmut Schwichtenberg, Ralf Steinbrüggen.
*Proof and system-reliability*(PDF). Springer. ISBN 978-1-4020-0608-1. - Robert Harper, Furio Honsell and Gordon Plotkin.
*A Framework For Defining Logics*. Journal of the Association for Computing Machinery, 40(1):143-184, 1993. - Arnon Avron, Furio Honsell, Ian Mason and Randy Pollack.
*Using typed lambda calculus to implement formal systems on a machine*. Journal of Automated Reasoning, 9:309-354, 1992. - Robert Harper.
*An Equational Formulation of LF*. Technical Report, University of Edinburgh, 1988. LFCS report ECS-LFCS-88-67. - Robert Harper, Donald Sannella and Andrzej Tarlecki.
*Structured Theory Presentations and Logic Representations*. Annals of Pure and Applied Logic, 67(1-3):113-160, 1994. - Samin Ishtiaq and David Pym.
*A Relevant Analysis of Natural Deduction*. Journal of Logic and Computation 8, 809-838, 1998. - Samin Ishtiaq and David Pym.
*Kripke Resource Models of a Dependently-typed, Bunched -calculus*. Journal of Logic and Computation 12(6), 1061-1104, 2002. - Per Martin-Löf. "On the Meanings of the Logical Constants and the Justifications of the Logical Laws." "Nordic Journal of Philosophical Logic", 1(1): 11-60, 1996.
- Bengt Nordström, Kent Petersson, and Jan M. Smith.
*Programming in Martin-Löf's Type Theory*. Oxford University Press, 1990. (The book is out of print, but a free version has been made available.) - David Pym.
*A Note on the Proof Theory of the -calculus*. Studia Logica 54: 199-230, 1995. - David Pym and Lincoln Wallen.
*Proof-search in the -calculus*. In: G. Huet and G. Plotkin (eds), Logical Frameworks, Cambridge University Press, 1991. - Didier Galmiche and David Pym.
*Proof-search in type-theoretic languages:an introduction*. Theoretical Computer Science 232 (2000) 5-53. - Philippa Gardner.
*Representing Logics in Type Theory*. Technical Report, University of Edinburgh, 1992. LFCS report ECS-LFCS-92-227. - Gilles Dowek.
*The undecidability of typability in the lambda-pi-calculus*. In M. Bezem, J.F. Groote (Eds.), Typed Lambda Calculi and Applications. Volume 664 of*Lecture Notes in Computer Science*, 139-145, 1993. - David Pym.
*Proofs, Search and Computation in General Logic*. Ph.D. thesis, University of Edinburgh, 1990. - David Pym.
*A Unification Algorithm for the -calculus.*Int. J. of Foundations of Computer Science 3(3), 333-378, 1992.

## External links

- Specific Logical Frameworks and Implementations (a list maintained by Frank Pfenning)