Skip to main content

Questions tagged [logical-frameworks]

Use this tag for proof assistants that are intended to be used to define logics or deductive systems in them.

Filter by
Sorted by
Tagged with
10 votes
1 answer
237 views

How "generic" are "generic proof assistants"?

I've read that Isabelle and Metamath (and maybe Andromeda) are "generic" proof assistants in some sense that allows them to be used to implement different theories such as HOL, ZF and ...
Max New's user avatar
  • 314
3 votes
0 answers
78 views

What are some "real world" first order logical theories for demos?

I'm working on a tool for first order logical theories. I want to show the tool can work with real world logical theories. What are some good theories for demos? I think I want demos that are: ...
Ms. Molly Stewart-Gallus's user avatar
9 votes
1 answer
140 views

How does a logical framework become a meta-logical framework?

In a recent answer, Isabelle was noted as a Logical Framework. A comment noted it was a Meta-Logical Framework. In researching for an understanding found "Logical and Meta-Logical Frameworks"...
Guy Coder's user avatar
  • 2,846
13 votes
1 answer
167 views

Attempts to accommodate theories of different consistency strength in single assistant

TL;DR: How / where to formalize results concerning the logical strength of systems? Are proof assistants having a weak base theory but also enough infrastructure to make it feasible? I'll start by ...
Pedro Sánchez Terraf's user avatar