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 ^b 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 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.

[Jacobs2001-1] Bart Jacobs (2001). Categorical Logic and Type Theory. Elsevier. p. 598. ISBN 978-0-444-50853-9.

[Gabbay1994-2] Dov M. Gabbay, ed. (1994). What is a logical system?. Clarendon Press. p. 382. ISBN 978-0-19-853859-2.

[BoveBarbosa2009-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.

[1]

[2]

[3]