LAB4: 谓词逻辑系统自动证明

回顾coq程序基本的结构：

Theorem (题目名字): forall P Q(所有变量) :Prop,需要证明的结论。
Proof.证明的过程。
Qed.

命题逻辑

intros 蕴含得到命题所有前提
inversion H 反演将前提H左边拆成两份（合取析取均可）
unford not 非将条件中的~变成false
elim 消除谬误如果条件中有H0：P->false此时使用命令elim H0命令相当于只需要证明P的正确性
spilt 拆分将合取结论拆成两份
left 和 right 选择析取结论的左半部分和右半部分
apply 应用如果条件H与结论相同，可直接使用apply H完成证明
apply A in B 以B为前提，结合A能够推出的结果,这里一定要注意顺序
assert (h : H) 假设H为一个新的目标当你证明了这个新的目标时 h作为你新的前提
destruct 同inversion 将原命题拆分成两个命题，但可分别命名

谓词逻辑

Variables A B: Set. 定义A,B两个两个集合
Variables P Q:A -> Prop. 在集合A上定义谓词变量P,Q
Variable R : A -> B -> Prop. 谓词变量R定义在A集合和集合B上，Prop代表某种性质

需要运用到的指令大部分都在上面，其他的按照逻辑一步一步推演即可, 总体而言难度不如上lab3。

结果如下：

Theorem exercise_1: forall P Q: Prop,~(P \/ Q) -> ~P /\ ~Q.
Proof.unfold not.intros.split.intros.apply H.left.apply H0.intros.apply H.right.apply H0.
Qed.Theorem exercise_2 : forall P Q R: Prop,P /\ (Q \/ R) <-> (P /\ Q) \/ (P /\ R).
Proof.split.intros.destruct H as [H1 H2].inversion H2.left.split.apply H1.apply H.right.split.apply H1.apply H.intros.destruct H as [H1 | H2].inversion H1.split.apply H.left.apply H0.split.inversion H2.apply H.right.inversion H2.apply H0.
Qed.Variables A B: Set.
Variables P Q R: A->Prop.
Theorem exercise_3:(forall x:A, ~P x /\ Q x) -> (forall x:A, P x -> Q x).
Proof.intros.apply H.
Qed.Theorem exercise_4:(forall x: A, (P x -> Q x)) -> (forall x: A,~Q x) -> (forall x: A, ~P x).
Proof.intros.intros H1.apply H in H1.apply H0 in H1.apply H1.
Qed.Theorem exercise_5:(forall x: A, (P x /\ Q x)) <-> (forall x: A,P x) /\ (forall x: A, Q x).
Proof.split.split.intros.apply H.apply H.intros.split.apply H.apply H.
Qed.Theorem exercise_6:(exists x:A, (~P x \/ Q x)) -> (exists x:A, (~(P x /\ ~Q x))).
Proof.intros.inversion H.exists x.inversion H0.intros H2.inversion H2.apply H1 in H3.apply H3.intros H4.inversion H4.apply H3 in H1.apply H1.
Qed.Theorem exercise_7:(exists x:A, (~P x /\ ~Q x)) -> (exists x:A, ~(P x /\ Q x)).
Proof.intros.inversion H.exists x.intros H1.inversion H0.inversion H1.apply H3 in H5.apply H5.
Qed.Theorem exercise_8:(exists x:A, (P x \/ Q x)) <-> (exists x:A, P x) \/ (exists x:A, Q x).
Proof.split.intros.inversion H.inversion H0.left.exists x.apply H1.right.exists x.apply H1.intros.inversion H.inversion H0.exists x.left.apply H1.inversion H0.exists x.right.apply H1.
Qed.Theorem exercise_9:(exists x:A, ~P x) -> ~(forall x:A, P x).
Proof.intros.inversion H.unfold not.intros.apply H0 in H1.apply H1.
Qed.Theorem exercise_10:(forall x:A, P x -> ~Q x) -> ~(exists x:A, (P x /\ Q x)).
Proof.unfold not.intros.inversion H0.inversion H1.apply H in H2.apply H2.apply H3.
Qed.Theorem exercise_11:(forall x:A, P x -> Q x) /\ (exists x:A, P x ) -> (exists x:A, Q x).
Proof.unfold not.intros.inversion H.inversion H1.apply H0 in H2.exists x.apply H2.
Qed.Theorem exercise_12:(exists x:A, P x /\ Q x) /\ (forall x:A, P x -> R x) -> (exists x:A, R x /\ Q x).
Proof.intros.inversion H.inversion H0.inversion H2.apply H1 in H3.exists x.split.apply H3.apply H4.
Qed.

形式化方法 Assignment 4: Proof for predicate logic相关推荐

形式化方法 Assignment 3: SAT
作业3 软件解决SAT问题 Part A: SAT基本问题的编码 /\ And 与 \/ Or 或 ~ Not 非 -> Implies 蕴含判断命题是否具有SAT性质 F = Or(P, Q ...
形式化方法、《大象：Thinking in UML》
形式化方法英文的名称是formal methods.在逻辑科学中是指分析.研究思维形式结构的方法.它把各种具有不同内容的思维形式(主要是命题和推理)加以比较,找出其中各个部分相互联结的方式,如命题中包 ...
【形式化方法：VDM++系列】4.VDM实战1——铁路费用计算
又有将近2个月没更新博客了啊!winter holiday简直玩儿疯了的说!结果假期前学习的形式化方法已经忘了大半!面对期末作业,大脑一片空白.于是,赶快复习了一下之前学习的姿势! 这次的主要任务是完 ...
形式化方法｜形式化方法对软件开发的挑战：历史与发展
几年前到某著名大学参加学术活动,无意中听到该校两位老师闲聊,现在还记得的一句话就是"形式化方法已经不行了".看来真是隔行如隔山,评价自己不熟悉的领域,而且随便说,难免出错.在对形式 ...
形式化方法-- petri net
形式化方法-Petri net Petri net是由C.A.Petri在其博士论文中提到的,petri net 通常包含以下几个元素,分别是:库所.变迁.流关系.容量函数.初始标识.权值函数.所以p ...
2022 CCF形式化方法工业应用前沿分论坛暨中科国创高可信联合上海控安新品发布会顺利召开！...
11月27日,2022年CCF中国软件大会"形式化方法工业应用前沿"技术分论坛暨中科国创高可信联合上海控安新品发布会于线上顺利召开.本次活动由CCF形式化方法专业委员会主办,华东师 ...
CCF ChinaSoft 2022预告丨形式化方法工业应用前沿分论坛暨中科国创高可信联合上海控安新品发布...
2022年11月25-27日,2022年CCF中国软件大会(CCF ChinaSoft 2022)将于线上举行.大会将围绕"聚焦产教研用协同创新,提升关键软件供给能力"主题,举办包 ...
软件工程——形式化方法概述
目录前言一.形式化方法定义二.形式化方法分类三.形式化方法意义四.形式化方法作用五.形式化方法优缺点 1.优点 2.缺点前言形式化方法英文的名称是formalmethods,形式化方法 ...
【形式化方法】Part B: SAT And Validity（SAT和有效性）
Part B: SAT 和有效性 In Exercise 1, we've learned how to represent propositions in Z3 and how to use Z3 ...
形式化方法（Formal Methods）
形式化方法是基于严密的.数学上的形式机制的计算机系统研究方法. 形式化方法(FM-Formal Method)知识体系中的6个知识领域为: ① 基础(Foundations); ② 形式化规格(For ...

形式化方法 Assignment 4: Proof for predicate logic

LAB4: 谓词逻辑系统自动证明

回顾coq程序基本的结构：

命题逻辑

谓词逻辑

形式化方法 Assignment 4: Proof for predicate logic相关推荐

最新文章

热门文章