Skip to main content
9 votes
Accepted

Attempts to accommodate theories of different consistency strength in single assistant

You could address your goals by using a generic proof assistant, one that supports user-definable theories, such as Isabelle and Metamath, and I am sure there are others. These allow you to define ...
Andrej Bauer's user avatar
  • 9,503
6 votes
Accepted

How "generic" are "generic proof assistants"?

Isabelle/Sequents contains a formalisation of intuitionistic linear logic, so conceivably you have a chance of implementing your logic in Isabelle, following the techniques used there. Whether what ...
Lawrence Paulson's user avatar
2 votes
Accepted

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

Let me try taking a stab at a few provisional definitions. I can make these arbitrarily rigorous, but being fully general makes it hard to see the forest for the trees (at least, for me). Provisional ...
Alex Nelson's user avatar
  • 1,564

Only top scored, non community-wiki answers of a minimum length are eligible