Assignment 6.

分析 Chap.5.1 (Lec.17) 自动售货机软件例子生成的判定表图例的第6列和第23列，分别给出：

(1) 输入条件的自然语义陈述；

第6列

售货机中有零钱找，投入一元硬币，按下橙汁按钮

第23列

售货机中没有零钱找，投入一元硬币，按下啤酒按钮

(2) 输出结果的自然语义陈述；

第6列

找回5角硬币，并送出橙汁饮料

第23列

售货机零钱找完，退还1元硬币

(3) 用命题逻辑形式描述实现上述输入-输出过程所应用的判定规则，并写出获得输出结果的推理演算过程。

第6列

• 输入11010，表示C1售货机有零钱找，C2投入1元硬币，C4按下橙汁按钮，输出00110，表示E23，找回5角硬币，E24送出橙汁饮料。

• 输入-输出过程的规则描述如下

KaTeX parse error: Expected 'EOF', got '\or' at position 5: C_4\̲o̲r̲ ̲C_{5} \Rightarr…

• 推理演算过程如下：以C1、C2、C4为前提，应用以下的步骤，可以证明逻辑结论E23、E24

$C_4\vee C_{5} \Rightarrow T_{12} \\ C_2\wedge T_{12} \Rightarrow T_{11} \\ C_1\wedge T_{11} \Rightarrow T_{13} \\ T_{13} \Rightarrow E_{23} \\ C_3\vee T_{13} \Rightarrow T_{14} \\ C_4\wedge T_{14} \Rightarrow E_{24}$C4​∨C5​⇒T12​C2​∧T12​⇒T11​C1​∧T11​⇒T13​T13​⇒E23​C3​∨T13​⇒T14​C4​∧T14​⇒E24​

第23列

• 输入01001，表示C2投入1元硬币，C5表示按下啤酒的按钮，输出11000，表示E21，售货机零钱找完了，E22，退还1元硬币。

• 输入-输出过程的规则描述如下
  $\sim C_1 \Rightarrow E_{21} \\ C_4 \vee C_5 \Rightarrow T_{12} \\ C_2 \wedge T_{12} \Rightarrow T_{11} \\ \sim C_1 \wedge T_{11} \Rightarrow E_{22}$∼C1​⇒E21​C4​∨C5​⇒T12​C2​∧T12​⇒T11​∼C1​∧T11​⇒E22​

• 推理演算过程如下：：以C2、C5为前提，应用以下的步骤，可以证明逻辑结论E21、E22

$\sim C_1 \Rightarrow E_{21} \\ C_4 \vee C_5 \Rightarrow T_{12} \\ C_2 \wedge T_{12} \Rightarrow T_{11} \\ \sim C_1 \wedge T_{11} \Rightarrow E_{22}$∼C1​⇒E21​C4​∨C5​⇒T12​C2​∧T12​⇒T11​∼C1​∧T11​⇒E22​