2TLCGPOWA算子及其在多属性群决策中的应用

基于集对分析理论中二元联系数的不确定性,将联系变量引入到区间二元语义环境中,定义了二元语义联系变量,给出了二元语义联系变量的运算法则,并提出了几种新的算术集结算子。针对决策矩阵元素为区间二元语义变量和属性权重完全未知的不确定多属性群决策问题,提出了一种基于2TLCGPOWA算子的不确定多属性群决策方法。最后通过对某大学教师的任职和晋升考核来说明该方法的可行性和有效性。     

纯语言多属性群决策方法研究

研究了属性权重、属性值以及专家权重均以语言形式给出的纯语言多属性群决策问题．定义了语言评估标度的运算法则，给出了一些基于语言评估标度及其运算法则的新算子，提出了一种纯语言多属性群决策方法．该法不但计算简洁便利，而且能充分地利用已有的语言决策信息．最后将该方法应用于解决供应链管理领域中的战略合作伙伴选择问题．     

基于二元联系数集结算子的多准则群决策方法

定义了二元联系数的加性运算法则, 给出了几种新的算术集结算子, 即二元联系数加权算术平均(BCNWAA)算子、二元联系数有序加权平均(BCNOWA) 算子和二元联系数混合集结(BCNHA) 算子, 提出了一种基于二元联系数的准则权重信息不完全确定的群决策方法. 该方法利用BCNWAA算子和BCNHA算子对二元联系数准则值进行集结; 利用二元联系数准则值的方差和准则权重的随机性, 通过构建优化模型确定最优准则权重. 最后, 通过实例分析表明了该方法的可行性和有效性.

     

区间直觉模糊信息的集成方法及其在决策中的应用

对区间直觉模糊信息的集成方法进行了研究.定义了区间直觉模糊数的一些运算法则,并基于这些运算法则,给出区间直觉模糊数的加权算术和加权几何集成算子.定义了区间直觉模糊数的得分函数和精确函数,进而给出了区间直觉模糊数的一种简单的排序方法.最后提供了一种基于区间直觉模糊信息的决策途径,并进行了实例分析.     

基于概率犹豫模糊信息集成算法的数据产品选择

作为犹豫模糊元的推广形式，概率犹豫模糊元能更好地刻画现实中的不确定性，此外由于Frank运算具有含参数的灵巧性，能反映决策者的主观偏好，因此将概率犹豫模糊元和Frank运算相结合，首先定义了概率犹豫模糊Frank运算法则，并提出改进的概率犹豫模糊元的得分函数；然后提出了概率犹豫模糊Frank加权平均算子，并讨论了算子的一些性质；在此基础上，构建了基于概率犹豫模糊Frank加权平均算子的多属性群决策方法；最后将其应用于数据产品的选择实例中，说明了该方法的有效性和可行性。     

一种新型的航空图像城区建筑物自动提取方法

提出了一种新的从航空城区图像中自动提取矩形建筑物的方法．该方法基于从航空城区图像中提取的边缘，经过轮廓跟踪，采用Splitting方法提取直线，得出其相应的直线几何图形；针对航空图像的复杂及现有边缘检测算法的不足，提出了一系列直线处理的方法(如直线的分类、排序、合并、调整等)有效地弥补了前述处理的不足；为提高矩形房屋提取的准确率，引入知识定义了几种近似的矩形结构．文章采用几何结构元分析的方法，提取图形中构成矩形的各种基本结构元，再根据结构元合并的准则，将各种基本结构元通过一定的合并算法合并成矩形结构．大量试验结果证明该方法提取矩形房屋的准确率较高，鲁棒性好，运算速度快，具有较强的实际应用价值．     

区间直觉模糊几何Bonferroni平均算子及其应用

研究了决策信息为区间直觉模糊数（IVIFN）且属性间存在相互关联的多属性群决策（MAGDM）问题,提出一种基于区间直觉模糊几何加权Bonferroni平均（IVIFGWBM）算子的决策方法。介绍了IVIFN的概念和运算法则,基于这些运算法则和几何Bonferroni平均（GBM）算子,定义了区间直觉模糊几何Bonferroni平均（IVIFGBM）算子和IVIFGWBM算子。研究了这些算子的一些性质,建立基于IVIFGWBM算子的MAGDM模型,结合排序方法进行决策。将该方法应用在一个MAGDM问题中,结果表明了该方法的有效性与可行性。     

多核环境下Hilbert曲线划分简单要素多边形合并算法

为了解决大规模复杂多边形数据合并运算效率问题,减少在空间数据库中检索多边形时的磁盘读取次数,针对多核环境下简单要素类多边形合并的特点,利用Hilbert曲线划分方法对简单要素的多边形进行空间数据划分,利用多核处理器并发执行,充分利用了多核计算环境中CPU的计算能力,保证了合理的任务分配与充分利用。介绍了该算法中用到的简单要素类多边形合并算子,利用对重合边的判断来进行多边形的合并;最后对提出的算法进行了实验分析。实验证明,本算法在进行大数据的多边形集合合并时效率较高,基于本算法开发的功能用于实际问题中可较好地解决大规模复杂多边形数据层合并运算的效率问题。     

算子Rough逻辑及其归结原理

本文基于Rough集理论定义了算子η及其合成运算，并用它作用于Rough逻辑公式，从而得到了带算子的Rough逻辑．讨论了这种逻辑公式的真值、语义模型、性质、归结原理及完备性定理和它的证明．     

犹豫模糊EWAA算子及其多属性决策方法

犹豫模糊信息集结是犹豫模糊集理论中的重要组成部分,近年来由于其越来越受到关注,已成为一个新的研究方向。基于Einstein运算定义了犹豫模糊元间的运算法则,比如:Einstein和、Einstein积以及Einstein幂运算。提出了三种新的Einstein算术平均集结算子,即犹豫模糊Einstein加权平均(HFEWA)算子、犹豫模糊Einstein有序加权平均(HFEOWA)算子以及犹豫模糊Einstein混合平均(HFEHA)算子。基于新的Einstein算术平均集结算子给出一种新的处理犹豫模糊环境下多属性决策问题的方法,并结合实例对决策方法的可行性与有效性进行检验。     

基于函数式语义的循环和递归程序结构通用证明技术

各类安全攸关系统的可靠运行离不开软件程序的正确执行.程序的演绎验证技术为程序执行的正确性提供高度保障.程序语言种类繁多,且用途覆盖高可靠性场景的新式语言不断涌现,难以为每种语言设计支撑其程序验证任务的整套逻辑规则,并证明其相对于形式语义的可靠性和完备性.语言无关的程序验证技术提供以程序语言的语义为参数的验证过程及其可靠性结果.对每种程序语言,提供其形式语义后可直接获得面向该语言的程序验证过程.提出一种面向大步操作语义的语言无关演绎验证技术,其核心是对不同语言中循环、递归等可导致无界行为的语法结构进行可靠推理的通用方法.特别地,借助大步操作语义的一种函数式形式化提供表达程序中子结构所执行计算的能力,从而允许借助辅助信息对子结构进行推理.证明所提出验证技术的可靠性和相对完备性,通过命令式、函数式语言中的程序验证实例初步评估了该技术的有效性,并在Coq辅助证明工具中形式化了所有理论结果和验证实例,为基于辅助证明工具实现面向大步语义的语言无关程序验证工具提供了基础.     

Coq Formalization of ZFC Set Theory for Teaching Scenarios

Discrete mathematics is a foundation course for computer-related majors, and propositional logic, first-order logic, and the axiomatic set theory are important parts of this course. Teaching practice shows that beginners find it difficult to accurately understand abstract concepts, such as syntax, semantics, and reasoning system. In recent years, some scholars have begun introducing interactive theorem provers into teaching to help students construct formal proofs so that they can understand logic systems more thoroughly. However, directly employing the existing theorem provers will increase students'' learning burden since these tools have a high threshold for getting started with them. To address this problem, we develop a prover for the Zermelo-Fraenkel set theory with the axiom of Choice (ZFC) in Coq for teaching scenarios. Specifically, the first-order logical reasoning system and the axiomatic set theory ZFC are formalized, and several automated proof tactics specific to reasoning rules are then developed. Students can utilize these automated proof tactics to construct formal proofs of theorems in a textbook-style concise proving environment. This tool has been introduced into the teaching of the course of discrete mathematics for freshmen. Students with no prior theorem-proving experience can quickly construct formal proofs of theorems including mathematical induction and Peano arithmetic with this tool, which verifies the practical effectiveness of this tool.     

A new bidding framework for combinatorial e-auctions

Bidding languages define the means through which participants in an electronic auction define bids and express requirements on their execution. The current state of combinatorial auction market design indicates that no existing bidding language is general enough to support auctions of both divisible and indivisible commodities. In this paper, we propose a novel bidding framework based on a two-level representation of a combined bid. At the inner level, bidding operators impose conditions on the executed proportions of packages of atomic single-item bids. Partial bids defined this way are then recursively combined through logical operators to produce a final combined bid that is submitted to the auctioneer. We present a formal specification of the framework, and analyze how it impacts the mathematical programming formulation of the allocation problem. An application in the context of combinatorial auctions of financial assets illustrates the utilization of the proposed bidding framework.     

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

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

Formal verification of Ada programs

The Penelope verification editor and its formal basis are described. Penelope is a prototype system for the interactive development and verification of programs that are written in a rich subset of sequential Ada. Because it generates verification conditions incrementally, Penelope can be used to develop a program and its correctness proof in concert. If an already-verified program is modified, one can attempt to prove the modified version by replaying and modifying the original sequence of proof steps. Verification conditions are generated by predicate transformers whose logical soundness can be proven by establishing a precise formal connection between predicate transformation and denotational definitions in the style of continuation semantics. Penelope's specification language, Larch/Ada, belongs to the family of Larch interface languages. It scales up properly, in the sense that one can demonstrate the soundness of decomposing an implementation hierarchically and reasoning locally about the implementation of each node in the hierarchy     

Foundations for object-oriented query processing

A minimal framework for an object-oriented query language standard should (1) include a formal definition of a high-level data model and the syntax and semantics of associated query languages, (2) provide the functionality of relational query languages, and (3) support proofs of correctness of transformations for logical query optimization. In this paper, a high-level conceptual model for object-oriented query processing is discussed; the model includes widely-used structural abstractions such as the isa relationship, associations (properties) between complex objects and complex objects/values, and inheritance of properties. A formal, algebraic query language for the model, inspired by relational algebra, is presented. Operators of the algebra allow queries based on values, queries that manipulate entire objects, and queries that construct new objects from existing objects/values. All queries retain connections to existing database objects, providing logical access paths to data. Each query result is a class, so the algebra has the closure property. The intensional and extensional results of query operators are summarized. Two forms of logical query optimization supported by the query algebra are outlined: algebraic transformations and classifier-based optimizations (optimizations which employ inclusion and exclusion dependencies between classes).