Knowledge representation using fuzzy deduction graphs

A new knowledge representation model, known as fuzzy deduction graph (FDG), is introduced in this paper. An FDG can represent a knowledge base containing the fuzzy propositions and fuzzy rules. In an FDG, a systematic method of finding the fuzzy reasoning path (FRP) is given which is based on Dijkstra's shortest path framework. The FRP gives a relationship between the antecedent (source) proposition and consequent (goal) proposition, such that the consequent proposition is reached with the greatest fuzzy value. The process of finding the FRP is illustrated with examples.     

Solving quantified verification conditions using satisfiability modulo theories

First-order logic provides a convenient formalism for describing a wide variety of verification conditions. Two main approaches to checking such conditions are pure first-order automated theorem proving (ATP) and automated theorem proving based on satisfiability modulo theories (SMT). Traditional ATP systems are designed to handle quantifiers easily, but often have difficulty reasoning with respect to theories. SMT systems, on the other hand, have built-in support for many useful theories, but have a much more difficult time with quantifiers. One clue on how to get the best of both worlds can be found in the legacy system Simplify which combines built-in theory reasoning with quantifier instantiation heuristics. Inspired by Simplify and motivated by a desire to provide a competitive alternative to ATP systems, this paper describes a methodology for reasoning about quantifiers in SMT systems. We present the methodology in the context of the Abstract DPLL Modulo Theories framework. Besides adapting many of Simplify’s techniques, we also introduce a number of new heuristics. Most important is the notion of instantiation level which provides an effective mechanism for prioritizing and managing the large search space inherent in quantifier instantiation techniques. These techniques have been implemented in the SMT system CVC3. Experimental results show that our methodology enables CVC3 to solve a significant number of quantified benchmarks that were not solvable with previous approaches.     

Accelerating temporal verification of Simulink diagrams using satisfiability modulo theories

Automatic verification of programs and computer systems with input variables represents a significant and well-motivated challenge. The case of Simulink diagrams is especially difficult, because there the inputs are read iteratively, and the number of input variables is in theory unbounded. We apply the techniques of explicit model checking to account for the temporal (control) aspects of verification and use set-based representation of data, thus handling both sources of non-determinism present in the verification. Two different representations of sets are evaluated in scalability with respect to the range of input variables. Explicit (enumerating) sets are very fast for small ranges but fail to scale. Symbolic sets, represented as first-order formulas in the bit-vector theory and compared using satisfiability modulo theory solvers, scale well to arbitrary (though still bounded) range of input variables. To leverage the combined strengths of explicit and symbolic representations, we have designed a hybrid representation which we showed to outperform both pure representations. Thus, the proposed method allows complete automatic verification without the need to limit the non-determinism of input. Moreover, the principle underlying the hybrid representation entails inferring knowledge about the system under verification, which the developers did not explicitly include in the system, and which can significantly accelerate the verification process.     

Video completion using tracking and fragment merging

Video completion is the problem of automatically filling space–time holes in video sequences left by the removal of unwanted objects in a scene. We solve it using texture synthesis, filling a hole inwards using three steps iteratively: we select the most promising target pixel at the edge of the hole, we find the source fragment most similar to the known part of the target’s neighborhood, and we merge source and target fragments to complete the target neighborhood, reducing the size of the hole. Earlier methods were slow, due to searching the whole video data for source fragments or completing holes pixel by pixel; they also produced blurred results due to sampling and smoothing. For speed, we track moving objects, allowing us to use a much smaller search space when seeking source fragments; we also complete holes fragment by fragment instead of pixelwise. Fine details are maintained by use of a graph cut algorithm when merging source and target fragments. Further techniques ensure temporal consistency of hole filling over successive frames. Examples demonstrate the effectiveness of our method.     

Event stream-based process discovery using abstract representations

The aim of process discovery, originating from the area of process mining, is to discover a process model based on business process execution data. A majority of process discovery techniques relies on an event log as an input. An event log is a static source of historical data capturing the execution of a business process. In this paper, we focus on process discovery relying on online streams of business process execution events. Learning process models from event streams poses both challenges and opportunities, i.e. we need to handle unlimited amounts of data using finite memory and, preferably, constant time. We propose a generic architecture that allows for adopting several classes of existing process discovery techniques in context of event streams. Moreover, we provide several instantiations of the architecture, accompanied by implementations in the process mining toolkit ProM (http://promtools.org). Using these instantiations, we evaluate several dimensions of stream-based process discovery. The evaluation shows that the proposed architecture allows us to lift process discovery to the streaming domain.     

Robust tracking-by-detection using a selection and completion mechanism

Computational Visual Media - It is challenging to track a target continuously in videos with long-term occlusion, or objects which leave then re-enter a scene. Existing tracking algorithms combined...     

Intelligent backtracking in plan-based deduction

This paper develops a method of mechanical deduction based on a graphical representation of the structure of proofs. Attempts to find a refutation(s) are recorded in the form of plans, corresponding to portions of an AND/OR graph search space and representing a purely deductive structure of derivation. This method can be applied to any initial base (set of nonnecessarily Horn clauses). Unlike the exhaustive (blind) backtracking which treats all the goals deduced in the course of a proof as equally probable sources of failure, his approach detects the exact source of failure. Only a small fragment of the solution space is kept on disk as a collection of pairs, each of which consists of a plan and a graph of constraints. The search strategy and the method of nonredundant processing of individual pairs which leads to a solution (if it exists) is presented. This approach is compared?on a special case?with a blind backtracking algorithm for which an exponential improvement is demonstrated. Some important implementation problems are discussed, and toplevel design of a mechanical deduction system implementing our algorithm is presented. It is proven that the algorithm is complete in the following sense: if for a given base a resolution refutation exists, then this refutation is found by the algorithm.     

Investigation of tritrophic interactions in an ecosystem using abstract chemistry

We investigated the population dynamics of a tritrophic interaction mediated by herbivore-induced plant volatiles that attracted carnivorous natural enemies of herbivores. We modeled the system by abstract chemistry, and an abstract rewriting system of multisets (ARMS), and compared the case where plants produced herbivore-induced volatiles with the case where they did not. We found that there was a case where herbivore-induced volatiles that attract carcivores resulted in a population increase of herbivores. This work was presented, in the Sixth International Symposium on Artificial Life and Robotics, Tokyo, Japan, January 15–17, 2001     

递推公式计算精馏塔的理论塔板数

阐述递推公式的推导过程,介绍如何和Excel函数及公式计算精馏塔理论塔板数的气-液相组成,使多媒体教学中的化工计算过程实现了图形化、可视化及自动化.其Excel逐板计算和Excel图解计算方法易于掌握,对于处理类似的化工计算有一定的参考作用.     

使用图割方法提取图像的纹理特征

研究目的是对代数多重网格（AMG）方法进行分析,粗网格中会保留强连接部分而去掉弱连接部分,可以提取图像的纹理信息。将AMG方法提取的图像的纹理特征结合到图分割算法中,针对具有纹理特征的图片构建能量函数,并使用最大流方法进行优化。使用一些自然图像进行了验证,结果证明针对该方法能够较好地提取图像的纹理特征。     

一种基于本体的抽象度可调文档聚类

文档聚类随着网上文本数量的激增以及实际应用中的需求,引起了人们广泛的关注。针对目前文档聚类的主要缺陷,提出了一种新的基于本体的抽象度可调文档聚类（Adjustable Text Clustering using Abstract Degree of Concept,ATCADC）。该方法采用Wordnet对VSM特征词进行概念映射和消歧处理,利用生成的特征概念实现文档语义层面上的矢量描述,并在二次特征选择的基础上,完成合成聚类（AHC）。方法能够依据用户设定的概念抽象度,借助专门设计的语义中心矢量调节聚类,还可利用关键特征概念对聚类簇进行解释。实验结果证明,聚类精度高,聚类簇可解释,调节效果有效,能够满足用户不同概念抽象度层次上的聚类。     

Program-substitution and admissibility of rules in algorithmic logic

Summary The purpose of this work is to show a point of view upon the notions of program-substitution and admissibility of rules which are the tools for proving properties of programs of algorithmic logic and the so-called extended algorithmic logic with quantifiers and with non-deterministic programs. We prove that the set of theses of algorithmic logic is closed under each program-substitution. This substitution rule allows us to formulate a problem of algorithmic structural completeness as a question about derivability of all structural, finitary and admissible rules. We prove the incompleteness of algorithmic logic strengthened by the substitution rule and its algorithmically structural completeness. This work was supported by the Polish Academy of Sciences CPBP 08–15.     

Specialisation of Prolog and FCP programs using abstract interpretation

This paper presents an approach to specialising logic programs which is based on abstract interpretation. Program specialisation involves two stages, the construction of an abstract computation tree and a program construction stage. For the tree construction stage, abstract OLDT resolution is defined and used to construct a complete and finite tree corresponding to a given logic program and a goal. In the program construction stage, a specialised program is extracted from this tree. We focus on two logic programming languages: sequential Prolog and Flat Concurrent Prolog. Although the procedural reading of concurrent logic programs is very different from that of sequential programs, the techniques presented provide a uniform approach to the specialisation of both languages. We present the results for Prolog rigorously, and extend them less formally to Flat Concurrent Prolog. There are two main advantages of basing program specialisation on abstract interpretation. Firstly, termination can be ensured by using abstract interpretations over finite domains, while performing a complete flow analysis of the program. Secondly, correctness of the specialised program is closely related to well-defined consistency conditions on the concrete and abstract interpretations.     

Image completion using prediction concept via support vector regression

Image completion is a widely used method for automatically removing objects or repairing the damaged portions of an image. However, information of the original image is often lacking in reconstructed structures; therefore, images with complex structures are difficult to restore. This study proposes a prediction-oriented image completion mechanism (PICM), which applies the prediction concept to image completion using numerous techniques and methods. The experiment results indicate that under normal circumstances, our PICM not only produces good inpainting quality but it is also easy to use.     

Information cut for clustering using a gradient descent approach

We introduce a new graph cut for clustering which we call the Information Cut. It is derived using Parzen windowing to estimate an information theoretic distance measure between probability density functions. We propose to optimize the Information Cut using a gradient descent-based approach. Our algorithm has several advantages compared to many other graph-based methods in terms of determining an appropriate affinity measure, computational complexity, memory requirements and coping with different data scales. We show that our method may produce clustering and image segmentation results comparable or better than the state-of-the art graph-based methods.     

Texture based segmentation using graph cut and Gabor filters

This paper describes a method for texture based segmentation. Texture features are extracted by applying a bank of Gabor filters using two-sided convolution strategy. Probability texture model is represented by Gaussian mixture that is trained with the Expectation-maximization algorithm. Texture similarity, obtained this way, is used like the input of a Graph cut method. We show that the combination of texture analysis and the Graph cut method produce good results.     

Novel automatic video cut detection technique using Gabor filtering

Video shot transition identification constitutes an important computer vision research field, being applied, as an essential step, in many other digital video analysis domains: video scene detection, video compression, video indexing, video content retrieval and video object tracking. This paper approaches the video cut transition detection domain, providing a novel feature-based automatic identification method. We propose a feature extraction technique that uses 2D Gabor filtering, computing tridimensional image feature vectors for the video frames. Most shot cut detection techniques use a thresholding operation to discriminate between the inter-frame difference metric values and thus identify the video break points. Our identification approach is not threshold-based, using an automatic unsupervised distance classification procedure instead of a threshold. Thus, we provide a region-growing based classification approach, that proves to be very efficient in clustering the distances between feature vectors of consecutive frames. The two resulted distance classes determine a satisfactory video shot detection.