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]
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 
. 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.0 1.1 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. 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)