Sorting of Contexts

To make proofs with contexts check-able without parsing ahead, it is important that the context is explicitly sorted when it is introduced by anchor. After some back and forth we realized that it should be enough to sort only the fixed variables, i.e., the variables that shadow earlier substitutions. For variables that get substitutions the sort can be inferred from the substituted term. Of course the usual sorting requirements of SMT-LIB apply.

Furthermore, a variable can never be substituted with a free variable, but this should already be the case and would be of no use. This should be documented in the specifications.

An example: The anchor that was (anchor :step t3 :args (x (:= y x))) now has the form. (anchor :step t3 :args ((x S) (:= y x))).

Since this is a breaking change, action is needed for all systems following the Alethe development.

• Update the specification
• Generate sorted anchors in veriT (implemented in commit dd70e05)
• Generate sorted anchors as described here from cvc5
• Handle sorted anchors in Isabelle
• Handle sorted anchors as described here in the proof checker

assigned to @hjsc

added format + 1 deleted label

marked the checklist item Handle sorted anchors in Isabelle as completed

marked the checklist item Handle sorted anchors as described here in the proof checker as completed

marked the checklist item Update the specification as completed

changed milestone to %Release 0.4

closed