2
$\begingroup$

(This is HW.) Suppose I have these following proof rules given. rules I have now

I am currently considering if I can prove the conjunction rule (given below) from the above given Hoare logic rules.

conjunction rule

My answer would be "no", because from the proof rules of Hoare logic, I can neither use the Implied rule to prove it (because from $A$ I cannot infer $A \wedge B$) nor introduce it anywhere from the first four proof rules (the only one which introduces conjunction in the post-condition requires a while). I am fairly confident that this line of reasoning is correct, but am I missing anything? For example, can I argue on a the propositional logic level that since I have $P$ as a precondition, and I have $Q_1$ and $Q_2$ as postconditions, I can simply introduce conjunction on the propositional logic level (instead of inferring purely on Hoare logic)?

$\endgroup$
3
$\begingroup$

Your reasoning is fine as far as the derivability of this rule. To respond to the latter part of your last paragraph, if the rules you've listed are all the rules available, then those are the only rules you can use. A derivation is a tree of applications of rules. You need to be able to state what rule you're using at each node in that tree. A(n explicit) proof that this rule was derivable would be an actual derivation, i.e. tree of rule applications.

There's a different and (slightly) harder question that you probably were not asked which is whether the Conjunction Rule is admissible. That is, could the Conjunction Rule be added without causing any problems, i.e. unsoundness.

$\endgroup$
  • $\begingroup$ I thought "admissible rule" meant "you can add this rule, but it won't change the inductively defined relation", and not only "it won't break soundness". Is that term also used with the second meaning? $\endgroup$ – chi Mar 12 at 8:55
  • $\begingroup$ @chi You're right. What I'm calling "admissible" here is actually a weaker notion that only requires the set of "theorems" to contain the "theorems" of the original system rather than be the same. The stronger, more usual, notion is also interesting here. $\endgroup$ – Derek Elkins Mar 13 at 3:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.