The material from yesterday's lecture is in the web site, including the one-way bridge model up to the point where we stopped. But please try to finish it with the material in the lecture on your own. Consult the model only if really necessary (because, e.g., things are really not working your you). Have it ready for next Wednesday, as we will continue working on it.
Those of you who want to send me again first part of the first exercise sheet, please do so until next Wednesday *before the lecture*, so that I can quickly comment on the solutions next Wed. I cannot accept resubmissions after 4pm CET, Wed. 24th March.
There was a question about the difference between theorems and non-theorems (in Rodin). From https://www3.hhu.de/stups/handbook/rodin/current/html/theorems.html: "Axioms, invariants and guards can be marked as theorems. This means that the validity of the theorems must be proven from the axioms, invariants or guards declared before the theorem."
This definition does not shed light on why and when they are useful. First, an axiom/invariant/guard that is marked as a theorem can be used anywhere axioms/invariants/guards are used. Using them is sound if the theorem has been proved. The main corresponding PO is THM, and may involve other POs such as WD. The difference is how we prove a theorem vs. a non-theorem.
An axiom marked as theorem has to be proved using the axioms (marked as theorem or no) *that appear before it*. On the other hand, a non-theorem axiom does not need a proof (but it may need e.g. WD POs): it is an initial truth.
An invariant marked as a theorem has to be proven using the existing axioms (theorems or not) and the invariants (theorems or not) that appear before it. The INV PO is not necessary for theorem invariants, because they are derived from formulas that are invariants themselves.
A guard marked as theorem can use all axioms and invariants plus the guards of the same event that appear before it. For example, in our one-way bridge model we may add the theorem guard "a + b + c ≤ n" and it will be discharged using the guards before it and the gluing invariant.
Theorems can be used to:
a) Have Rodin prove a specific property that is not a PO. For example, absence of deadlock is something that we may want or not. So we can write a formula that expresses it (as we did) and just "trick" Rodin into proving it by making it an invariant theorem which instructs Rodin to use whatever is available to prove it. It could as well be marked as a regular, non-theorem invariant. But in this case more proofs have to be done, because its establishment/preservation has to be proven for every event (5 proofs, in our case). If we mark it as a theorem, only one proof needs to be done, as it depends only on invariants and axioms. Of course not all invariant properties can be proven based on the rest of the invariants: some of them need to ensure that they are preserved across event activations. In the end, some invariant has to be the first one.
b) Have pre-proved formulas that are useful in the proving process. That can happen because they often appear in manually-assisted proofs (as we hinted at with the use of f(i) > f(j) ⇒ i > j instead of i ≤ j ⇒ f(i) ≤ f(j) in the sorted array example), or because they are necessary to help automatic provers discharge some PO. In this sense they act as lemmas or auxiliary formulas in the CUT rule, which theorem provers don't use by themselves, but which we can simulate by introducing intermediate formulas (theorems) when we think it's appropriate.
Best regards,