检索结果-南通市图书馆

R-calculus without the cut rule

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

science china(Information sciences) 2011年第12期54卷 2550-2563页

作者： luo jie & li wei state key laboratory of software development environment, school of computer science and Engineering, beihang university, beijing 100191, china state key laboratory of software development environment School of Computer Science and Engineering Beihang University Beijing China

R-calculus is an inference system for deducing all possible changes when a theory is refuted by the facts. In this paper, we try to eliminate the cut rule in R-calculus by modifying the existing rules and by introducing new rules. The result is the R-calculus without the cut rule, which still preserves the reachability, soundness and completeness as R-calculus does. R-calculus without the cut rule is a formal inference system of logical connective symbols and quantifier symbols solely. It can serve as the theoretical foundation of the automation of revision calculus.

关键词： revision R-calculus cut rule

A formal semantics for debugging synchronous message passing-based concurrent programs

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

science china(Information sciences) 2014年第12期57卷 198-215页

作者： li He luo jie li wei state key laboratory of software development environment School of Computer Science and EngineeringBeihang University

In this paper,we propose a semantic framework to debug synchronous message passing-based concurrent programs,which are increasingly useful as parallel computing and distributed systems become more and more *** first design a concurrent programming language model to uniformly represent existing concurrent programming *** to sequential programming languages,this model contains communication statements,i.e.,sending and receiving statements,and a concurrent structure to represent communication and *** then propose a debugging process consisting of a tracing and a locating *** tracing procedure re-executes a program with a failed test case and uses specially designed data structures to collect useful execution information for locating *** provide for the tracing procedure a structural operational semantics to represent synchronous communication and *** locating procedure backward locates the ill-designed statement by using information obtained in the tracing procedure,generates a fix equation,and tries to fix the bug by solving the fix *** also propose a structural operational semantics for the locating *** supply two examples to test our proposed operational semantics.

关键词： debugging synchronous message passing concurrent program operational semantics

Contrary description logic: Gentzen deduction system

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

science china(Information sciences) 2017年第11期60卷 171-179页

作者： wei li Yuefei SUI jie luo Bo CHEN state key laboratory of software development environment Beihang University key laboratory of Intelligent Information Processing Institute of Computing TechnologyChinese Academy of Sciences

Traditional description logics are based on complementary rather than contrary concepts. This work proposes a contrary description logic based on the contrary concept constructors ～, ?(instead of ?).A Gentzen-type deduction system is applied to make the system sound and complete with the three-valued semantics of contrary description logic.

关键词： description logics contradictory contrary soundness completeness

A decomposition based algorithm for maximal contractions

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

Frontiers of computer science 2013年第6期7卷 801-811页

作者： Dongchen JIANG wei li jie luo Yihua LOU Zhengzhong liAO state key laboratory of computer Architecture Institute of Computing Technology Chinese Academy of Sciences Beijing 100190 China state key laboratory of software development environment Beihang University Beijing 100191 China Tencent technology (beijing) Company limited Beijing 100080 China

This paper proposes a decomposition based algo- rithm for revision problems in classical propositional logic. A set of decomposing rules are presented to analyze the satis- fiability of formulas. The satisfiability of a formula is equivalent to the satisfiability of a set of literal sets. A decomposing function is constructed to calculate all satisfiable literal sets of a given formula. When expressing the satisfiability of a formula, these literal sets are equivalent to all satisfied models of such formula. A revision algorithm based on this decomposing function is proposed, which can calculate maximal contractions of a given problem. In order to reduce the memory requirement, a filter function is introduced. The improved algorithm has a good performance in both time and space perspectives.

关键词： belief change maximal contraction decomposing rules revision algorithm

在线全文

学校读者我要写书评

暂无评论

KENN:线性结构熵的图核神经网络

软件学报 2024年第5期35卷 2430-2445页

作者：徐立祥许巍陈恩红罗斌唐远炎合肥大学人工智能与大数据学院安徽合肥230601 中国科学技术大学计算机科学与技术学院安徽合肥230027 认知智能全国重点实验室安徽合肥230088 安徽大学计算机科学与技术学院安徽合肥230601 澳门大学珠海澳大科技研究院中国澳门999078

图神经网络(graph neural network,GNN)是一种利用深度学习直接对图结构数据进行表征的框架,近年来受到人们越来越多的关注.然而传统的基于消息传递聚合的图神经网络(messaging passing GNN,MP-GNN)忽略了不同节点的平滑速度,无差别地... 详细信息

图神经网络(graph neural network,GNN)是一种利用深度学习直接对图结构数据进行表征的框架,近年来受到人们越来越多的关注.然而传统的基于消息传递聚合的图神经网络(messaging passing GNN,MP-GNN)忽略了不同节点的平滑速度,无差别地聚合了邻居信息,易造成过平滑现象.为此,研究并提出一种线性结构熵的图核神经网络分类方法,即KENN.它首先利用图核方法对节点子图进行结构编码,判断子图之间的同构性,进而利用同构系数来定义不同邻居间的平滑系数.其次基于低复杂度的线性结构熵提取图的结构信息,加深和丰富图数据的结构表达能力.通过将线性结构熵、图核和图神经网络三者进行深度融合提出了图核神经网络分类方法.它不仅可以解决生物分子数据节点特征的稀疏问题,也可以解决社交网络数据以节点度作为特征所产生的信息冗余问题,同时还使得图神经网络能够自适应调整对图结构特征的表征能力,使其超越MP-GNN的上界(WL测试).最后,在7个公开的图分类数据集上实验验证了所提出模型的性能优于其他的基准模型.

关键词：图分类结构熵图核消息传递聚合图神经网络

一种基于指向路径分次删剪的移动Agent通信算法

在线全文

学校读者我要写书评

暂无评论

计算机科学 2004年第1期31卷 20-24页

作者：贾志勇罗杰王德强谢立南京大学计算机系软件新技术国家重点实验室南京210093 南京大学计算机科学与技术系南京210093

在移动agent环境下,agent的移动为应用程序的开发提供了更灵活的通信处理方式,但也同时对通信算法的设计提出了许多挑战,其中最突出的就是由于消息传输和agent移动之间的异步性而造成的通信不可靠问题。针对目前解决该问题的各种机制和... 详细信息

在移动agent环境下,agent的移动为应用程序的开发提供了更灵活的通信处理方式,但也同时对通信算法的设计提出了许多挑战,其中最突出的就是由于消息传输和agent移动之间的异步性而造成的通信不可靠问题。针对目前解决该问题的各种机制和算法的不足之处,该文提出了一种新的agent通信算法—S_COMP,它综合采用了Home寻址、途经节点转发、指向路径分次删剪和集中同步等手段,能够适应具有不同移动和通信特点的agent的通信需要,在确保消息传输可靠性的同时兼顾了效率和适应性。

关键词：移动Agent通信算法应用程序异步性可靠性适应性

在线全文

学校读者我要写书评

暂无评论

WiFense:从衍射模型到边界监控

软件学报 2024年第3期35卷 1515-1533页

作者：刘兆鹏李晟洁张越曾有为张大庆北京大学信息科学技术学院北京100871 高可信软件技术教育部重点实验室(北京大学) 北京100871

近年来,随着普适计算概念的深入人心,智能感知技术已成为研究者们关注的焦点,且基于WiFi的非接触式感知因其优秀的普适性、低廉的部署成本以及良好的用户体验越来越受到学术界和工业界的青睐.典型的WiFi非接触式感知工作有手势识别、呼... 详细信息

近年来,随着普适计算概念的深入人心,智能感知技术已成为研究者们关注的焦点,且基于WiFi的非接触式感知因其优秀的普适性、低廉的部署成本以及良好的用户体验越来越受到学术界和工业界的青睐.典型的WiFi非接触式感知工作有手势识别、呼吸检测、入侵检测、行为识别等,这些工作若实际部署,需首先避免其他无关区域中无关行为的干扰,因此需要判断目标是否进入到特定的感知区域中.这意味着系统应具备精准判断目标在界线哪一侧的能力,然而现有工作未能找到一个可以对某个自由设定的边界进行精确监控的方法,这阻碍了WiFi感知应用的实际落地.基于这一关键问题,从电磁波衍射的物理本质出发,结合菲涅尔衍射模型(Fresnel diffraction model),找到一种目标穿越link(收发设备天线的连线)时的信号特征(Rayleigh distribution in Fresnel diffraction model,RFD),并揭示该信号特征与人体活动之间的数学关系;之后以link作为边界,结合天线间距带来的波形时延以及AGC(automatic gain control)在link被遮挡时的特征,通过越线检测实现对边界的监控.在此基础上,还实现了两个实际应用,即入侵检测系统和居家状态监测系统,前者的精确率超过89%、召回率超过91%,后者的准确率超过89%.在验证所提边界监控算法的可用性和鲁棒性的同时,也展示了所提方法与其他WiFi感知技术相结合的巨大潜力,为WiFi感知技术的实际部署提供了思考方向.

关键词：非接触式感知 WiFi 信道状态信息(CSI) link穿越检测边界监控

A representative model based algorithm for maximal contractions

在线全文

学校读者我要写书评

暂无评论

science china(Information sciences) 2013年第1期56卷 5-17页

作者： JIANG DongChen LOU YiHua JIN Yi luo jie li wei state key laboratory of software development environment Beihang University IBM china Company limited IBM China Development Laboratory

In this paper,we propose a representative model based algorithm to calculate maximal *** a formal theory Γ and a fact set Δ,the algorithm begins by accepting all models of refutation by facts of Γ with respect to Δ and filters these models to obtain the models of *** to the completeness of R-calculus,the relevant maximal contraction is obtained *** order to improve the efficiency,we divide the models into different classes according to the assignments of atomic propositions and only select relevant representative models to verify the satisfiability of each *** algorithm is correct,and all maximal contractions of a given problem can be calculated by *** could make a selection according to their requirements.A benchmark algorithm is also *** show that the algorithm has a good performance on normal revision problems.

关键词： revision calculus maximal contraction belief change assignment equivalence class representative model

Quality assessment in competition-based software crowdsourcing

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

Frontiers of computer science 2020年第6期14卷 17-30页

作者： Zhenghui HU Wenjun WU jie luo Xin WANG Boshu li state key laboratory of software development environment Beihang UniversityBeijing 100191China

Quality assessment is a critical component incrowdsourcing-based software engineering(CBSE)as soft-ware products arc developed by the crowd with unknownor varied skills and *** this *** proposea novel metric called the project score to measure the perfor-mance of projects and the quality of products for compctition-based software crowdsourcing devclopment(CBSCD)*** the best of our knowledge,this is the first work to deal with the quality issue of CBSE in the perspective ofprojccts instead of *** particular,we develop a hi-crarchical quality evaluation framework for CBSCD projects and come up with two metric aggregatibn modcls for *** first model is a modified squale model that canlocate the sofiware modules of poor quality,and the secondone is a clustering-based aggregation model,which takes dif-ferent impacts of phases into *** test the effective-ness of the proposed *** conduct an empirical studyon TopCoder,which is a famous CBSCD *** that the proposed project score is a strong indicator ofthe performance and product quality of CBSCD *** find that the clustering-based aggregation model outpcr-forms the Squale one by increasing the percentage of the per-formance evaluation criterion of aggregation models by anadditional 29%.Our approach to quality assessment for CB-sCD projects could potentially facilitate software managersto assess the overall quality of a crowdsourced project con-sisting of programming contests.

关键词： crowdsourcing software engineering.productquality.competition evaluation framework metric aggregation