Logical frameworks are essentially strictly related to proof assistance.
What is really a proof assistant? Well, if we build an interactive proof
development environment for higher order constructive type theory, since
constructive type theory is can be use as computational metamodel, this
readily provides a generally interactive proof development environment
for a generic logic. | ![]() |