公理系统

摘要： 定理证明是目前主流的形式化验证方法,拥有强大的抽象和逻辑表达能力,且不存在状态空间爆炸问题,可用于有穷和无穷状态系统,但其不能完全自动化,并且要求用户掌握较强的数学知识.含索引式的命题投影时序逻辑(PPTL)是一种具有完全正则表达能力,并且包含LTL的时序逻辑,具有较强的建模和性质描述能力.目前,一个可靠完备的含索引式的PPTL公理系统已被构建,然而基于该公理系统的定理证明尚未得到良好工具的支持,存在证明自动化程度较低以及证明冗长易错的问题.鉴于此,首先设计了支持索引式的PPTL定理证明器的实现框架,包括公理系统的形式化与交互式定理证明;然后,在Coq中形式化定义了含索引式的PPTL公式、公理与推理规则,完成了框架中公理系统的实现;最后,通过两个实例的交互式证明验证了该定理证明器的可用性.

摘要： 自从波兰数学家Z.Pawlak建立信息表的逻辑系统以来,出现了各种信息系统及其逻辑的研究。集值信息系统在机器学习方面有着重要的应用,本文从一个具体的集值信息系统的例子引发出建立集值信息系统的公理系统必要性。首先借助相容性关系给出模态算子的语义;然后给出集值信息系统的逻辑的语法和语义;最后建立集值信息系统的公理系统的公理和推理规则,并且利用传统方法证明集值信息系统的逻辑系统的可靠性和完全性。从逻辑本质上看,集值信息系统的逻辑系统就是一种多模态逻辑系统,它也给出多模态逻辑的非常完美的诠释。

摘要： 本文用一个具体的有趣的折纸活动与问题提出系列,以折纸抛物线为载体,展示了折纸几何与解析几何的关系.折纸几何可以理解为某种形式的"直观几何",虽然人们已经清楚了折纸几何的公理系统,但其直观性依然令人追随,直观导致理解,直观导致发现,解析几何则通过方程与计算精确地呈现几何对象及其关系.

摘要： 1899年,希尔伯特发表了著名的《几何基础》一书,第一次给出了完备的欧几里得几何公理系统,精确地提出了公理系统的相容性、独立性与完备性要求.20世纪初,为了消除朴素集合论悖论,构建坚实的数学基础,以希尔伯特为代表的的形式主义学派于1922年提出了著名的"希尔伯特纲领",即一个使数学中永远消除悖论的方案.希尔伯特的基本思路是:(1)先把古典数学的内容公理化,进而形式化,使之成为用形式符号和符号序列组成的系统,并用TF表示.

摘要： 18世纪的朝鲜是内部实学思潮和外界西洋文学肆无忌惮地刺激传统学术秩序的时期,这一现象在艺术领域也不例外.同时,燕行,即在北京的旅行,对建立这种新学术和文化生态起了极大的刺激.本文将重点放在以实学研究为基础的燕行者如何运用自然科学知识分析西方美术,从而展示18世纪朝鲜自然科学和艺术相关的一面.

摘要： 敌友逻辑(van der Hoek,et al.,2018)采用结构平衡理论的视角对社会网络的动态变化进行了刻画.在一个稳定的社会网络中,主体之间没有理由改变当下的关系,而不稳定网络则通常会向稳定网络演进.敌友逻辑基于分支时间逻辑CTL,其中每条时间线表示网络的一个演进过程.本文前半部分探讨敌友逻辑的可靠且完全的公理系统.敌友逻辑的模型检测、有效性和可满足性检测问题的计算复杂性已知都是PSPACE完全的.本文后半部分介绍敌友逻辑模型检测的程序实现.

摘要： 张清宇先生在20世纪90年代创建了不用联结词的逻辑系统,在其中使用括号表达命题联结词和量词的功能,这是一项逻辑符号技术的创新性工作.波兰表示法和括号表示法是逻辑符号表示法的两个相互映衬的典范.在括号表示法中,“不用联结词”指的仅仅是语形层面上的,而不是语义层面上的.基于括号表示法的命题逻辑公理系统H和一阶逻辑系统QH都可以进一步简化.

摘要： 张清宇先生在20世纪90年代创建了不用联结词的逻辑系统,在其中使用括号表达命题联结词和量词的功能,这是一项逻辑符号技术的创新性工作。波兰表示法和括号表示法是逻辑符号表示法的两个相互映衬的典范。在括号表示法中,“不用联结词”指的仅仅是语形层面上的,而不是语义层面上的。基于括号表示法的命题逻辑公理系统H和一阶逻辑系统QH都可以进一步简化。

摘要： 本文通过对数学公理的属性与法律原则的特性、数学公理系统与法律原则系统、数学公理化方法与法律逻辑推理之间的比较分析,提出数学公理对于法律原则的完善具有重要的借鉴价值.

摘要： 1975年,Goodenough和Gerhart在研究软件测试能否保证软件的正确性时首次提出了软件测试理论的中心问题是软件测试充分性问题,即如何确定一个软件测试充分性准则来指出测试到何种程度是充分的。软件可靠性测试也面临同样的问题。迄今为止,人们已经提出了许多软件测试充分性准则,并试图对比各种准则的优劣,但结果一直不令人满意。80 年代中期,人们开始对软件测试充分性准则进行公理化研究,充分性准则公理系统被认为是对软件测试充分性准则所具有的一般性质的刻划和描述,但尚没有一种被公认为是揭示了软件测试充分性的基本性质的,因此对于这些“公理系统”定义的性质能否被视为公理,人们尚未达成共识。基于对原有测试充分性准则的公理系统进行的分析和形式化阐述,文章对软件可靠性测试充分性准则进行了公理化的研究,并对结果进行了分析。在研究过程中,提出了对于原有测试充分性准则公理系统的改进建议。

摘要： 如今的CPU结构十分复杂,传统的测试、模拟等验证方法无法完全保证CPU结构设计的正确性.针对CPU结构设计的正确性验证问题,本文基于CPU结构模型建立了CPU结构公理系统,提出了在此公理系统上进行定理证明的形式化方法,开发了自动验证工具,并对MIPS指令集上的CPU结构设计进行了验证.

摘要： 以罗伯特·范·罗伊的工作为基础，本文展示如何通过形式化的方法把三段论逻辑扩充到全部命题逻辑。文中将依次给出按现代逻辑标准形式化的三个逻辑：亚里土多德的三段论逻辑SYL，引入否定词项等之后的扩充系统，最终得到从三段论逻辑扩充而来的命题逻辑。

摘要： 以罗伯特·范·罗伊的工作为基础，本文展示如何通过形式化的方法把三段论逻辑扩充到全部命题逻辑。文中将依次给出按现代逻辑标准形式化的三个逻辑：亚里土多德的三段论逻辑SYL，引入否定词项等之后的扩充系统，最终得到从三段论逻辑扩充而来的命题逻辑。

摘要： 以罗伯特·范·罗伊的工作为基础，本文展示如何通过形式化的方法把三段论逻辑扩充到全部命题逻辑。文中将依次给出按现代逻辑标准形式化的三个逻辑：亚里土多德的三段论逻辑SYL，引入否定词项等之后的扩充系统，最终得到从三段论逻辑扩充而来的命题逻辑。

摘要： 以罗伯特·范·罗伊的工作为基础，本文展示如何通过形式化的方法把三段论逻辑扩充到全部命题逻辑。文中将依次给出按现代逻辑标准形式化的三个逻辑：亚里土多德的三段论逻辑SYL，引入否定词项等之后的扩充系统，最终得到从三段论逻辑扩充而来的命题逻辑。

摘要： 本发明提供了一种基于公理设计的植介入医疗器械关键参数提取及评价方法，所述评价方法从待评价的植介入医疗器械具体临床使用目的与植入位置的解剖结构约束出发，在用户域中定义其用户需求，在功能域中对包括生物力学性能、材料学性能、生物学性能在内的各项性能与结构设计参数、材料设计参数进行分解细化，并形成伦理学约束。通过力学测试、材料学测试与生物相容性测试等测试方法得出不同设计参数影响下植介入医疗器械各项性能指标的变化情况，在此基础上得到能够定量反映植介入医疗器械设计参数和性能二者之间变化关系的设计矩阵，从信息量与耦合度的角度对植介入医疗器械的设计进行评价，评价结果可以为植介入医疗器械设计的优化提供依据。

摘要： 本发明设计了一种基于公理设计理论的产品绿色配置方法，属于机械设计自动化领域。本发明方法是基于公理设计理论，根据其中的独立公理，筛选满足功能需求的各个功能模块；然后根据各个模块的绿色性能及其功能权重，筛选满足绿色性能需求的产品配置方案；最后基于公理设计理论的信息公理，计算符合条件的产品配置方案的信息量，挑选最佳产品配置方案。利用该方法进行产品绿色配置，可以快速、有效的配置出既满足功能需求又满足绿色性能需求的产品。

摘要： 本发明公开了基于绿色办公理念的滑动门移动系统，包括工作箱，所述工作箱左右端面对称滑动连接有一滑门机构，所述工作箱上侧设置有一顶块，所述顶块下端面内设置有一下端壁连通外界空间的顶部滑动槽，所述工作箱下侧设置有一底板，所述底板上端面内设置有一上端壁连通外界空间的底部滑动槽，所述工作箱上端面贯穿顶部滑动槽下端壁且位于顶部滑动槽内，所述工作箱上端内设置有一上端壁连通顶部滑动槽的工作空间。此装置结构简单，操作便捷，将滑动门变成了一种纯靠机械机械操作的门，去除了人力移动滑动门的不稳定性，增加了安全性，并且在电机故障时还能转化成普通滑动门来使用，避免了突发情况时被困。

摘要： 本发明公开了一种基于公理化的油田套管失效信息系统的设计方法，包括步骤：(a)首先，定义知识库中信息系统的功能要求；(b)然后，通过识别设计参数把功能域的FRs映射到结构域；(c)选择最佳设计；(d)软件模块的分解；(e)面向对象的编程和页面模块；(f)构建软件系统的结构。本发明能快速完成基于公理化的油田套管失效信息系统的设计，且设计步骤简单，设计结果准确，大大降低了设计成本。

摘要： 本发明公开了一种基于公理设计下的系统设计方法，包括步骤：(a)首先，确定用户域中系统必须满足的消费者的需求CAs及其属性，然后再在功能域中确定系统满足CAs的FRs及其这些FRs的约束条件Cs；(b)然后，域间映射；(c)接着，系统设计中的功能的独立性；(d)最佳设计；(e)定义模块；(f)分解；(g)系统结构的表征。本发明能快速完成基于公理设计下的系统设计，且设计步骤简单，设计方法准确，大大降低了分析设计成本。

摘要： 本发明涉及一种基于公理解释的类激活映射方法及装置。首先将电气设备图像输入至已训练好的CNN模型，并提取模型中目标卷积层的特征图，同时获取目标类别分数，利用反向传播计算特征图相对于分数的梯度并对其优化处理，将优化后的梯度进行全局平均池化操作得到权重，最后将权重与特征图线性结合，并进行上采样和归一化操作得到初始类激活图；将得到的初始类激活图与输入图像点乘，对点乘后的图像进行平滑操作后再送入模型，经过softmax操作后生成N个分数，最终平均到一个分数；最后将得到的分数与初始类激活图相乘，ReLU操作后得到最后的类激活图。利用本发明生成的类激活图在清晰度、对象定位等方面有更好的视觉解释。

摘要： 本发明属于知识图谱的表示学习和本体构建的技术领域，具体涉及一种基于线性规划的本体包含公理学习方法，包括构建表示学习模型SetE，将知识图谱Abox的实体数据、类型数据及关系数据输入表示学习模型SetE，计算类型数据之间的包含关系，提取包含关系形成公理。本发明可以用线性表示学习模型来捕捉谓词特征，并且通过把包含关系归纳和约简成线性规划来获得本体包含关系，对于知识图谱不完整的情况下仍然可以高效地学习出相应的本体。

摘要： 本发明公开了一种基于公理化模糊集的不同语义的表情识别方法，具体包括以下步骤：步骤1，根据类内的相似性和类之间的差异，为每个表情构造语义概念集；步骤2，提取人脸特征信息并转化为语义概念；步骤3，将语义概念制作成对应的规则集，用来区分表情的类别；步骤4，提出优化准则，用于为每个表情选择最适合的语义概念。本申请能客观地将人脸特征转化为语义概念，模糊集及其逻辑运算是根据原始数据的分布和模糊集的语义在算法上确定的。通过考虑模糊性和随机性，促进了如何将数据库中的信息转换为隶属函数及其模糊逻辑运算的研究。本申请不需要定义隶属函数和初始值，因为所有数据都是从原始数据库中获得的。

摘要： 本发明提供了一种基于公理设计的植介入医疗器械关键参数提取及评价方法，所述评价方法从待评价的植介入医疗器械具体临床使用目的与植入位置的解剖结构约束出发，在用户域中定义其用户需求，在功能域中对包括生物力学性能、材料学性能、生物学性能在内的各项性能与结构设计参数、材料设计参数进行分解细化，并形成伦理学约束。通过力学测试、材料学测试与生物相容性测试等测试方法得出不同设计参数影响下植介入医疗器械各项性能指标的变化情况，在此基础上得到能够定量反映植介入医疗器械设计参数和性能二者之间变化关系的设计矩阵，从信息量与耦合度的角度对植介入医疗器械的设计进行评价，评价结果可以为植介入医疗器械设计的优化提供依据。

摘要： 提供一种关于演示线段公理性质的趣味滚动装置，具有支架、竖板、卡通动物模板，竖板正面下端设有的开口盒子，开口盒子内放置两个一模一样的小球，竖板正面左侧设有用纸质口杯制成的直线段通道；竖板正面右侧设有用塑料瓶呈Z字型构成的曲线段通道；上述直线段通道与曲线段通道的起始点和结束点分别处于同一水平高度位置；竖板正面中部还安装电子计时器。本实用新型除了实验的方式多样外，有助于降低理解抽象概念的难度，通过小球从不同路径通道下落耗时快慢的直观比对，帮助低年级的学生更快地掌握两点之间线段最短的公理性质概念，具备显著的趣味性、互动性、生动性和直观性特点，且装置整体结构简单，易于实现，适合普及。