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
4
questions
9
votes
1
answer
183
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 ...
- 294
3
votes
0
answers
75
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:
...
- 2,748
8
votes
1
answer
127
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"...
- 2,826
13
votes
1
answer
140
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 ...
