Skip to content

Symm and Not_Symm Rule

We have decided a while ago already to add two new proof rules to Alethe but have not added them to the Standard yet:

https://alethe.zulipchat.com/#narrow/stream/304854-isabelle-reconstruction/topic/Not_Symm/near/259117445

image

SYMM corresponds to the first case in this graphic (from the cvc5 proof calculus), the NOT_SYMM to the second. They are already used in cvc5, Isabelle and Carcara.

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