Skip to content

Premises from outside of a subproof

In the case of veriT, a step in a subproof can never use the conclusion of a step from outside the subproof. Cvc5, however, can do this. We need to investigate if this is always fine and clarify this in the document.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information