精华内容
下载资源
问答
  • 在Lukasiewicz命题逻辑中的全体赋值集上引入了不确定性测度的概念, 利用McNaughton函数关于该不确定性测度的Choquet积分定义命题的Choquet积分真度概念. 证明了当赋值空间上的不确定性测度满足有限可加性时Choquet...
  • 在二值命题逻辑系统,利用势为2均匀概率测度空间无穷乘积,通过计算理论[Γ]全体模型占整个赋值空间测度定义了理论[Γ]真度,进而利用理论真度简化了理论发散度和相容度计算公式,给出了由推理...
  • 将三值命题逻辑系统真度概念引入到概率逻辑定义公式期望,给出反映公式之间内在联系相关系数,研究无限公式收敛时所遵循规律及特点,引入度量不确定性特征值一熵.
  • 在n值[S-MTL]逻辑系统的统一框架下,通过视全体赋值之集为通常乘积拓扑空间,给出了命题的Borel概率真度定义。通过构造公式所诱导的阶梯函数给出了公式真度的积分表达式,进而利用命题的Borel概率真度在该逻辑系统...
  • 基于均匀概率空音无穷乘积在匕ukasiewicz三值命题逻辑中引入了公式可靠真度概念,证明了全体公式可靠真度值之集在[0,1]中没有孤立点;利用可靠真度定义了可靠相似度和伪距离,进而建立了逻辑度量空间,证明了...
  • 将二值命题逻辑系统真度概念引入到概率逻辑定义了公式期望,给出了反映公式之间内在联系相关系数,研究了无限公式收敛时所遵循规律及特点,引入了度量不确定性特征值—熵。
  • 给出Lukasiewicz,l值命题逻辑中公式α-随机真度概念和性质,利用α-随机真度定义了公式间α-D2相似度,进而导出全体公式集上一种伪距离。
  • 在[n]值[R0]命题逻辑系统给出了公式列按真度收敛的定义,研究了公式列按度量收敛、按赋值收敛及按真度收敛的性质,给出了三种收敛各自的充分必要条件,在公式列是有限原子的条件下证明了公式列按度量收敛、按赋值...
  • 通过引入赋值密度函数、边缘密度函数等概念给出了连续值命题逻辑系统公式概率真度的定义,明确了概率真度在[0,1]的分布情况,并得到了一些概率真度的推理规则;引入相似度,给出了伪距离的定义,确定了二者之间...
  • 基于条件概率的思想,在连续值命题逻辑系统引入赋值密度函数概念,给出了公式的概率真度、数学期望、条件概率真度的定义,并得到了一些概率真度的推理规则。证明了Lukasiewicz逻辑系统概率真度、条件概率真度在...
  • 利用势为3的非均匀概率空间的无穷乘积,在£ukasiewicz三值命题...利用概率真度定义了概率相似度和伪距离,进而建立了概率逻辑度量空间,证明了该空间没有孤立点,为三值命题的近似推理理论提供了一种可能的框架。
  • 抽象 这项任务是使用解析定理证明者实现自动推理,该定理证明者可用于通过否定证明从命题知识库(KB)进行推论。...在给定条件下,我在“ Sammy.kb”和“ ss.kb”中定义命题逻辑。 Sammy.kb C1Y C2Y C3Y C1
  • 由联结词和多个命题常项可以组成复合命题,若是有联结词和多个命题变项则可以组成命题公式。更具体说,命题公式是由命题常项、命题变项、联结词、...在命题逻辑中命题公式又称合式公式,简称为公式。 命题公式...

    由联结词和多个命题常项可以组成复合命题,若是有联结词和多个命题变项则可以组成命题公式。更具体的说,命题公式是由命题常项、命题变项、联结词、括号组成的特殊符号串,通常用大写字母表示。

    命题公式的严格定义
    1. 单个命题变项p,q,r,...p,q,r,...是命题公式
    2. 多个命题公式通过联结词有限次的组合而成的符号串是命题公式

    在命题逻辑中命题公式又称合式公式,简称为公式。

    命题公式的层次

    命题公式的层次是命题公式的重要概念之一,有利于描述命题公式的求解过程。

    定义:

    1. 若命题公式AA是单个命题常项或命题变项,则称AA是0层公式
    2. 若命题公式AA是有其他命题公式通过联结词组合而成的。设组成AA的所以命题公式中层次最高命题公式的层次为nn,则称AA的层次为n+1n+1
    命题公式的赋值(解释)及真值表

    定义:
    AA为一个命题公式p1,p2,...,pnp_1,p_2,...,p_nAA中出现的所有命题变项,则给p1,p2,...,pnp_1,p_2,...,p_n指定一组真值的行为,称为对AA赋值(解释)。若指定的一组值使AA的值为真,则称这组值为AA成真赋值;若使AA的值为假,则称这组值为AA成假赋值

    一个含有命题变项的命题公式的真值是不确定的,只有对它的每个命题变项都用指定的命题常项代替后,其真值才唯一确定,命题公式也才能被称为一个命题。

    含有nn个命题变项的命题公式共有2n2^n组赋值。
    将命题公式AA在所有赋值之下的取值情况列成表,则称该表为AA的真值表。构造真值表的步骤如下:

    1. 将命题公式中的所有命题变项按从左到右的出现顺序列出(有脚标则按脚标顺序)
    2. 将所有可能赋值赋给命题变项,从00…0开始,每次加1,直到11…1为止(即以二进制渐增的方式赋值)
    3. 对应的每个赋值公式都计算出其命题公式各层次的值

    举例:
    列出命题公式¬(pq)q\lnot (p\to q)\land q的真值表

    pp qq pqp\to q ¬(pq)\lnot (p\to q) ¬(pq)q\lnot (p\to q)\land q
    0 0 1 0 0
    0 1 1 0 0
    1 0 0 1 0
    1 1 1 0 0
    命题公式的分类

    定义:
    AA为一个命题公式

    1. AA在所有赋值下取值均为真,则称AA重言式(永真式)
    2. AA在所有赋值下取值均为假,则称AA矛盾式(永假式)
    3. AA至少存在一组成真赋值,则称AA可满足式

    根据在各种赋值下的取值情况,所有的命题公式都可以分为以上三类。并且根据定义我们可以知道,重言式一定是可满足式,反之不真。

    举例:
    求命题公式(p(pq))q(p\land (p\to q))\to q是哪种类型的命题公式。
    解:画出真值表

    pp qq pqp\to q p(pq)p\land(p\to q) (p(pq))q(p\land (p\to q))\to q
    0 0 1 0 1
    0 1 1 0 1
    1 0 0 0 1
    1 1 1 1 1

    由真值表可知命题公式(p(pq))q(p\land (p\to q))\to q为一个重言式

    真值函数

    定义:
    一个n(n1)n(n\geqslant 1)阶笛卡尔积{0,1}n\{0,1\}^n{0,1}\{0,1\}的函数称为一个nn元真值函数,nn元真值函数FF记为F:{0,1}n{0,1}F:\{0,1\}^n\to \{0,1\}

    nn个命题变项的真值表实际上是给出{0,1}n\{0,1\}^n{0,1}\{0,1\}的一个对应关系,这就是真值函数。nn个命题变项,共有2n2^n个可能的赋值。对于每个赋值,真值函数的函数值非0即1。于是nn个命题变项共可以组成22n2^{2^{n}}个不同的真值函数。其中每一个真值函数都对应一个真值表,同时也对应着无穷个命题公式,这些公式彼此都是等值的,它们中的每一个都是这个真值函数的一个表达式。

    例如,含有两个命题变项p,qp,q的真值函数共有16个函数值。

    pp qq F1F_1 F2F_2 F3F_3 F4F_4 F5F_5 F6F_6 F7F_7 F8F_8
    0 0 0 0 0 0 0 0 0 0
    0 1 0 0 0 0 1 1 1 1
    1 0 0 0 1 1 0 0 1 1
    1 1 0 1 0 1 0 1 0 1
    pp qq F9F_9 F10F_10 F11F_11 F12F_12 F13F_13 F14F_14 F15F_15 F16F_16
    0 0 1 1 1 1 1 1 1
    0 1 0 0 0 0 1 1 1 1
    1 0 0 0 1 1 0 0 1 1
    1 1 0 1 0 1 0 1 0 1
    展开全文
  • del公式概率真度的定义,研究了概率真度的推理规则,在此基础上给出了三种相似度,讨论了其性质及关系,并由此定义了三种伪距离,讨论了逻辑度量空间的结构及其性质,为推理程度的数值化提供了依据。
  • 离散数学命题逻辑连接词解释

    千次阅读 2020-03-06 17:05:19
    在数理逻辑中,复合命题是由原子命题与逻辑联结词组合而成,联结词是复合命题重要组成部分,为了便于书写和进行推演,必须对联结词作出明确规定并符号化。下面介绍各个联结词。 (1)否定 定义1-2.1设p为一命题,p...

    命题逻辑连接词
    在自然语言中,常常使用“或”,“与”,“但是”等一些联结词,对于这种联结词的使用,一般没有很严格的定义,因此有时显得不很确切。在数理逻辑中,复合命题是由原子命题与逻辑联结词组合而成,联结词是复合命题中的重要组成部分,为了便于书写和进行推演,必须对联结词作出明确规定并符号化。下面介绍各个联结词。
    (1)否定
    定义1-2.1设p为一命题,p的否定是一个新的命题,记作┓p.若p为t, ┓p为f;若p为f,┓p为t.联结词"┓"表示命题的否定.否定联结词有时亦可记作"-".

    命题p与其否定┓p的关系如表1-2.1所示.

    表1-2.1
    在这里插入图片描述

    例 用p表示命题“3是素数”
    则┓p即为命题“3不是素数”

    “否定”的意义仅是修改了命题的内容,我们仍把它看作为联结词,它是一个一元运算.

    (2)合取

    定义1-2.2 两个命题p和q的合取是一个复合命题,记作p∧q.,读作“p与q”或“p与q的合取”。当且仅当p、q同时为t时, p∧q为t,在其他情况下, p∧q的真值都是f.。

    联结词"∧"的定义如表1-2.2所示.

    表1-2.2

    合取连接词的含义相当于自然语言中的“p和q”,“p与q”,“p且q,“p,同时q”等。
    命题联结词“合取”也可以将若干个命题联结在一起.

    p表示命题“3是素数”
    q表示命题“7是素数”
    则“3和7都是素数”可以表示为p∧q。
    “合取”是一个二元运算.

    (3)析取

    定义1-2.3 两个命题p和q的析取是一个复合命题,记作p∨q,读作“p或q”或“p,q的析取”。当且仅当p、q同时为f时, p∨q的真值为f,否则p∨q的真值为t.

    联结词“∨”的定义如表1-2.3所示.

    在这里插入图片描述
    表1-2.3

    从析取的定义可以看到,联结词∨与汉语中的“或”的意义也不完全相同,因为汉语中的“或”,可表示“不可兼或”,也可以表示“可兼或”。

    例1 小明在看电视或者吃饭

    在例1中的“或者”为可兼或”。

    例2 小明今天上午十点半在清华大学或者北京大学。

    这个例子中的“或者”字为“不可兼或”。

    (4)条件

    定义1-2.4 给定两个命题p和q,其条件命题是一个复合命题,记作p→q,读作“如果p,那么q”或“若p则q”.当且仅当p的真值为t,q的真值为f时, p→q的真值为f,否则p→q的真值为t.我们称p为前件,q为后件.

    联结词“→”的定义如表1-2.4所示.

    表1-2.4
    在这里插入图片描述

    例1 如果某动物为哺乳动物,则它必胎生.
    例2 因为你是人,所以你是死的
    例3 如果某动物为卵生,则它必定不是哺乳动物

    上述三个例子都可用条件命题p→q表达.

    在数学上和有些逻辑学的书籍中,“若p则q”亦可叫作p蕴含q,而本书在条件命题中将避免使用“蕴含”一词,因为在以后将另外定义“蕴含”这个概念.

    命题联结词“→”亦可记作“é”.条件联结词亦是二远运算.

    (5)双条件

    定义1-2.5 给定两个命题p和q,其复合命题p<=>q称作双条件命题,读作“p当且仅当q”,当p和q的真值相同时, p<=>q的真值为t,否则p<=>q的真值为f.

    联结词”的定义可如表1-2.5所示.

    表1-2.5
    在这里插入图片描述

    这里写图片描述

    两个三角形全等,当且今当它们的三组对应边相等。

    上面的例子可用双条件命题p«q来表示。与前面的联结词一样,双条件命题也可以不顾其因果联系,而只根据联结词定义确定真值。双条件联结词亦可记作“<=>”或”iff“。它亦是二元运算。

    (6)异或
    定义1-2.6给定两个命题p和q,其复合命题p⊕q称作异或命题,读作“p异或q”,当且仅当pq的真值相同是,p⊕q的真值为假。异或词为二元联结词。

    联结词“⊕”的定义如表1-2.6所示

    在这里插入图片描述

    展开全文
  • 连续属性离散化是知识发现研究重要预处理过程,基于最近邻聚类和粗集相关理论,提出一种新有监督多属性离散化方法。该算法分两个阶段来处理,首先利用最近邻聚类动态调整聚类类别数,生成初始聚类。然后...
  • 基于某信息限制下若A则B推理思想,以真度为基础,在二值命题逻辑系统中引入有限信息限制下公式蕴涵度概念,由此定义了信息限制蕴涵度量,并通过...对二值命题逻辑中基于信息限制蕴涵度量近似推理问题进行讨论。
  • 第三章命题逻辑的推理理论 3.1推理形式结构 数理逻辑的主要任务是用数学方法研究推理....定义3.1设A1,A2,...Ak和B都是命题公式,若对于A1,A2,...,Ak和B出现的命题变项任意一组赋值,或者A1^A2^...

    第三章命题逻辑的推理理论

     

    3.1推理的形式结构

     

    数理逻辑的主要任务是用数学的方法研究推理.所谓推理是指从前提出发推出结论的思维过程,而前提是已知的命题公式集合,结论是从前提出发应用推理规则推出的命题公式.为此, 首先应该明确什么样的推理是正确的.

    定义3.1设A1,A2,...Ak和B都是命题公式,若对于A1,A2,...,Ak和B中出现的命题变项的任意一组赋值,或者A1^A2^…^Ak为假,或者当A1^A2^…^Ak为真时B也为真,则称由前提A1,A2,…,Ak推出结论B的推理是有效的或正确的,并称B是有效的结论.

    关于定义3.1还需做以下几点说明

    1. 由前提A1,A2,…,Ak推结论B的推理是否正确与诸前提的排列次序无关,前提是一个有限的公式集合.设前提为集合Γ,将由Γ推B的推理记为Γ├B.若推理是正确的,则记为Γ╞ B,否则记为|≠B.这里称├B或{A1,A2,…,Ak}├B为推理的形式结构
    2. 设A1,A2,...,Ak,B中共出现n个命题变项,对于任一组赋值α1α2…αn(αi=0或1,i=1,2,…,n),前提和结论的取值情况有以下4种
    1. A1^A2^...Ak为0,B为0;
    2. A1^A2^...Ak为0,B为1;
    3. A1^A2^...Ak为1,B为0;
    4. A1^A2^...Ak为1,B为1;

    由定义3.1可知,只要不出现情况(3),推理就是正确的,因而判断推理是否正确,就是判断是否会出现情况(3)

    1. 由上面的讨论可知,推理正确并不能保证结论B一定成立,因为前提可能就不成立.这与人们通常对推理的理解是不同的,通常只能认为在正确的前提下推出正确的结论才是正确的.而在这里,如果前提不正确,不论结论正确与否,都说推理正确

    例3.1判断下列推理是否正确

    1. Ip,p→ql├q
    2. Ip,q→pl├q

    解:写出前提的合取式与结论的真值表,看是否出现前提合取式为真,而结论为假的情况

    1. 由表3.1,没有出现前提合取式为真,结论为假的情况,因而推理正确,即{p,p→q}|=q
    2. 由表3.1,当赋值为10时,前提的合取式为真,而结论为假,因而推理不正确,即{p,g→p}|≠q

     

    对于例3.1中这样简单的推理,不难通过直接观察判断推理是否正确。如在(1)中,当q为假时,无论p是真还是假,P^(q→p)均为假,因而不会出现前提合取式为真,结论为假的情况,故推理正确.而在(2)中,当q为假,P为真时,出现了前提合取式为真,结论为假的情况,因而推理不正确

    下面给出推理形式结构另一种等价的形式,为此,首先证明下面定理

    定理3.1命题公式A1,A2,…,Ak推B的推理正确当且仅当A1^A2^…^Ak→B为重言式

     必要性,若A1,A2,…,A,推B的推理正确,则对于A1,A2,…,Ak和B中所含命题变项的任意一组赋值,不会出现A1^A2^…^Ak为真且B为假的情况,因而在任何赋值下,蕴涵式A1^A2^…^Ak→B均为真,故它为重言式

    充分性,若蕴涵式A1^A2^…^A→B为重言式,则对于任何赋值此蕴涵式均为真,因而不会出现前件为真后件为假的情况,即在任何赋值下,或者A1^A2^…^A4为假,或者A1^A2^…^Ak和B同时为真,故A1,A2,...,Ak推B的推理正确

    由定理3.1,由前提A1,A2,…,Ak推B的推理的形式结构

    {A1,A2,...,Ak}|-B (3.1)

    等同于蕴涵式

    A1^A2^…^A→B (3.2)

    其中推理前提的合取式成了蕴涵式的前件,结论成了蕴涵式的后件.推理正确

    {A1,A2,...,Ak}|=B (3.3)

    等同于

    A1^A2^…^A=>B (3.4)

    其中=>同<=>个样是一种元语言符号,表示蕴涵式为重言式。

    今后把推理的形式结构写成:

    前提:A1,A2,...,Ak

    结论:B

    并且也把(3.2)式称作推理的形式结构,通过判断(3.2)式是否为重言式来确定推理是否正确.根据前2章的讨论,判断(3.2)式是否为重言式有下面3种方法

    1. 真值表法
    2. 等值演算法
    3. 主析取范式法

    现在可以将例3.1中的两个推理写成(3.5)的形式

    (1)

    前提:p,P→q

    结论:q

    推理的形式结构:(p^(P→q))→q

    (2)

    前提:p,q→q

    结论:q

    推理的形式结构:(p^(q→p))→q

    由例3.1已知,(1)正确,即(p^(p→q))→q;而(2)不正确,记为(P^(q→p))≠>q.

    例3.2判断下面推理是否正确

    1. 若a能被4整除,则a能被2整除,a能被4整除.所以,a能被2整除
    2. 若a能被4整除,则a能被2整除,a能被2整除.所以,a能被4整除
    3. 下午马芳或去看电影或去游泳,她没去看电影.所以,她去游泳了
    4. 若下午气温超过30℃,则王小燕必去游泳,若她去游泳,她就不去看电影了.所以,若王燕没去看电影,下午气温必超计了30℃

     解上述类型的推理问题,首先应将简单命题符号化,然后分别写出前提、结论、推理的形式结构,接着进行判断

    1. 设p:a能被4整除

    q:a能被2整除

    前提:p→q,p

    结论:q

    推理的形式结构:(p→q)^P→p (3.6)

    由例3此推理正确,即(p→q)^p=>p

    1. 设p,q的含义同(1)

    前提:p->q,q

    结论:p

    推理的形式结构:(p→q)^q→p (3.7)

    当然可用真值表法、等值演算、主析取范式等方法来判断(3.7)式是否为重言式,但在此推理中,容易看出,01是(3.7)式的成假赋值,所以此推理不正确

    p:马芳下午去看电影

    q:马芳下午去游泳

    前提:pVq,┓p

    结论:q

    推理的形式结构:((pVq)^┓p)→p (3.8)

    用等值演算法来判断(3.8)式是否为重言式

    ((pVq)^┓p)->q

    <=>((p^┓p)V(q^┓p))→q

    <=>(qA┓p)->q

    <=>┓qVPVq

    <=>1

    得证(3.8)式为重言式,所以推理正确

    p:下午气温超过30℃

    q:王小燕去游泳

    r:王小燕去看电影

    前提:p→q,q→┓r

    结论:┓r->p

    推理的形式结构:((p→q)^(q→┓r)→(┓r→p)

    用主析取范式法判(39)式是否为重言式

    ((p→q)^(q→┓r)→(┓r→p)

    <=>┓((┓pVq)^(┓V┓r))V(rVp)

    <=>((p∧q)V(q∧r))v(rVp)

    <=>pVr (用两次吸收律)

    <=>(p∧┓q∧┓r)V(P^┓q^r)V(p^q^┓r)

    ( p^q^r)V(┓p∧┓q^r)V(┓p^q∧r)

    V(P∧┓q∧r)V(P^q∧r)

    <=> m1,Vm3 Vm4Vm6 Vm7 (重排了序)

    可见(3.9)式不是重言式(主析取范式中缺2个极小项m0和m2),所以推理不正确

    有一些重要的重言蕴涵式,称为推理定律.下面给出9条推理定律,它们是:

     

    其中A,B,C,D等是元语言符号,表示任意的命题公式

    把具体的命题公式代入某条推理定律后就得到这条推理定律的一个代人实例.例如p=>pVq,p→q=>(p→q)Vr,p=> pvqvr等都是附加定律的代入实例,推理定律的毎一个代人实例都是重言式,可以使用这些推理定律证明推理正确.在下一节将看到,由这9条推理定律产生9条推理规则,构成一个推理系统中的推理规则集

    除上述9条推理定律外,2.1节给出的24个等值式中的每一个都能产生出两条推理定律例如,双重否定律A<=>┓┓A产生两条推理定律A=>┓┓A和┓┓A=>A.

     

     

    展开全文
  • 也提供一套形式化语言,可编写数学算法、定义、定理;它还可以用于程序正确性证明。 2、Coq安装 Coq-8.11.0 安装包【Windows、MacOS】 链接:https://pan.baidu.com/s/1rAjW8D6G5GJI3sQP1JfG7g...

    一、Coq的安装与使用

    1、Coq简介

            Coq是一款交互式证明辅助工具,提供一套证明系统,可以编写证明、检查证明;也提供一套形式化语言,可编写数学算法、定义、定理;它还可以用于程序的正确性证明。

    2、Coq的安装

    Coq-8.11.0 安装包【Windows、MacOS】

    链接:https://pan.baidu.com/s/1rAjW8D6G5GJI3sQP1JfG7g 
    提取码:ects

    安装完成之后,Coq自带CoqIde,对于形式化方法课程来说应该是够用了。

    【我有尝试使用另外一种IDE:Proof General,但是没有成功,等成功之后再来更新吧,目前就先用CoqIde了hhhh】

    3、Warm-up Test

    (1)创建一个名为 coq_warm_up.v 的文件,保存如下代码:

    【其中 “.v” 是Coq文件的默认后缀】

    Inductive day : Type := 
    | monday : day 
    | tuesday : day 
    | wednesday : day 
    | thursday : day 
    | friday : day 
    | saturday : day 
    | sunday : day. 
    
    Definition next_weekday (d:day) : day := 
    match d with 
    | monday => tuesday 
    | tuesday => wednesday 
    | wednesday => thursday 
    | thursday => friday 
    | friday => monday 
    | saturday => monday 
    | sunday => monday 
    end.
    
    Eval compute in (next_weekday friday). 
    Eval compute in (next_weekday (next_weekday saturday)). 

    (2)运行CoqIde,打开上述文件;

    (3)单击 Go to end 按钮,会得到如下的输出:

         = monday
         : day
         = tuesday
         : day

    此时说明Coq安装成功。

    4、Coq功能分区

    • Tool bar 工具栏:提供可执行的基本命令。
    • Script buffers 脚本缓冲区:用于打开和编辑脚本。
    • Goal window 目标窗口:显示待验证目标。
    • Message window 消息窗口

    二、Coq Tactics——如果使用Coq进行proof development

    在proof development的每个阶段,都有一个要证明的子目标列表。

    最初,该列表由所要证明的新定理的本身组成;

    应用某些策略之后,目标列表包含该策略生成的子目标,接下来的工作就是分别对这些子目标进行处理。

     

    主要包括以下策略:intros, apply, inversion, split, right and left

     

    A basic theorem:

    Theorem ident body: type.
    Proof.
        Tactics
    Qed.
    • Theorem - Coq中的一个命令,声明了一个需要证明的新定理;

    • ident - 新定理的名称;

    • body - 新定理的主体;

    • type - 

            forall 新定理中出现的变量名(多个变量用空格隔开):Prop,

                所要证明的新定理.

    • Proof - 标示着证明新定理的开始

    • Tactics - 指导证明的过程,在结论和前提之间提出演绎规则,实现反向推理

    • Qed - 标示着证明新定理的完成

     

    1、Implication(蕴含):intros and apply tactic

    【蕴含的引入规则:intros】

    主要用于拆分所要证明定理中的已知前提和所要证明的结论。【详见下方】

     

    【蕴含的删除规则:apply】

    【详见下方】

     

    第一个栗子:证明定理 P -> P成立

    证明代码如下:

    Theorem example1: forall P: Prop, 
        P -> P.
    Proof.
        intros.
        apply H.
    Qed.
    

    分析解释如下:

    (1)执行前三行,结果如下:

    由goal-window展示的结果可知,我们的证明目标位于水平线的下方。

    横线上方没有任何的内容,表示 local context 为空,没有任何东西可以使用。

    (2)执行intros策略:

    基于当前目标,intros策略具有不同的效果,如果是:

    forall T: type, T-> U    

    将 T: type 和 Hn: T 放入 local context,新的子目标就是U。

    执行intros策略后,根据横线上方的内容,local context 中有两个前提可供使用。

    (3)执行apply H:

    在步骤(2)中,我们得到了一个名为H的假设,并且该假设的值与我们唯一的子目标相同,当我们得出与目标相同的假设时,使用 apply 策略。

    (4)使用Qed命令完成证明:

    当goal-window显示“No more subgoals”,表示证明过程结束,使用Qed命令完成证明,该命令可以让Qed保存定理及其证明。

    相关练习:证明定理 P -> (Q -> P) 成立

    Theorem exercise1: forall P Q:Prop,
        P -> (Q -> P).
    Proof.
        intros.
        apply H.
    Qed.

    (1)前三行:

    (2)第四行:

    此时发现子目标P和前提H相同,因此直接apply H即可。

    (3)第五行:

     

    第二个栗子:证明定理 (P -> Q) -> P -> Q 成立

    证明代码如下:

    Theorem example2: forall P Q: Prop,
        (P -> Q) -> P -> Q.
    Proof.
        intros.
        apply H in H0.
        apply H0.
    Qed.

    分析解释如下:

    (1)执行前三行:

    (2)执行第四行:

    在local context中得到了两个假设,但是都和子目标不相同时:

    如果我们知道: (a) x implies y,并且 (b) x 为真 时,我们可以使用 apply (a) in (b) 策略将(b)中的 x 转换为 y。

    在本例中,

    H: P -> Q   

    H0: P 

     

    由H可知,P implies Q,并且由H0可知,P为真,因此我们可以使用:

    apply H in H0

    将H0转换为Q。

    即:将假设 H: P -> Q 应用于假设 H0: P,将假设H0变为Q。

    (3)执行第五行:

    此时前提H0和子目标Q相同,apply H0 即可。

    (4)执行第六行:

    证毕。

    相关练习:证明 P -> (Q -> ( H -> Q )) 成立

    代码如下:

    Theorem exercise2: forall P Q H:Prop,
       P -> (Q -> (H -> Q)).
    Proof.
        intros.
        apply H1.
    Qed.

     

    2、Conjunction(合取、交):inversion(反演) and split(拆分) tactic

    【合取的】

     

    【合取的引入规则】

    在Coq中使用这个命令就是将结论拆分成两个来证明,两个都需要进行证明。

     

    第一个栗子:证明 P /\ Q -> Q 成立

    证明代码如下:

    Theorem example3: forall P Q: Prop,
        P/\Q -> Q.
    Proof.
        intros.
        inversion H.
        apply H1.
    Qed.

    分析解释如下:

    (1)执行前三行:

    (2)执行第四行:

    【 inversion 策略 用法一】

    inversion 策略用于证明具有 conjuction(合取、交)连接的定理。

    执行完第四行之后,我们得到了一个假设 H: P /\ Q,其中具有合取运算符。

    inversion 策略主要用于发现假设成立的前提。

    有假设H可知,P /\ Q为真,只有在 P 为真并且 Q 为真的情况下,P /\ Q 才可能为真,因此我们可以使用 Inversion 策略向 local context 中添加两个假设—— H0: P  H1: Q。

    (3)执行第五行:

    此时假设H1和子目标相同,因此只需要 apply H1 即可。

    (4)执行第六行:

    相关练习:证明 P /\ Q ->P 成立

    代码如下:

    Theorem exercise3: forall P Q: Prop,
        P /\ Q -> P.
    Proof.
        intros.
        inversion H.
        apply H0.
    Qed.

     

    第二个栗子:证明 (P /\ Q) -> (Q /\ P)

    证明代码如下:

    Theorem example4: forall P Q:Prop,
        (P /\ Q) -> (Q /\ P).
    Proof.
        intros.
        inversion H.
        split.
        apply H1.
        apply H0.
    Qed.

    分析解释如下:

    (1)执行前三行:

    (2)执行第四行:

    假设中包含合取运算符,因此使用 Inversion 策略。

    (3)执行第五行:

    我们需要证明的目标是 Q /\ P 成立,显然 Q /\ P 成立的条件是 Q 和 P 都为真,因此我们可以将目标拆分。

    split 策略用于将目标拆分成几个子目标,然后再对子目标进行一一证明。

    (3)执行第六行:

    首先证明子目标Q,直接 apply H1 即可

    (7)执行第七行:

    再证明剩余的一个子目标P,apply H0

    (8)执行第八行:

    相关练习:证明 (P /\ (Q /\ R)) -> ((P /\ Q) /\ R) 成立

    Theorem exercise4: forall P Q R:Prop,
        (P /\ (Q /\ R)) -> ((P /\ Q) /\ R).
    Proof.
        intros.
        inversion H.
        inversion H1.
        split.
        split.
        apply H0.
        apply H2.
        apply H3.
    Qed.

     

    3、Disjunction(析取,并): right and left tactic

    【析取的引入规则 left & right】

    对目标结论输入 left,能够使得目标变成 P;同理对目标结论输入 right,能够使得目标变成 Q。

    在实际操作时,选择一个证明起来比较简单的式子。

     

    第一个栗子:证明 (P \/ Q) -> (Q \/ P) 成立

    证明代码如下:

    Theorem example5: forall P Q: Prop,
        (P \/ Q) -> (Q \/ P).
    Proof.
        intros.
        inversion H.
        right.
        apply H0.
        left.
        apply H0.
    Qed.

    分析解释如下:

    (1)执行前三行:

    (2)执行第四行:

    【 inversion 策略 用法二】

    inversion 策略还可用于具有 disjunction(合取、并)连接的定理,生成两个具有相同结论、但 local context 中H0值不同的子目标。

    (3)执行第五行:

    第一个子目标需要我们在假设 H0: P 成立的前提下,证明 Q \/ P 为真,因此许需要证明 Q 为真或者 P 为真 或者 Q 和 P 均为真即可。

    前提为 H0: P,需要证明的子目标 Q \/ P 中包含 P,且 P 位于合取符号的右侧,因此,使用 right 策略使得子目标与假设 H0 相同。

    (4)执行第六行:

    此时 前提 H0 与第一个子目标相同,因此只需要 apply H0 即可。

    (5)执行第七行:

    需要证明的目标为:在 H0: Q 成立的前提下,证明 Q \/ P 为真,Q 位于合取符号的左侧,因此使用 left 策略使得目标与假设 H0 相同。

    (6)执行第八行:

    (7)执行第九行:

    相关练习:证明 (P \/ (Q \/ R)) -> ((P \/ Q) \/ R) 成立

    代码如下:

    Theorem exercise5: forall P Q R:Prop,
        (P \/ (Q \/ R)) -> ((P \/ Q) \/ R).
    Proof.
        intros.
        inversion H.
        left.
        left.
        apply H0.
        inversion H0.
        left.
        right.
        apply H1.
        right.
        apply H1.
    Qed.

     

    4、not(~):unfold 策略

    【使用场景】

    当我们想要展开某个定义或者函数实现时,使用 unfold 策略。

    当我们想要将 ~X 转换为 X -> False 时,使用 unfold 策略,有两种实现方法:

    (1)unfold not

    (2)unfold "~"

     

    举个栗子:证明 P -> ~P -> Q 成立。

    证明代码如下:

    Theorem absurd: forall P Q:Prop,
        P -> ~P -> Q.
    Proof.
        unfold not.
        intros.
        elim H0.
        apply H.
    Qed.

    (1)执行前三行代码:

    使用 unfold not 将 ~Q 转换为 Q -> False。

    (2)执行第四行代码:

    elim 策略用于消除谬误。

    (3)执行第五行代码:

    (4)执行第七行代码:

    练习:

    证明 ((P -> R) /\ (Q -> R)) -> (P /\ Q -> R) 成立。

    Theorem exercise6: forall P Q R:Prop,
        ((P -> R) /\ (Q -> R)) -> (P /\ Q -> R).
    Proof.
        intros.
        inversion H0.
        inversion H.
        apply H3 in H1.
        apply H1.
    Qed.

     

    证明 (P -> Q /\ R) -> ((P -> Q) /\ (P -> R)) 成立。

    Theorem exercise7: forall P Q R:Prop,   
        (P -> Q /\ R) -> ((P -> Q) /\ (P -> R)).
    Proof.
        intros.
        split.
        apply H.
        apply H.
    Qed.

     

    证明  ((P /\ Q) /\ R, S /\ T) -> (Q /\ S) 成立。

    Theorem challenge1: forall P Q R S T:Prop,
        (((P /\ Q) /\ R) /\ (S /\ T)) -> (Q /\ S).
    Proof.
        intros.
        inversion H.
        inversion H0.
        inversion H2.
        inversion H1.
        split.
        apply H5.
        apply H6.
    Qed.

     

    证明 (P -> Q) -> (~Q -> ~P) 成立。

    证明代码如下:

    Theorem challenge2: forall P Q:Prop,
        (P -> Q) -> (~Q -> ~P).
    Proof.
        unfold not.
        intros.
        apply H in H1.
        apply H0 in H1.
        apply H1.
    Qed.

    (1)执行前三行代码:

    (2)执行第四行:

    (3)执行第五行:

    (4)执行第六行:

    (5)执行第七行:

    (6)执行第八行:

     

    参考:

    https://www.cnblogs.com/luluathena/archive/2010/08/19/1803065.html

    http://www.doc88.com/p-5187845230295.html

    https://zhuanlan.zhihu.com/p/33294417?edition=yidianzixun

    展开全文
  • 命题逻辑中包含了对字符串一系列操作,命题逻辑完备性是指在逻辑语义上任意重言式(即定理)一定可以被字符串操作表示出来。 定义 字符集: {¬,→,(,),p1,p2,p3,⋯ }\{\neg,\rightarrow,(,),p_1,p_2,p_3,\...
  • Natural Logic Interpreter根据推理规则和命题逻辑自动解释和验证嵌套自然逻辑论证(以自然语言表达的逻辑论证)。 该程序使用递归函数实现“分而治之”算法来遍历嵌套的逻辑参数,并能够相应地定义和验证它们。...
  • 命题13-命题21是逻辑命题的延续,逻辑加与包含关系融汇其中,我们按照片断的顺序,开始命题13-21的理解。 命题13:如果L⊕B=L,那么B在L。 如果任意词项附加到另一个词项,并不改变另一个词项,那么,这个所附加...
  • (1)定义3.1:设A1,A2,A3...Ak和B都是命题公式,若对于A1,A2,A3...Ak和B出现的命题变项任意一组赋值,或者A1,A2,A3...Ak为假,或者当A1,A2,A3...Ak为真是,B也为真,则称由前提A1,A2,A3...Ak推出结论...
  • 在二值命题逻辑系统引入了公式T-真度概念,并讨论其逻辑运算性质。以此为基础定义了公式T-相似度和T-伪距离,得到了公式到有限理论结论集T-伪距离T-真度表示式,为研究二值命题逻辑系统基于T-真度近似...
  • 在n值Lukasiewicz命题逻辑系统引入了公式集F(S)上真度函数公理化定义,给出了真度函数若干重要性质,利用真度函数从形式上定义了相似度和伪距离,建立了逻辑度量空间,为从语构角度展开近似推理提供了一种...
  • 基本逻辑思维(命题,语言) 语言: 在数学、计算机科学和语言学,形式语言是必不可少一组符号串。 程序设计语言: 一种设计用来向机器传达指令以控制其行为语言。 关于情境推理包括复杂句子和自然语言...
  • 推理的定义:从一组前提合乎逻辑地推出结果的思维过程。 比如我们有一堆叫做G1,G2...GnG_1,G_2...G_nG1​,G2​...Gn​的前提,在这些前提均成立的情况下,我们可以得到一个叫做HHH的结论,这就叫做推理。类似于生活...
  • 第一章 命题逻辑 1.5联结词完备集

    千次阅读 2019-08-01 20:28:05
    我们知道一个有两个命题变元p,q构成的命题公式p,q组合真值情况有4种,而每种所对应FiF_iFi​都有0,1两种情况。所以共有424^242=16种情况。如图: 有些版本异或也表示为⊕,清...
  • 在添加了[Δ]算子Gödeln值命题逻辑系统,给出了Gödel[n]值命题逻辑系统有限理论的平均真度的定义,给出了该系统下的一些重要结论并给予证明,验证了在该系统下平均真度的一些基本性质,为进一步在该系统下研究...
  • 第一章 命题逻辑 1-2联结词 P Q ¬P P∧Q P∨Q P→Q P⇄Q T T ...定义命题公式,对于分量指派真值各种可能组合,就确定了这个命题公式各种真值情况,把它汇成列表,就是命题公式

空空如也

空空如也

1 2 3 4 5 ... 9
收藏数 169
精华内容 67
关键字:

逻辑中命题的定义