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 (theorem prover) are based on this idea. Unlike a direct embedding, the logical framework approach allows many logics to be embedded in the same type system.
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’.
Read more about Logical Framework: LF
Famous quotes containing the words logical and/or framework:
“Opera, next to Gothic architecture, is one of the strangest inventions of Western man. It could not have been foreseen by any logical process.”
—Kenneth MacKenzie Clark, Baron of Saltwood (1903–1983)
“The city is a fact in nature, like a cave, a run of mackerel or an ant-heap. But it is also a conscious work of art, and it holds within its communal framework many simpler and more personal forms of art. Mind takes form in the city; and in turn, urban forms condition mind.”
—Lewis Mumford (1895–1990)