期刊文献+
共找到28篇文章
< 1 2 >
每页显示 20 50 100
一阶逻辑中公理化真度研究 被引量:2
1
作者 郝娇 惠小静 +1 位作者 马硕 金明慧 《计算机科学》 CSCD 北大核心 2021年第S02期669-671,712,共4页
一阶逻辑是公理系统的标准形式逻辑之一,其中包含的程度化推理等研究内容,是一个研究热点也是难点。文中从一阶逻辑演算的语义理论出发,利用可满足性及完备性定理研究了一阶逻辑中公理化真度。首先给出并、交运算可满足性的定义,其次说... 一阶逻辑是公理系统的标准形式逻辑之一,其中包含的程度化推理等研究内容,是一个研究热点也是难点。文中从一阶逻辑演算的语义理论出发,利用可满足性及完备性定理研究了一阶逻辑中公理化真度。首先给出并、交运算可满足性的定义,其次说明了两个特殊公式与逻辑有效公式以及定理的关系,最后得出与公式等价的前束范式。上述结果将为谓词逻辑程度化研究做准备。 展开更多
关键词 一阶逻辑 逻辑有效公式 可满足性 定理 前束范式
下载PDF
基于否证蕴含的极小一阶不可满足子式求解算法 被引量:1
2
作者 张建民 沈胜宇 李思昆 《计算机学报》 EI CSCD 北大核心 2010年第3期415-426,共12页
解释公式不可满足的原因在软件分析与验证等众多领域都具有非常重要的理论与应用价值,而极小不可满足子公式能够为公式不可满足的原因提供精炼的解释,帮助应用领域的自动化工具迅速定位错误,准确地诊断问题失败的本质缘由.文中针对极小... 解释公式不可满足的原因在软件分析与验证等众多领域都具有非常重要的理论与应用价值,而极小不可满足子公式能够为公式不可满足的原因提供精炼的解释,帮助应用领域的自动化工具迅速定位错误,准确地诊断问题失败的本质缘由.文中针对极小一阶不可满足子式的求解问题,引入了否证蕴含图及其正向与逆向可达结点的概念,并证明了不可满足子式与否证蕴含图之间的关系.基于二者的关系,提出了基于冲突分析与否证蕴含的极小一阶不可满足子式求解算法,并融合了蕴含图剪枝技术,以提高算法效率.通过实验与当前最优的深度优先搜索算法进行了比较,结果表明:文中的算法显著优于深度优先搜索算法,并且随着公式复杂度的增加,性能优势更加明显. 展开更多
关键词 一阶逻辑公式 可满足模理论问题 极小不可满足子式 消解否证 否证蕴含图
下载PDF
一阶逻辑vs组合范畴语法:公式、目标与表达力
3
作者 姚从军 林延廷 《贵州工程应用技术学院学报》 2023年第1期51-58,共8页
一阶逻辑和组合范畴语法都是追逐“莱布尼茨之梦”的产物。一阶逻辑独立于自然语言,从人工语言出发,依据公式形成规则,生成逻辑公式;组合范畴语法实现了自然语言表达式的句法和语义的并行推演,伴随句法组合,自动生成相应的语义表达式。... 一阶逻辑和组合范畴语法都是追逐“莱布尼茨之梦”的产物。一阶逻辑独立于自然语言,从人工语言出发,依据公式形成规则,生成逻辑公式;组合范畴语法实现了自然语言表达式的句法和语义的并行推演,伴随句法组合,自动生成相应的语义表达式。一阶逻辑以找出有效的推理模式为目标,关注系统本身的可靠性和完全性;组合范畴语法旨在用形式化的方法判断语句是否合语法和给出语言表达式的形式语义,关注计算机对自然语言的理解和处理。一阶逻辑对自然语言的抽象化程度非常高,舍弃了自然语言的内涵意义;组合范畴语法立足自然语言,全面、细致地刻画自然语言的句法和语义。 展开更多
关键词 一阶逻辑 组合范畴语法 合式公式 有效推理 自然语言处理
下载PDF
一阶谓词公式F与其Herbrand扩张之间的关系
4
作者 张韬 汤建钢 《伊犁师范学院学报(自然科学版)》 2016年第1期9-13,共5页
任意一个一阶谓词公式F,先找到其中的个体常元和函数符号,并由此产生公式F的Herbrand域,然后用Herbrand域中的项替代公式F中的变元,以消去量词符号而得到公式F的函数形式.公式F的所有可能的函数形式组成的集合就是Herbrand扩张.研究了... 任意一个一阶谓词公式F,先找到其中的个体常元和函数符号,并由此产生公式F的Herbrand域,然后用Herbrand域中的项替代公式F中的变元,以消去量词符号而得到公式F的函数形式.公式F的所有可能的函数形式组成的集合就是Herbrand扩张.研究了寻找一阶谓词公式与Herbrand扩张之间的关系. 展开更多
关键词 命题公式 一阶谓词公式 Herbrand扩张 可满足性
下载PDF
一阶逻辑中不含相同谓词符号公式的真度研究
5
作者 王波 惠小静 鲁星 《贵州大学学报(自然科学版)》 2022年第5期29-34,共6页
自真度概念被提出以来,命题逻辑的计量化得到了广泛的关注和发展。谓词逻辑的相关研究是一个难点,其中一阶逻辑的公理化真度以及程度化才刚刚起步。从文字的完全闭包及其合取的公理化真度出发,首先,证明了不含相同谓词符号广义合取式的... 自真度概念被提出以来,命题逻辑的计量化得到了广泛的关注和发展。谓词逻辑的相关研究是一个难点,其中一阶逻辑的公理化真度以及程度化才刚刚起步。从文字的完全闭包及其合取的公理化真度出发,首先,证明了不含相同谓词符号广义合取式的真度计算公式;其次,通过合取范式的结构特点,证明了合取范式的真度计算公式;再次,证明了2个公式的逻辑等价性。所得结果为后续公理化真度性质研究奠定了基础。 展开更多
关键词 一阶逻辑 公式真度 合取范式 逻辑等价
下载PDF
一类一阶逻辑公式中的公理化真度理论及其应用 被引量:32
6
作者 王国俊 《中国科学:信息科学》 CSCD 2012年第5期648-662,共15页
设Φ是全体不含函数符号的一阶闭逻辑公式之集.本文基于有限模型和均匀概率的思想对非单调逻辑中的典型案例做了分析,通过概率计算给出了应当赋予文字的完全闭包及其合取的真度值.以此为基础,在Φ中建立了公理化的真度理论.证明了Φ中... 设Φ是全体不含函数符号的一阶闭逻辑公式之集.本文基于有限模型和均匀概率的思想对非单调逻辑中的典型案例做了分析,通过概率计算给出了应当赋予文字的完全闭包及其合取的真度值.以此为基础,在Φ中建立了公理化的真度理论.证明了Φ中每个公式的真度都是可计算的,并且证明了Φ中逻辑公式的真度之集H与命题逻辑中的计算结果相一致,特别是其中所有闭文字的真度都等于1/2.在真度理论的基础上引入了Φ中公式之间相似度和伪距离的计算方法,并提出了逻辑理论的相容度理论.作为应用,给出了估计Horn子句型数据库相容度的一种方法. 展开更多
关键词 谓词逻辑 一阶逻辑公式 函数符号 真度 可计算性 HORN子句
原文传递
人工湿地动力学模型研究 被引量:7
7
作者 邓春光 蔡明凯 《安徽农业科学》 CAS 北大核心 2007年第15期4583-4584,4613,共3页
人工湿地作为一种新型生态污水处理技术,在实际应用中取得了快速发展。讨论了人工湿地3种常用的数学模型(一级动力学模型、Monod动力学模型和Ergun公式),并对表达式之间的转换关系作了较为详细的推导;同时对其各自的优缺点作了分析。从... 人工湿地作为一种新型生态污水处理技术,在实际应用中取得了快速发展。讨论了人工湿地3种常用的数学模型(一级动力学模型、Monod动力学模型和Ergun公式),并对表达式之间的转换关系作了较为详细的推导;同时对其各自的优缺点作了分析。从中可以看出,人们对人工湿地去除污染物的内在机制尚缺乏定量化的了解,目前还难以对其设计、运行和预测作出十分准确的评价。最后对数学模型的研究方向作了展望。 展开更多
关键词 人工湿地 一级动力学模型 Monod动力学模型 Ergun公式
下载PDF
{I_(m)}(α-逻辑有效公式)的理论及其应用 被引量:6
8
作者 张兴芳 孟广武 +1 位作者 赵峰 张安英 《工程数学学报》 CSCD 北大核心 2007年第1期179-182,共4页
建立了一阶模糊语言φ的α[I]-真公式,可达α^(+)[I]-真公式,可数解释模型{I_(m)}(α-逻辑有效公式),可达{I_(m)}(α-逻辑有效公式)及{I_(m)}(α^(+)-逻辑有效公式)的理论,并讨论了它们的一系列性质及其在近似推理中的应用。
关键词 一阶模糊语言 α[I]-真公式 可数解释模型{I_(m)} {I_(m)}(α-逻辑有效公式)
下载PDF
基于一阶谓词公式去除商务数据冗余关联规则的研究 被引量:6
9
作者 郭瑞 钱晓东 《计算机工程与科学》 CSCD 北大核心 2017年第3期593-598,共6页
由于现代网络数据量的急速增长,利用现有的算法生成关联规则时,冗余规则的数量远远大于实际有价值的规则,冗余规则不仅影响用户分析,而且使关联规则的利用率也大大降低。针对关联规则的冗余问题,提出了一种基于一阶谓词公式去除商务数... 由于现代网络数据量的急速增长,利用现有的算法生成关联规则时,冗余规则的数量远远大于实际有价值的规则,冗余规则不仅影响用户分析,而且使关联规则的利用率也大大降低。针对关联规则的冗余问题,提出了一种基于一阶谓词公式去除商务数据冗余关联规则的方法,利用一阶谓词公式来表示关联规则,通过等价公式进行转换,并利用算法和矩阵等价将谓词公式转换为邻接矩阵,然后利用冗余规则算法进行删除。实验原始数据为UCI数据集,并利用Weka生成关联规则。最后利用Matlab和Java实现冗余规则的去除。 展开更多
关键词 关联规则 一阶谓词公式 关联矩阵 邻接矩阵
下载PDF
一阶逻辑中基于treelet图神经网络的前提选择
10
作者 马雪 何星星 +1 位作者 兰咏琪 李莹芳 《计算机工程与科学》 CSCD 北大核心 2024年第2期374-380,共7页
前提选择是解决自动定理证明器面对大规模问题时性能降低的有效方法。当前面向一阶逻辑中前提选择的主流图神经网络忽略了逻辑公式图内部的节点顺序信息。针对此问题,将一种面向高阶逻辑公式的保序方法拓展到一阶逻辑中,并提出了一种基... 前提选择是解决自动定理证明器面对大规模问题时性能降低的有效方法。当前面向一阶逻辑中前提选择的主流图神经网络忽略了逻辑公式图内部的节点顺序信息。针对此问题,将一种面向高阶逻辑公式的保序方法拓展到一阶逻辑中,并提出了一种基于treelet的图神经网络模型。该模型在信息聚合时一部分聚合中心节点的父、子节点信息,另一部分聚合节点顺序信息。实验分析表明:基于treelet的图神经网络模型在前提选择任务中比最优的主流图神经网络模型的分类准确率提高了约2%。 展开更多
关键词 一阶逻辑公式 图神经网络 前提选择 二元分类
下载PDF
基于边权重图神经网络的一阶逻辑前提选择 被引量:3
11
作者 刘清华 徐扬 +1 位作者 吴贯锋 李瑞杰 《西南交通大学学报》 EI CSCD 北大核心 2022年第6期1368-1375,共8页
为提高自动定理证明器在大规模问题中证明问题的能力,前提选择任务应运而生.由于公式图的有向性,主流的图神经网络框架只能单向地对节点进行更新,且无法编码公式图中子节点间的顺序.针对以上问题,提出了带有边类型的双向公式图表示方法... 为提高自动定理证明器在大规模问题中证明问题的能力,前提选择任务应运而生.由于公式图的有向性,主流的图神经网络框架只能单向地对节点进行更新,且无法编码公式图中子节点间的顺序.针对以上问题,提出了带有边类型的双向公式图表示方法,并提出了一种基于边权重的图神经网络(edge-weight-based graph neural network,EW-GNN)模型用于编码一阶逻辑公式.该模型首先利用相连节点的信息来更新对应边类型的特征表示,随后利用更新后的边类型特征计算邻接节点对中心节点的权重,最后利用邻接节点的信息双向地对中心节点进行更新.实验比较分析表明:基于边权重的图神经网络模型在前提选择任务中表现得更加优越,其在相同的测试集上比当前最优模型的分类准确率高了约1%. 展开更多
关键词 图神经网络 双向图 前提选择 一阶逻辑公式
下载PDF
EXPONENTIAL FOURIER COLLOCATION METHODS FOR SOLVING FIRST-ORDER DIFFERENTIAL EQUATIONS 被引量:1
12
作者 Bin Wang Xinyuan Wu +1 位作者 Fanwei Meng Yonglei Fang 《Journal of Computational Mathematics》 SCIE CSCD 2017年第6期711-736,共26页
In this paper, a novel class of exponential Fourier collocation methods (EFCMs) is presented for solving systems of first-order ordinary differential equations. These so-called exponential Fourier collocation method... In this paper, a novel class of exponential Fourier collocation methods (EFCMs) is presented for solving systems of first-order ordinary differential equations. These so-called exponential Fourier collocation methods are based on the variation-of-constants formula, incorporating a local Fourier expansion of the underlying problem with collocation meth- ods. We discuss in detail the connections of EFCMs with trigonometric Fourier colloca- tion methods (TFCMs), the well-known Hamiltonian Boundary Value Methods (HBVMs), Gauss methods and Radau IIA methods. It turns out that the novel EFCMs are an es- sential extension of these existing methods. We also analyse the accuracy in preserving the quadratic invariants and the Hamiltonian energy when the underlying system is a Hamiltonian system. Other properties of EFCMs including the order of approximations and the convergence of fixed-point iterations are investigated as well. The analysis given in this paper proves further that EFCMs can achieve arbitrarily high order in a routine manner which allows us to construct higher-order methods for solving systems of first- order ordinary differential equations conveniently. We also derive a practical fourth-order EFCM denoted by EFCM(2,2) as an illustrative example. The numerical experiments using EFCM(2,2) are implemented in comparison with an existing fourth-order HBVM, an energy-preserving collocation method and a fourth-order exponential integrator in the literature. The numerical results demonstrate the remarkable efficiency and robustness of the novel EFCM(2,2). 展开更多
关键词 first-order differential equations Exponential Fourier collocation methods Variation-of-constants formula Structure-preserving exponential integrators Collocation methods.
原文传递
基于语言真值格值一阶逻辑系统L_(v(n×2))F(X)中程度化公式的一些注记 被引量:2
13
作者 赖家俊 徐扬 《系统科学与数学》 CSCD 北大核心 2013年第10期1256-1262,共7页
引入了语言真值格值一阶逻辑系统L_(v(n×2))F(X)的原子程度公式和语言真值格值程度合式公式的概念,讨论了解释域D下的公式偏真和恒真的一些推演性质,得到了程度化公式偏真和恒真的一些语义与语法特征.
关键词 语言真值格值一阶逻辑 形式推演 逻辑公式 程度化公式
原文传递
平面第二类曲线积分的一种简便计算方法 被引量:1
14
作者 李小梅 《浙江科技学院学报》 CAS 2012年第3期185-189,共5页
第二类曲线积分的计算在微积分学中是一个难点,其中概念既多又抽象,计算既繁又难以判断;而在研究生入学考试的命题中,曲线积分的出题率却又非常高,同时又伴随着题目难度大、解题正确率低的现象。但是,若将格林公式进行转化,就可得到平... 第二类曲线积分的计算在微积分学中是一个难点,其中概念既多又抽象,计算既繁又难以判断;而在研究生入学考试的命题中,曲线积分的出题率却又非常高,同时又伴随着题目难度大、解题正确率低的现象。但是,若将格林公式进行转化,就可得到平面第二类曲线积分计算的一种简便方法。它无需更多的判别就可直接进行计算,给正确理解、准确计算平面第二类曲线积分提供了一种思路。 展开更多
关键词 第二类曲线积分 连通区域 一阶连续偏导数 正向曲线 格林公式
下载PDF
谓词逻辑中公理化真度的若干评注
15
作者 马硕 惠小静 郝娇 《宁夏大学学报(自然科学版)》 CAS 2022年第1期30-32,40,共4页
根据一阶谓词逻辑中公理化真度的定义对给定公式的真度进行了计算,讨论了该真度下伪距离的性质,并应用赋值法论证了真度为1的公式与广义定理及定理的关系,分析了真度为0的公式与广义矛盾式及矛盾式之间的异同.
关键词 一阶谓词逻辑 真度 广义矛盾式 矛盾式 定理
下载PDF
关于常微分方程中Liouville公式的注记
16
作者 武力兵 沙秋夫 姜本源 《辽宁科技大学学报》 CAS 2010年第1期1-3,11,共4页
证明了n阶齐次线性微分方程(dnx)/(dtn)+a1(t)(dn-1x)/(dtn-1)+…+an-1(t)dx/dt+an(t)x=0的Liouville公式W′(t)=W(t0)e-∫tt0a1(s)ds是一阶齐次线性微分方程组x′=A(t)x所对应的Liouville公式W′(t)=W(t0)e-integral from a=1 to t sum... 证明了n阶齐次线性微分方程(dnx)/(dtn)+a1(t)(dn-1x)/(dtn-1)+…+an-1(t)dx/dt+an(t)x=0的Liouville公式W′(t)=W(t0)e-∫tt0a1(s)ds是一阶齐次线性微分方程组x′=A(t)x所对应的Liouville公式W′(t)=W(t0)e-integral from a=1 to t sum from i=1 to n aii(s)ds的特殊情形。 展开更多
关键词 n阶线性齐次微分方程 一阶齐次线性微分方程组 Liouville公式
下载PDF
一阶系统KL中一组形式相近公式之间的关系
17
作者 齐玉霞 周相泉 刘庆松 《山东师范大学学报(自然科学版)》 CAS 2010年第3期29-31,共3页
一阶语言是自然语言(特别的数学语言)的一种形式化体系,引入不同的连接词、量词、个体变元、谓词、个体常元、关系符号便有了不同的表达式.笔者讨论了一阶形式系统KL中一组形式相近公式(任意xi)A(xi),A(xi),( xi)A(xf)... 一阶语言是自然语言(特别的数学语言)的一种形式化体系,引入不同的连接词、量词、个体变元、谓词、个体常元、关系符号便有了不同的表达式.笔者讨论了一阶形式系统KL中一组形式相近公式(任意xi)A(xi),A(xi),( xi)A(xf),A(t),A(ai)之间的关系.从而可以更方便从语义和语构两方面研究一阶语言. 展开更多
关键词 一阶形式系统KL 逻辑有效公式 完备性 关系
下载PDF
冰温贮藏对鲜切山药品质的影响及货架期的预测 被引量:12
18
作者 马卓云 于潇潇 +1 位作者 杨舒乔 苑宁 《农产品加工》 2021年第2期4-9,共6页
以山药为原料进行鲜切处理,分别在冰温,4,14,25℃下贮藏,通过对样品感官评分、褐变度、失重率、多酚氧化酶活性(PPO)、丙二醛(MDA)含量和菌落总数等指标进行测定,研究冰温贮藏技术对鲜切山药品质影响。随后基于试验数据,利用阿伦尼乌斯... 以山药为原料进行鲜切处理,分别在冰温,4,14,25℃下贮藏,通过对样品感官评分、褐变度、失重率、多酚氧化酶活性(PPO)、丙二醛(MDA)含量和菌落总数等指标进行测定,研究冰温贮藏技术对鲜切山药品质影响。随后基于试验数据,利用阿伦尼乌斯方程建立鲜切山药MDA含量和褐变度品质指标的一级动力学模型来模拟鲜切山药的货架期模型,并以偏差度(BF)、准确度(AF)对上述货架期模型进行评价。结果表明,冰温贮藏可以有效延缓鲜切山药的褐变,同时降低失重率,保持多酚氧化酶活性,降低丙二醛含量,维持低微生物水平,能够较好地保持鲜切山药的品质。以MDA含量为品质指标预测的货架期模型AF为0.9,更趋近于1,可以更好地反映鲜切山药的品质指标变化,建模更准确,该模型EA=54732.03232 J/mol,k0=6170217959.94,可在适宜的范围内对鲜切山药进行实时监测。 展开更多
关键词 冰温贮藏 一级动力学模型 阿伦尼乌斯方程 货架期预测
下载PDF
XPath语义特性及其对XML数据操作的应用研究 被引量:3
19
作者 张婷 常致全 肖厚新 《信息技术》 2006年第5期94-97,100,共5页
给出了XPath语义的简洁定义,使用XPath标准的语法格式说明查询步骤,并通过一个具体实例说明定位路径的方法,实现了XPath与XSLT结合的XML查询,同时对XPath在.NET中的应用进行了研究。
关键词 XPATH 路径匹配 语义函数 模型树 一阶公式
下载PDF
面向前提选择的新型图约简表示与图神经网络模型
20
作者 兰咏琪 何星星 +1 位作者 李莹芳 李天瑞 《计算机科学》 CSCD 北大核心 2024年第5期193-199,共7页
自动定理证明器在证明问题时其搜索空间通常会呈现爆炸式增长,前提选择为该问题提供了新的解决思路。针对现有前提选择方法中逻辑公式图、图神经网络模型难以捕捉到公式图潜在信息的问题,提出了一种基于删除重复量词的简化逻辑公式图表... 自动定理证明器在证明问题时其搜索空间通常会呈现爆炸式增长,前提选择为该问题提供了新的解决思路。针对现有前提选择方法中逻辑公式图、图神经网络模型难以捕捉到公式图潜在信息的问题,提出了一种基于删除重复量词的简化逻辑公式图表示和具有注意力机制的项游走图神经网络模型,充分利用逻辑公式的语法和语义信息提高前提选择问题的分类精度。首先,将一阶逻辑猜想和前提公式转化为基于删除重复量词的简化一阶逻辑公式图;其次,利用消息传递图神经网络对节点和节点的项游走特征信息进行聚合和更新,随后使用注意力机制为图上的节点分配权重,进而调整图节点嵌入信息;最后,将前提图向量和猜想图向量拼接并输入二元分类器中实现前提分类。实验结果表明,所提方法在MPTP数据集和CNF数据集上的准确率分别达到了88.61%和84.74%,超越现有最优的前提选择方法。 展开更多
关键词 图神经网络 前提选择 注意力机制 一阶逻辑公式 图约简表示方法
下载PDF
上一页 1 2 下一页 到第
使用帮助 返回顶部