In
logic
Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from premises ...
, a logical framework provides a means to define (or present) a logic as a signature in a higher-order
type theory
In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a foundat ...
in such a way that
provability of a formula in the original logic reduces to a
type inhabitation In type theory, a branch of mathematical logic, in a given typed calculus, the type inhabitation problem for this calculus is the following problem: given a type \tau and a typing environment \Gamma, does there exist a \lambda-term M such that \Gam ...
problem in the framework type theory.
This approach has been used successfully for (interactive)
automated theorem proving
Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a maj ...
. The first logical framework was
Automath
Automath ("automating mathematics") is a formal language, devised by Nicolaas Govert de Bruijn starting in 1967, for expressing complete mathematical theories in such a way that an included automated proof checker can verify their correctness.
Ove ...
; however, the name of the idea comes from the more widely known Edinburgh Logical Framework, LF. Several more recent proof tools like
Isabelle
Isabel is a female name of Spanish origin. Isabelle is a name that is similar, but it is of French origin. It originates as the medieval Spanish form of '' Elisabeth'' (ultimately Hebrew ''Elisheva''), Arising in the 12th century, it became popul ...
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
Per Erik Rutger Martin-Löf (; ; born 8 May 1942) is a Swedish logician, philosopher, and mathematical statistician. He is internationally renowned for his work on the foundations of probability, statistics, mathematical logic, and computer scie ...
'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
In computer science and logic, a dependent type is a type whose definition depends on a value. It is an overlapping feature of type theory and type systems. In intuitionistic type theory, dependent types are used to encode logic's quantifiers lik ...
. This is a system of first-order dependent function types which are related by the
propositions as types principle
In logic and linguistics, a proposition is the meaning of a declarative sentence (linguistics), sentence. In philosophy, "Meaning (philosophy), meaning" is understood to be a non-linguistic entity which is shared by all sentences with the same me ...
to
first-order
In mathematics and other formal sciences, first-order or first order most often means either:
* "linear" (a polynomial of degree at most one), as in first-order approximation and other calculus uses, where it is contrasted with "polynomials of high ...
minimal logic
Minimal logic, or minimal calculus, is a symbolic logic system originally developed by Ingebrigt Johansson. It is an intuitionistic and paraconsistent logic, that rejects both the law of the excluded middle as well as the principle of explosion (' ...
. 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
In abstract rewriting, an object is in normal form if it cannot be rewritten any further, i.e. it is irreducible. Depending on the rewriting system, an object may rewrite to several normal forms or none at all. Many properties of rewriting systems ...
and
Church-Rosser and the property of being well-typed is
decidable. However,
type inference
Type inference refers to the automatic detection of the type of an expression in a formal language. These include programming languages and mathematical type systems, but also natural languages in some branches of computer science and linguistics ...
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
Per Erik Rutger Martin-Löf (; ; born 8 May 1942) is a Swedish logician, philosopher, and mathematical statistician. He is internationally renowned for his work on the foundations of probability, statistics, mathematical logic, and computer scie ...
's development of
Kant
Immanuel Kant (, , ; 22 April 1724 – 12 February 1804) was a German Philosophy, philosopher and one of the central Age of Enlightenment, Enlightenment thinkers. Born in Königsberg, Kant's comprehensive and systematic works in epistemolo ...
's notion of
judgement
Judgement (or US spelling judgment) is also known as ''adjudication'', which means the evaluation of evidence to make a decision. Judgement is also the ability to make considered decisions. The term has at least five distinct uses. Aristotle s ...
, 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
A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system.
A form ...
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 Twelf is an implementation of the logical framework LF developed by Frank Pfenning and Carsten Schürmann at Carnegie Mellon University. It is used for logic programming and for the formalization of programming language theory.
Introduction
At i ...
system at
Carnegie Mellon University
Carnegie Mellon University (CMU) is a private research university in Pittsburgh, Pennsylvania. One of its predecessors was established in 1900 by Andrew Carnegie as the Carnegie Technical Schools; it became the Carnegie Institute of Technology ...
. Twelf includes
* a logic programming engine
* meta-theoretic reasoning about logic programs (termination, coverage, etc.)
* an inductive
meta-logic
Metalogic is the study of the metatheory of logic. Whereas ''logic'' studies how logical systems can be used to construct valid and sound arguments, metalogic studies the properties of logical systems.Harry GenslerIntroduction to Logic Routledge, ...
al theorem prover
See also
*
Grammatical Framework
Grammatical Framework (GF) is a programming language for writing grammars of natural languages. GF is capable of parsing and generating texts in several languages simultaneously while working from a language-independent representation of meaning. ...
*
Turnstile (symbol)
In mathematical logic and computer science the symbol \vdash has taken the name turnstile because of its resemblance to a typical turnstile if viewed from above. It is also referred to as tee and is often read as "yields", "proves", "satisfies" o ...
References
Further reading
* {{cite book, editor=
Helmut Schwichtenberg
Helmut Schwichtenberg (born 5 April 1942 in Żagań) is a German mathematical logician.
Schwichtenberg studied mathematics from 1961 at the FU Berlin and from 1964 at the University of Münster, where he received his doctorate in 1968 from D ...
, Ralf Steinbrüggen, title=Proof and system-reliability, chapter=Logical frameworks – a brief introduction, year=2002, publisher=
Springer
Springer or springers may refer to:
Publishers
* Springer Science+Business Media, aka Springer International Publishing, a worldwide publishing group founded in 1842 in Germany formerly known as Springer-Verlag.
** Springer Nature, a multinationa ...
, isbn=978-1-4020-0608-1, author=
Frank Pfenning
Frank Pfenning is a German-American professor of computer science, adjunct professor in the department of philosophy, and head of the Computer Science Department at Carnegie Mellon University.
Education and career
Pfenning grew up in Rüssel ...
, url=https://www.cs.cmu.edu/~fp/papers/mdorf01.pdf
*
Robert Harper Robert or Bob Harper may refer to:
* Robert Almer Harper (1862–1946), American botanist
* Robert Goodloe Harper (1765–1825), US senator from Maryland
* Robert Harper (fl. 1734–1761), founder of Harpers Ferry, West Virginia
* Robert Harper (a ...
, Furio Honsell and
Gordon Plotkin
Gordon David Plotkin, (born 9 September 1946) is a theoretical computer scientist in the School of Informatics at the University of Edinburgh. Plotkin is probably best known for his introduction of structural operational semantics (SOS) and hi ...
. ''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
The University of Edinburgh ( sco, University o Edinburgh, gd, Oilthigh Dhùn Èideann; abbreviated as ''Edin.'' in post-nominals) is a public research university based in Edinburgh, Scotland. Granted a royal charter by King James VI in 15 ...
, 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
Nordic most commonly refers to:
* Nordic countries, written in plural as Nordics, the northwestern European countries, including Scandinavia, Fennoscandia and the North Atlantic
* Scandinavia, a cultural, historical and ethno-linguistic region ...
", 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
Oxford University Press (OUP) is the university press of the University of Oxford. It is the largest university press in the world, and its printing history dates back to the 1480s. Having been officially granted the legal right to print books ...
, 1990. (The book is out of print, bu
a free versionhas 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
Lincoln Wallen is a British-American computer scientist and the Chief Technology Officer (CTO) of Improbable (company), Improbable. He is the former CTO of DreamWorks Animation.
Wallen received a first-class degree in Mathematics and Physics fr ...
. ''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.'' 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
Frank Pfenning is a German-American professor of computer science, adjunct professor in the department of philosophy, and head of the Computer Science Department at Carnegie Mellon University.
Education and career
Pfenning grew up in Rüssel ...
, but mostly dead links from 1997)
Logic in computer science
Type theory
Proof assistants
Dependently typed programming