• Source: 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. 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. Unlike a direct embedding, the logical framework approach allows many logics to be embedded in the same type system.




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 kinds (or type classes, or 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



J
⊢
K


{\displaystyle J\vdash K}

and the general,



Λ
x
∈
J
.
K
(
x
)


{\displaystyle \Lambda x\in J.K(x)}

, 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





L




{\displaystyle {\mathcal {L}}}

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



Λ
x
∈
C
.
J
(
x
)
⊢
K


{\displaystyle \Lambda x\in C.J(x)\vdash K}

.
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


Grammatical Framework
Turnstile (symbol)




References






Further reading


Frank Pfenning (2002). "Logical frameworks – a brief introduction". In Helmut Schwichtenberg, Ralf Steinbrüggen (ed.). 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



λ


{\displaystyle \lambda }

-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



λ
Π


{\displaystyle \lambda \Pi }

-calculus. Studia Logica 54: 199-230, 1995.
David Pym and Lincoln Wallen. Proof-search in the



λ
Π


{\displaystyle \lambda \Pi }

-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



λ
Π


{\displaystyle \lambda \Pi }

-calculus. International Journal of Foundations of Computer Science 3(3), 333-378, 1992.




External links


Specific Logical Frameworks and Implementations (a list maintained by Frank Pfenning, but mostly dead links from 1997)

Kata Kunci Pencarian:

• Banten Mengajar
• Model OSI
• Forensik digital
• Sejarah kecerdasan buatan
• Graph database
• Logical framework
• Logical Framework Approach
• Framework
• Nonstandard analysis
• Logical Volume Manager (Linux)
• Higher-order abstract syntax
• Genesis creation narrative
• LEGO (proof assistant)
• Results-based management
• Lf