Questions tagged [logical-frameworks]
Use this tag for proof assistants that are intended to be used to define logics or deductive systems in them.
4
questions
10
votes
1
answer
248
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 ...
- 314
3
votes
0
answers
79
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,868
9
votes
1
answer
145
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,846
13
votes
1
answer
171
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 ...
- 1,013