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]

  1. ^ a b Bart Jacobs (2001). Categorical Logic and Type Theory. Elsevier. p. 598. ISBN 978-0-444-50853-9.
  2. ^ Dov M. Gabbay, ed. (1994). What is a logical system?. Clarendon Press. p. 382. ISBN 978-0-19-853859-2.
  3. ^ Ana Bove; Luis Soares Barbosa; Alberto Pardo (2009). Language Engineering and Rigorous 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.