Questions tagged [logical-frameworks]

Use this tag for proof assistants that are generic, in that they allow a variety of logics to used with them

Filter by
Sorted by
Tagged with
3 votes
0 answers

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: ...
user avatar
7 votes
1 answer

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"...
user avatar
  • 2,676
13 votes
1 answer

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 ...
user avatar