\documentclass[全部作业]{subfiles}
\pagestyle{fancyplain}
\fancyhead{}
\fancyhead[C]{\mysignature}
\setcounter{chapter}{4}
\setcounter{section}{1}

\begin{document}
    \section{谓词公式的等值演算和前束范式}
    \begin{enumerate}
        \item 指出谓词公式$\forall x\forall y(P(x,y)\lor Q(y,z))\land \exists xR(x,y)$的指导变元、量词的辖域、约束变元和自由变元。
        \begin{figure}[h]
            \centering
            \includexopp[0.8]{7.1.1}
        \end{figure}
        \item 求谓词公式$\forall x \forall y (P(x,y) \leftrightarrow Q(x,y)) \to \exists  x \forall  y R(x,y)$的前束范式。
        \begin{proof}[解]
        \begin{zhongwen}
            $$
            \begin{aligned}
            &\forall x \forall y(P(x,y) \leftrightarrow Q(x,y)) \to \exists x \forall y R(x, y) \\
            =&\forall x \forall y(P(x,y)\leftrightarrow Q(x,y)) \to  \exists z \forall uR(z, u) & （换名）  \\
            =&\lnot (\forall x\forall y(P(x,y)\leftrightarrow Q(x,y)))\lor \exists z\forall uR(z,u) & （消去\to ） \\
            =&\exists x\exists y(\lnot (P(x,y)\leftrightarrow Q(x,y)))\lor \exists z\forall u R(z,u) & （内移\lnot ）\\
            =&\exists x\exists y\exists z\forall u(\lnot (P(x,y)\leftrightarrow Q(x,y))\lor R(z,u)) & （量词前移） \\
            =&\exists x\exists y\exists z\forall u((P(x,y)\leftrightarrow Q(x,y))\to R(z,u)) & （恢复\to （非必要）） \\
            \end{aligned}
            $$
        \end{zhongwen}
        \end{proof}
    \end{enumerate}
    \section{一阶逻辑的推理理论}
    \begin{enumerate}
        \item 构造$\forall x(P(x)\lor Q(x)), \forall x(Q(x) \to \lnot R(x)), \forall xR(x) \Rightarrow \forall xP(x)$的形式证明。
        \begin{proof}
        \begin{zhongwen}
            $$设y为任意的个体变量$$
            \begin{enumerate}[label=\mycircle{\arabic{enumii}},leftmargin=\linewidth/4,rightmargin=\linewidth/4]
                \item $\forall x(P(x)\lor Q(x))$\hfill 前提引入
                \item $P(y)\lor Q(y)$\hfill \mycircle{1} US规则
                \item $\forall x(Q(x)\to \lnot R(x))$\hfill 前提引入
                \item $Q(y)\to \lnot R(y)$\hfill  \mycircle{3} US规则
                \item $\forall xR(x)$ \hfill 前提引入
                \item $R(y)$\hfill \mycircle{5} US规则
                \item $\lnot Q(y)$\hfill \mycircle{4} \mycircle{6} 拒取式
                \item $P(y)$ \hfill  \mycircle{2} \mycircle{7} 析取三段论
                \item $\forall xP(x)$\hfill \mycircle{8} UG规则
            \end{enumerate}
        \end{zhongwen}
        \end{proof}
        \item 证明下面的推理：\\
        “每个科研工作者都是努力工作的。每个努力工作而又聪明的人都取得事业的成功。某个人是科研工作者并且聪明。所以，某人事业取得成功。”
        \begin{zhongwen}
            $$
            \begin{aligned}
            &设P(x): x是科研工作者，Q(x): x努力工作，R(x): x聪明，S(x): x取得事业的成功， \\
            &e: 某个人，则需要证明： \\
            &\forall x(P(x)\to Q(x)), \forall x (Q(x)\land R(x)\to S(x)), P(e)\land R(e) \Rightarrow S(e) \\
            \end{aligned}
            $$
        \end{zhongwen}
        \begin{proof}
        \begin{zhongwen}
            \begin{enumerate}[label=\mycircle{\arabic{enumii}},leftmargin=\linewidth/4,rightmargin=\linewidth/4]
                \item $P(e)\land R(e)$\hfill 前提引入
                \item $P(e)$\hfill \mycircle{1} 化简
                \item $R(e)$\hfill \mycircle{1} 化简
                \item $\forall x(P(x)\to Q(x))$\hfill 前提引入
                \item $P(e)\to Q(e)$\hfill \mycircle{4} US规则
                \item $Q(e)$\hfill \mycircle{2} \mycircle{5} 假言推理
                \item $Q(e)\land R(e)$\hfill \mycircle{3} \mycircle{6} 合取引入
                \item $\forall x(Q(x)\land R(x)\to S(x))$\hfill 前提引入
                \item $Q(e)\land R(e)\to S(e)$\hfill  \mycircle{8} US规则
                \item $S(e)$\hfill \mycircle{7} \mycircle{9} 假言推理
            \end{enumerate}
        \end{zhongwen}
        \end{proof}
    \end{enumerate}
\end{document}