检索结果-南通市图书馆

Complexity of Some Problems Concerning 2CNF Formulas

维普期刊数据库评论

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

中山大学学报（社会科学版） 2003年第S1期43卷 131-146页

作者： hans kleine Büning 帕德恩大学

In this paper we investigate the complexity of several problems concerning 2CNF formulas. At first, we show that the minimal unsatisfiability problem for 2CNF formulas can be solved in linear time. Then we prove that the problem determining if a 2CNF formula can be transformed to a minimal unsatisfiable formula is also solvable in linear time. Thirdly, we show the polynomial solvability of the satisfiability problem for symmetric monotone formulas in which all clauses has length 2 or ? n - k ( n is the ...

关键词： minimal unsatisfiable formulas symmetric monotone formulas satisfiability complexity

变量极小不可满足在模型检测中的应用(英文)

在线全文

学校读者我要写书评

暂无评论

软件学报 2008年第1期19卷 39-47页

作者：陈振宇陶志红 kleine BURNING hans 王立福东南大学计算机科学与工程学院江苏南京210096 北京大学软件与微电子学院北京100871 Department of Computer Science University of Paderborn Paderborn 33095 Germany

提出一个结合变量抽象和有界模型检测(BMC)的验证框架,用于证明反例不存在或输出存在反例.引入变量极小不可满足(VMU)的数学概念来驱动抽象精化的验证过程.一个VMU公式F的变量集合是保证其不可满足性的一个极小集合.严格证明了VMU驱动... 详细信息

提出一个结合变量抽象和有界模型检测(BMC)的验证框架,用于证明反例不存在或输出存在反例.引入变量极小不可满足(VMU)的数学概念来驱动抽象精化的验证过程.一个VMU公式F的变量集合是保证其不可满足性的一个极小集合.严格证明了VMU驱动的精化满足抽象精化框架中的两个理想性质:有效性和极小性.虽然VMU的判定问题和极小不可满足(MU)一样难,即DP完全的,该案例研究表明,在变量抽象精化过程中,VMU比MU更为有效.

关键词：极小不可满足抽象精化模型检测

Dining Cryptographer安全协议及工程分析

在线全文

学校读者我要写书评

暂无评论

电子学报 2005年第2期33卷 262-265页

作者：陶志红 hans kleineBuing 张世琨王立福南京大学数学系江苏南京210093 Paderborn大学计算机系北京大学计算机系北京100871

网络信息安全包括信息内容的加密及通讯的匿名性质 .DiningCryptographer (DC net)协议[1,2 ] 就是一个基于数学不可解特性的基础安全匿名通信协议 ,其主要特点是通过提供匿名信息服务来避免恶意攻击 .本文在介绍DC net协议工作原理的... 详细信息

网络信息安全包括信息内容的加密及通讯的匿名性质 .DiningCryptographer (DC net)协议[1,2 ] 就是一个基于数学不可解特性的基础安全匿名通信协议 ,其主要特点是通过提供匿名信息服务来避免恶意攻击 .本文在介绍DC net协议工作原理的基础上 ,从工程应用角度给出了如何构建基于DC net协议的分布式安全信息服务 ,并对运行时的有关问题进行了研究 .

关键词：安全协议形式化分析电子商务 Internet网络 DC—net(Dining Cryptographer net)协议

在线全文

学校读者我要写书评

暂无评论

辅助变元之于命题与量化布尔公式的作用

逻辑学研究 2010年第3期3卷 1-23页

作者：乌维.布贝克汉斯.克莱那.布吕宁帕德博恩大学计算机科学研究所

使用辅助变元来引入定义,在知识表达中是一个流行和有力的技巧,能够得到更短、更自然的编码而无需冗长的重复。这篇论文中,我们形式地定义了辅助变元的概念,检验了其表达力并讨论了有趣的相关应用。我们把以下两者联系起来:一是,反复使... 详细信息

使用辅助变元来引入定义,在知识表达中是一个流行和有力的技巧,能够得到更短、更自然的编码而无需冗长的重复。这篇论文中,我们形式地定义了辅助变元的概念,检验了其表达力并讨论了有趣的相关应用。我们把以下两者联系起来:一是,反复使用中间结果而不通过定义重复;二是,布尔函数其他表达中的相似概念。特别的,我们表明带定义的命题逻辑与具有任意输出端的布尔线路以及约束变元满足Horn性质的存在量化布尔公式(记作(?)HORN^b)具有相同的表达力。本文还考虑了定义结构的限制,以及命题定义的扩充。特别的,我们检验了正命题定义与带存在量化的正定义之间的关系(或等价地,检验了(?)HORN^b公式和约束变元未被Horn限定的存在量化的CNF公式(记作(?)CNF~*)之间的关系)。对命题定义的进一步扩充,是允许在定义中使用任意的量词,或等价地,允许布尔公式的嵌入。我们还证明了,量化CNF公式中的约束变元的表达力,是由子句中被约束部分的极小不可满足子公式或极小假子公式的结构所决定的。

关键词：命题逻辑公式量化表达力知识表达定义检验概念

在线全文

学校读者我要写书评

暂无评论

世界哲学史