A Decision Procedure for a Sublanguage of Set Theory Involving Monotone, Additive, and Multiplicative Functions, I: The Two-Level Case

2LS is a decidable many-sorted set-theoretic language involving one sort for elements and one sort for sets of elements. In this paper we extend 2LS with constructs for expressing monotonicity, additivity, and multiplicativity properties of set-to-set functions. We call the resulting language 2LSmf. We prove that 2LSmf is decidable by reducing the problem of determining the satisfiability of its sentences to the problem of determining the satisfiability of sentences of 2LS. Furthermore, we prove that the language 2LSmf is stably infinite with respect to the sort of elements. Therefore, by using a many-sorted version of the Nelson–Oppen combination method, 2LSmf can be combined with other languages modeling the sort of elements.     

A Tableau-Based Decision Procedure for a Fragment of Set Theory with Iterated Membership

MLSS is a decidable fragment of set theory involving the predicates membership and set equality and the operators union, intersection, set difference, and singleton. In this paper we extend MLSS with the iterated membership predicate, that is, with a predicate denoting the transitive closure of the membership relation. We call the resulting language MLSS⁺. We prove that MLSS⁺ is decidable by providing a decision procedure for it based on Smullyan semantic tableaux. As an application of our results, we show how our decision procedure can be used as a black box in order to allow an interactive theorem prover to verify some basic properties of the ordinal numbers.This research was in part supported by murst grant prot. 2001017741 under the Italian project Ragionamento su aggregati e numeri a supporto della programmazione e relative verifiche.     

Probabilistic Constrained MPC for Multiplicative and Additive Stochastic Uncertainty

The technical note develops a receding horizon control strategy to guarantee closed-loop convergence and feasibility in respect of soft constraints. Earlier results addressed the case of multiplicative uncertainty only. The present technical note extends these to the more general case of additive and multiplicative uncertainty and proposes a method of handling probabilistic constraints. The results are illustrated by a simple design study considering the control of a wind turbine.      

基于粗糙的属性约简在企业客户优惠决策中的应用

粗糙集理论是近代新兴的数据处理方法,在对粗糙集理论的一些算法研究后,提出了用其解决企业中大量数据中获取的较优决策,为企业信息系统的决策支持提供新的解决方法。     

应用于PHM系统的相近粗糙集决策模型研究

PHM(Prognostic and Health Management)是现代军事和工业生产领域设备实现自主维护与保障的关键技术。文章通过对相近粗糙集理论进行分析,构建一个可以应用于PHM系统的决策模型。以某歼击机的故障飞行信息作为测试数据,在加入噪声干扰和不加噪声干扰的条件下,对经典粗糙集理论,可变精度粗糙集理论以及相近粗糙集理论的决策结果进行比较。结果表明在保持分类性能不变的条件下,相近粗糙集理论对含有噪声系统的适应性要好于经典粗糙集理论和可变精度的粗糙集理论,适合运用于PHM系统的决策算法。     

A Locally Gradient-Preserving Reinitialization for Level Set Functions

The level set method commonly requires a reinitialization of the level set function due to interface motion and deformation. We extend the traditional technique for reinitializing the level set function to a method that preserves the interface gradient. The gradient of the level set function represents the stretching of the interface, which is of critical importance in many physical applications. The proposed locally gradient-preserving reinitialization (LGPR) method involves the solution of three PDEs of Hamilton–Jacobi type in succession; first the signed distance function is found using a traditional reinitialization technique, then the interface gradient is extended into the domain by a transport equation, and finally the new level set function is found by solving a generalized reinitialization equation. We prove the well-posedness of the Hamilton–Jacobi equations, with possibly discontinuous Hamiltonians, and propose numerical schemes for their solutions. A subcell resolution technique is used in the numerical solution of the transport equation to extend data away from the interface directly with high accuracy. The reinitialization technique is computationally inexpensive if the PDEs are solved only in a small band surrounding the interface. As an important application, we show how the LGPR procedure can be used to make possible the local level set approach to the Eulerian Immersed boundary method.     

An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types

The theory of recursive data types is a valuable modeling tool for software verification. In the past, decision procedures have been proposed for both the full theory and its universal fragment. However, previous work has been limited in various ways. In this paper, we present a general algorithm for the universal fragment. The algorithm is presented declaratively as a set of abstract rules which are terminating, sound, and complete. We show how other algorithms can be realized as strategies within our general framework. Finally, we propose a new strategy and give experimental results showing that it performs well in practice.     

基于粗集的属性约简在电信企业决策中的应用

粗糙集理论是近代新兴的一种研究不完整、不确定知识和数据的表达、学习、归纳的理论方法.在对粗集理论的一些算法研究后,提出了用其解决电信企业中大量数据中获取的较优决策,为企业信息系统的决策支持提供新的解决方法.     

用粗糙集理论建立决策树的一种方法

在数据挖掘中,分期是一个很重要的问题,有很多流行的分类器可以创建决策树木产生类模型。本文介绍了通过信息增益或熵的比较来构造一棵决策树的数桩挖掘算法思想,给出了用粗糙集理论构造决策树的一种方法,并用曲面造型方面的实例说明了决策树的生成过程。通过与ID3方法的比较,该种方法可以降低决策树的复杂性,优化决策树的结构,能挖掘较好的规则信息。     

粗描述逻辑RALCQ的Tableau推理

基于描述逻辑ALCQ,通过引入分级近似算子而得到粗描述逻辑RALCQ。随后通过转换的方法得到粗描述逻辑RALCQ的Tableau算法推理规则及推理复杂性。     

基于粗糙集理论分析的学习过程评价模型

本文基于粗糙集理论,提出了一个面向学习过程的评价模型.该模型从已有的数据出发,对学习过程中的诸多因素进行约简,去除其中不必要的因素,发现影响学习效果的关键因素及各种因素之间的关联规则,并利用这些规则对学习者的学习过程进行评价.     

Extended Decision Procedure for a Fragment of HL with Binders

This work is a brief presentation of an extension of the proof procedure for a decidable fragment of hybrid logic presented in a previous paper. It shows how to extend such a calculus to multi-modal logic enriched with transitivity and relation inclusion assertions. A further result reported in this work is that the logic extending the considered fragment with the addition of graded modalities has an undecidable satisfiability problem, unless further syntactical restrictions are placed on their use.     

基于粗糙集理论的智能决策支持系统

本文着重介绍了基于粗糙集理论的智能决策支持系统的总体结构及其各个模块的功能。首先介绍了智能决策支持系统产生的背景．即人工智能技术和决策支持相结合而产生的。粗糙集理论是研究不完整、不确定知识并口．数据的表达、学习、归纳的理论和方法，适合于发现数据中隐含的、潜在有用的规律，即知识，找出其内部数据的关联关系和特征，因此在智能决策支持系统中发挥着重要作用。     

粗糙集和决策树方法在IDS中的应用研究

人侵检测系统(IDS)是数据挖掘的一个热门应用领域.为了解决当前建立的入侵检测系统缺少有效性的问题,文中首先介绍入侵检测系统产生的背景和入侵检测系统的特点,分析决策树归纳学习的过程,从数据挖掘的角度,首先使用粗糙集进行属性约简,运用决策树学习方法对入侵检测数据进行归纳学习.从结果看出粗糙集和决策树学习方法在建立入侵检测系统上的有效性和实用性.     

A Decision Procedure for Linear “Big O” Equations

Let F be the set of functions from an infinite set, S, to an ordered ring, R. For f, g, and h in F, the assertion f = g + O(h) means that for some constant C, |f(x) − g(x)| ≤C |h(x)| for every x in S. Let L be the first-order language with variables ranging over such functions, symbols for 0, +, −, min , max , and absolute value, and a ternary relation f = g + O(h). We show that the set of quantifier-free formulas in this language that are valid in the intended class of interpretations is decidable and does not depend on the underlying set, S, or the ordered ring, R. If R is a subfield of the real numbers, we can add a constant 1 function, as well as multiplication by constants from any computable subfield. We obtain further decidability results for certain situations in which one adds symbols denoting the elements of a fixed sequence of functions of strictly increasing rates of growth.     

粗糙集和决策树方法在IDS中的应用研究

入侵检测系统（IDS）是数据挖掘的一个热门应用领域。为了解决当前建立的入侵检测系统缺少有效性的问题，文中首先介绍入侵检测系统产生的背景和入侵检测系统的特点，分析决策树归纳学习的过程，从数据挖掘的角度，首先使用粗糙集进行属性约简，运用决策树学习方法对入侵检测数据进行归纳学习。从结果看出粗糙集和决策树学习方法在建立入侵检测系统上的有效性和实用性。     

A Decision Procedure for (Co)datatypes in SMT Solvers

We present a decision procedure that combines reasoning about datatypes and codatatypes. The dual of the acyclicity rule for datatypes is a uniqueness rule that identifies observationally equal codatatype values, including cyclic values. The procedure decides universal problems and is composable via the Nelson–Oppen method. It has been implemented in CVC4, a state-of-the-art SMT solver. An evaluation based on problems generated from formalizations developed with Isabelle demonstrates the potential of the procedure.