REAIZATION OF THE NEIGHBORING LOGIC SYMMETRY FOR BOOLEAN ORDERED SET

By means of Logic symmetric relation,the single neighboring Logic path for Ndimensions Boolean ordered set is solved.A new method of determining any logic neighboringsubset in limited dimension is proposed.Its results are intuitional and realizable for computer.

基于有限谓词追踪的民机系统需求一致性检查方法

针对民机安全关键系统在正向研发过程中,系统级需求的正确性难以在设计早期全部完成确认的问题,提出一种基于有限谓词追踪的功能需求一致性检查体系。首先,引入一阶逻辑中的谓词追踪,建立系统内部功能需求与交互功能需求形式化规约方法。其次,针对单条、多条需求内容正确性以及需求关系一致性,构建需求一致性检查形式化规约,开展需求自冲突、集冲突与需求关系一致性检验,并生成可解释的检查反例进行需求迭代。最后,以机载平视显示(head-up display,HUD)系统飞行信息符号生成与显示功能为例,验证该方法的正确性与有效性。研究结果表明,基于有限谓词追踪的功能需求一致性检查方法能够提高需求一致性检查效率、降低研发成本,为民机系统级需求确认提供支持。

学校教学秩序重构的空间逻辑:动力与路向

作为素养时代教学变革的根本性问题,学校教学秩序重构内嵌于学校教学空间之中并以空间逻辑为基本遵循。教学秩序与空间逻辑之间具有合规律性、合目的性和合价值性三重联结向度,奠定了基于空间逻辑重构教学秩序的逻辑前提。学校教学秩序重构由空间自上而下的三组动力推动,包括社会秩序宏观投射与教学领域深化改革的张力平衡、教学资源迭代升级与师生关系生命互摄的要素协调,以及固化观念悄然解构与教学价值自觉出场的矛盾对立。基于空间逻辑重构教学秩序要根据教学空间的教育性、技术性和社会性特点,以主体具身交互澄清教学秩序的价值指向,在技术与教学的深度融合中重构教学秩序,以教学空间正义构建师生的主体间性关系。

冷战结束以来俄罗斯对国际秩序的认知历程及其演变逻辑

冷战结束以来俄罗斯对国际秩序的认知经历了一个曲折的发展历程:20世纪90年代中前期,俄罗斯全盘接受并极力融入美西方主导的自由国际秩序;20世纪90年代中后期开始到2007年,俄罗斯开始质疑和反思美西方自由国际秩序的制度标准和地缘安排,但依然希望被接纳;2008年至今,俄罗斯逐渐放弃对美西方自由国际秩序的幻想,并开始反击其地缘安排。2022年乌克兰危机爆发意味着俄罗斯对美西方秩序的彻底反击,并提出和推进其多极世界秩序构想。俄罗斯对国际秩序的认知历程是其自我认知与对外部世界的认知不断调适的产物,其形成过程受到多种因素的共同作用,主要包括俄罗斯的大国梦想和历史文化传统、美西方对俄罗斯的态度,以及世界政治的客观形势。

面向前提选择的新型图约简表示与图神经网络模型

自动定理证明器在证明问题时其搜索空间通常会呈现爆炸式增长,前提选择为该问题提供了新的解决思路。针对现有前提选择方法中逻辑公式图、图神经网络模型难以捕捉到公式图潜在信息的问题,提出了一种基于删除重复量词的简化逻辑公式图表示和具有注意力机制的项游走图神经网络模型,充分利用逻辑公式的语法和语义信息提高前提选择问题的分类精度。首先,将一阶逻辑猜想和前提公式转化为基于删除重复量词的简化一阶逻辑公式图;其次,利用消息传递图神经网络对节点和节点的项游走特征信息进行聚合和更新,随后使用注意力机制为图上的节点分配权重,进而调整图节点嵌入信息;最后,将前提图向量和猜想图向量拼接并输入二元分类器中实现前提分类。实验结果表明,所提方法在MPTP数据集和CNF数据集上的准确率分别达到了88.61%和84.74%,超越现有最优的前提选择方法。

一阶逻辑定理证明器中的无效子句删除策略

在一阶逻辑定理证明器中,子句预处理是不可或缺的步骤,而子句的消去规则是预处理中极其重要的部分。传统的基于纯文字规则的子句消去方法在理论上存在子句删除过多的问题,在算法实现上又存在子句删除不充分的情况。为了提高子句删除的精确率,在理论上,基于纯文字规则对子句进行再分类。第一类称为无效子句,该类子句不能通过等词替换与某个子句形成互补对,此类子句应完全删除;第二类为相对无效子句,该类子句无法与当前子句集中的子句形成互补对,但能进行等词替换,此类子句应在参与演绎后综合考虑是否删除。在算法实现中,考虑到子句的消去应是动态的过程,当前消去的子句会影响已判断的子句的无效性,提出一种用于判定子句无效性的递归遍历算法。将上述子句约简规则应用于证明器CSE1.5(Contradiction Separation Extension 1.5)中,以2019—2022的CADE(Conference on Automated DEduction)自动定理证明(ATP)系统竞赛中一阶逻辑问题组为测试对象。在300 s内,应用所提算法的CSE1.5_IC比原始CSE1.5总共多证明了27个问题。在两个版本证明器共同证明的所有FNE(FOF theorems without Equality)测试例中,CSE1.5_IC比CSE1.5平均每个问题多约简了28个子句,平均求解时间减少了7.07 s。实验结果表明,所提无效子句约简算法是一种有效的预处理方式,能够提高一阶逻辑子句集的约简精确率,同时能够提高自动定理证明器的证明能力和缩短证明时间。

一阶逻辑中基于treelet图神经网络的前提选择

前提选择是解决自动定理证明器面对大规模问题时性能降低的有效方法。当前面向一阶逻辑中前提选择的主流图神经网络忽略了逻辑公式图内部的节点顺序信息。针对此问题,将一种面向高阶逻辑公式的保序方法拓展到一阶逻辑中,并提出了一种基于treelet的图神经网络模型。该模型在信息聚合时一部分聚合中心节点的父、子节点信息,另一部分聚合节点顺序信息。实验分析表明:基于treelet的图神经网络模型在前提选择任务中比最优的主流图神经网络模型的分类准确率提高了约2%。

可满足性模理论综述

可满足性模理论(SMT)是指判定一阶逻辑公式在特定背景理论下的可满足性问题。基于一阶逻辑的SMT相比SAT描述能力更强、抽象能力更高,能处理更加复杂的问题。SMT求解器在各个领域都有应用,已经成为重要的形式化验证引擎。目前,SMT已被广泛应用在人工智能、硬件RTL验证、自动化推理和软件工程等领域。根据近些年SMT的发展,首先阐述SMT基本知识和常见的背景理论;然后分析总结Eager方法、Lazy方法和DPLL(T)方法的实现流程,并进一步介绍主流求解器Z3、CVC5和MathSAT5的实现过程;接着介绍SMT的扩展问题#SMT、SMT应用在深度神经网络的SMTlayer方法和量子SMT求解器;最后对SMT的发展进行展望,并讨论其面临的挑战。

父亲的缺位——论《阿卡迪亚》中的知识逻辑与性别秩序

在当代英国剧作家汤姆·斯托帕德所著《阿卡迪亚》中,贵族家庭里父亲的缺席和学术场域中权威的消解具有某种相似性,不仅表明传统父权秩序走向了崩塌,更体现出以颠覆与重述为核心的知识逻辑。这种知识逻辑贯穿剧中人物对知识的追寻、认知与重构,其背后则是理性与感性以及人文与科学的结合。首先,生活在19世纪英国的贵族小姐托马西娜具有罕见的科学禀赋,亦怀揣热情与爱,拒绝接受传统性别角色。其次,以汉娜为代表的20世纪当代学者致力于挖掘尘封的历史,坚信在权威论断和主流观点之外,其实另有真相。最后,剧中的一众知识青年慢慢发觉,无论是盲目崇拜理性与逻辑,还是完全遵从自身激情与想象,都会导致对真实的扭曲和对学术事业的破坏,其经历揭示知识霸权的本质在于拒绝多元与差异,固守自封。随着情节发展,对立与冲突被化解,原有秩序下中心与边缘的二元对立消融。通过对比、再现发生在古今不同时空西德利庄园中的故事,斯托帕德构想了一个理性与感性有机结合、古典主义与浪漫主义交融碰撞的图景,指出在知识追寻与生产过程中,人们需要避免急功近利的学术浮夸,努力消除性别对立与学术霸权,以还原女性被父权话语遮蔽的才华,消解依仗传统权力话语关系的逻各斯中心话语体系。

阶数位于1到2之间的分数阶神经网络同步控制

近年来,神经网络同步问题吸引了系统控制、数学和计算机科学等多个领域学者的关注。针对阶数位于1到2之间的分数阶神经网络同步控制问题,通过变量替换法,将阶数在(1,2)之间的分数阶神经网络同步控制问题转化为阶数在(0,1)之间的分数阶神经网络同步控制问题。由于分数阶神经网络中含有未知非线性函数项,因此使用模糊逻辑系统进行逼近。之后,为了使从神经网络跟踪主神经网络,设计了合适的控制器,并且,对其同步误差系统进行稳定性分析。最后,通过仿真实例验证了所提出方法的有效性。

基于一阶谓词逻辑的结构设计规范表示方法

目前,基于BIM模型的合规性审查采用人工方式,工作量繁重且自动化程度低,开展自动合规性审查研究具有重要意义。在结构设计领域能够有效支撑规范知识表示与推理并支持设计审查自动化的设计规范表达方法有待开发。基于一阶谓词逻辑,通过转译《混凝土结构设计规范》中的设计条款,提出一种结构设计规范规则表达和推理方法。该方法可实现将半结构化设计规范条款转换为结构化知识并支持灵活查询与推理,通过“谓词定义”和“函数定义”转译设计规范中语言类、表格类和计算公式类设计条款,提出两种规范条款谓词定义方式。对于语言模糊类、表后注释类和条款补充类的设计条款给出转译解决方案。提出的方法有效地解决了传统一阶谓词对于结构设计条款表示不充分和不精确的问题,进而为设计规范的计算机表达提供一种参考方法。

基于矩阵解耦的精馏塔VOFFLC温控系统

针对复杂的精馏塔MIMO温控系统的多变量、非线性、强耦合的特点和自适应需求,设计了基于矩阵解耦精馏塔的VOFFLC系统。首先,对温控系统的多变量控制模型进行改进,利用矩阵解耦理论实现对角解耦,以此改变控制通道的特性;然后,设计基于矩阵解耦的精馏塔VOFFLC温控系统,实现精馏塔的塔顶和塔底的自适应温控;最后,采用仿真实验,对所设计的多种温控系统进行性能比较。实验结果表明,VOFFLC系统可以实现控制参数的自适应,具有更强的论域容错性和鲁棒性。

The Narratological Analysis on Ivanhoe

沃尔特·司各特的小说《艾凡赫》中运用了许多叙事手法,他们在塑造人物性格、反映作者立场及推动情节发展上起到一定作用。本文从叙事聚焦、叙事时间和叙事逻辑三个方面对沃尔特.司各特的小说《艾凡赫》展开分析。通过分析可以看出作者作为政治保守派的立场,男女主人公的性格特征和故事情节的发展。

面向5G超密集异构网络的模糊逻辑切换算法

针对基站之间距离近、网络数量庞大的超密集网络中切换过程存在干扰以及频繁切换问题,提出了一种基于预判决的模糊逻辑切换算法。算法在计算用户接收信号的信干噪比基础上,预筛选出干扰较小的网络,计算用户在筛选出的候选网络中的停留时间,当停留时间大于门限值时对候选网络使用基于模糊逻辑的逼近理想解排序算法。通过模糊逻辑优化网络属性参数,进而使用逼近理想解排序算法对候选网络进行排序。排序过程中,使用修正后的贴近度计算方式使计算结果更加精确。仿真实验证明,该算法在超密集异构网络切换中可以有效降低切换次数,减少网络阻塞概率,有效提升用户服务质量。

中国式教师教育现代化:逻辑、特征与路径

中国式教师教育现代化有其鲜明的内在逻辑,体现在以提升教师作为专业人的现代性品格为价值追寻,以马克思主义教师队伍建设思想为理论指导,以教师教育高质量发展现实需要为实践关照。中国式教师教育现代化不同于西方精英式教师教育现代化,具有人民性、公平性、融合性和开放性等鲜明特征。新时代,推进中国式教师教育现代化要坚持党对教师教育事业全面领导的发展思想,构建创新共生体发展模式,聚焦特色化建设发展主线,打造面向世界的开放发展格局。

基于大规模语言模型的知识图谱可微规则抽取

知识图谱上的推理是预测不完整三元组中缺失的实体或关系,对结构化知识进行补全,并用于不同下游任务的过程。不同于被普遍研究的黑盒方法,如基于表示学习的推理方法,基于规则抽取的推理方法通过从知识图谱中泛化出一阶逻辑规则,实现一种可解释的推理范式。为解决离散的符号空间与连续的嵌入空间之间的鸿沟,提出一种基于大规模预训练语言模型的知识图谱可微规则抽取方法DRaM,将离散的一阶逻辑规则与连续的向量空间进行融合。针对规则中的原子公式顺序对推理过程产生的影响,通过引入大规模预训练语言模型对推理过程进行编码来解决。融合一阶逻辑规则的可微推理方法DRaM,在三个知识图谱数据集Family、Kinship和UMLS上进行的链接预测任务获得了较好的结果,尤其针对链接预测指标Hits@10,DRaM获得了最佳的推理结果。实验结果表明,DRaM能够有效地解决知识图谱上可微推理存在的问题,并且可以从推理过程中抽取带有置信度的一阶逻辑规则。DRaM不仅通过一阶逻辑规则增强了推理效果,同时增强了方法的可解释性。

基于子句活跃度和复杂度的多元动态演绎算法及应用

一阶逻辑自动定理证明是知识表示与自动推理领域重要的研究内容,如何有效选取子句参与演绎是提升自动推理能力和效率的研究热点。基于多元动态演绎良好的演绎特性,通过分析子句的变元项性质和函数项结构,提出了一种子句活跃度和复杂度的度量与计算方法,能很好地对不同项结构的子句进行有效评估;基于该子句评估方法,提出了一种子句充分协同演绎的多元动态演绎算法,能有效优化多元演绎搜索路径。将该多元动态演绎算法应用于国际顶尖证明器Eprover 2.6中,以2021年国际自动推理FOF组竞赛例为测试对象,在标准的300 s测试时间内,加入了多元动态演绎算法的Eprover 2.6相比原始Eprover 2.6多证明定理4个,在证明定理总数相同的条件下,平均证明时间减少了1.12 s;能证明Eprover 2.6未证明定理16个,占未证明定理总数的15.1%。实验结果表明,该多元动态演绎算法是一种有效的推理方法,能在一定程度上提升自动定理的证明能力和时间效率。

基于多引擎并行协作的SCADE模型检测

SCADE语言是一种同步数据流语言,通常被用于实时嵌入式自动控制系统的开发,在航空航天、交通、核工业等领域有广泛的应用。已有的SCADE同步语言模型检测工具存在无法验证部分复杂程序和验证效率低下的问题。为了解决现有的问题,该文提出了多引擎并行协作的方法,通过并行执行BMC引擎、归纳法引擎和程序抽象引擎三个模型检测引擎来实现对SCADE同步语言程序验证的协作,其中程序抽象引擎通过反例引导的抽象精化方法解决了大型复杂程序验证效率低下的问题。实现了一款针对SCADE同步语言程序的模型检测工具PSMC,该工具采用多引擎并行协作方法来提升SCADE同步语言程序模型检测的效率。手动构造了887个SCADE同步语言程序用于对PSMC进行实验验证,结果表明提出的优化方法可以有效地对SCADE同步语言程序进行自动的验证,并且可以提升模型检测的验证效率(约31%)。

乡村治理的文化逻辑:从传统到现代的阴阳秩序

本文试图探讨乡村治理文化逻辑从传统到现代的传承与变迁,这套逻辑包含了属阴的宗教信仰和属阳的儒家伦理规范两个面向。传统中国的乡村治理存在一阴一阳两个操作系统,阳面是儒家伦理,阴面则是神道设教;宗教信仰和伦理规范的内在一致性构建了一种阴阳和合的治理秩序,并促成了贯穿国家与乡村的教化之治。而在现代中国,现代化使得神道设教基本崩解,乡村治理体系从阴阳和合到阴阳二分,这也成为当代乡村治理的困境之一。为此,国家尝试以产业化、非遗化和场所合法化等制度性方式重新吸纳民间信仰;与此同时,地方社会自发的民间信仰复兴也有效地激活了乡村治理的文化资源,其关键在于这种复兴所激发的地方自主性正是乡村共同体形成内生秩序的基础。本文认为,乡村治理应当继续赋予民间信仰等乡土文化发展的空间,从而发挥其低成本治理优势。

针对教学场景的ZFC集合论Coq形式化

离散数学是计算机类专业的基础课程之一,命题逻辑、一阶逻辑与公理集合论是其重要组成部分.教学实践表明,初学者准确理解语法、语义、推理系统等抽象概念是有一定难度的.近年来,已有一些学者开始在教学中引入交互式定理证明工具,以帮助学生构造形式化证明,更透彻地理解逻辑系统.然而,现有的定理证明器有较高上手门槛,直接使用会增加学生的学习负担.鉴于此,在Coq中开发了针对教学场景的ZFC公理集合论证明器.首先,形式化了一阶逻辑推理系统和ZFC公理集合论;之后,开发了数条自动化推理规则证明策略.学生可以在与教科书风格相同的简洁证明环境中使用自动化证明策略完成定理的形式化证明.该工具被用在了大一新生离散数学课程的教学中,没有定理证明经验的学生使用该工具可以快速完成数学归纳法和皮亚诺算术系统等定理的形式化证明,验证了该工具的实际效果.