Object-oriented analysis of ELIMINO

ELIMINO is a mathematical research system developed for the implementation of Wu‘s method,a powerful method for polynomial equation system solving and geometric theorem proving.The aim of ELIMINO is to provide user a programmable interpreting environment to use Wu‘s method in scientific research and engineering computation.In this paper,the development of ELIMINO system is outlined and the techniques adopted are discussed,then some details about the aobject-oriented analysis of ELIMINO are presented.     

Eliminating redundant search space on backtracking for forward chaining theorem proving

This paper introduces some improvements on the intelligent backtracking strategy for forward chaining theorem proving. How to decide a minimal useful consequent atom set for a refutation derived at a node in a proof tree is discussed. In most cases, an unnecessary non-Horn clause used for forward chaining will be split only once. The increase of the search space by invoking unnecessary forward chaining clauses will be nearly linear, not exponential anymore.In this paper, the principle of the proposed method and its correctness are introduced. Moreover,some examples are provided to show that the proposed approach is powerful for forward chaining theorem proving.     

Reduction Algorithms Based on Discernibility Matrix：The Ordered Atributes Method

In this Paper,we present reduction algorithms based on the principle of Skowron‘s discernibility matrix-the ordered attributes method.The completeness of the algorithms for Pawlak reduct and the uniqueness for a given order of the attributes are proved.Since a discernibility matrix requires the size of the memory of |U|^2,U is a universe of bojects,it would be impossible to apply these algorithms directly to a massive object set.In order to solve the problem,a so=called quasi-discernibility matrix and two reduction algorithms are prpopsed.Although the proposed algorithms are incomplete for Pawlak reduct,their optimal paradigms ensure the completeness as long as they satisfy some conditions.Finally,we consider the problem on the reduction of distributive object sets.     

RETE网络中的优化编译模式及其PVS形式验证

In the compilation of rule program to the intermediate code-RETE network,optimizing compilation is an important compiler schema,and is a necessary step in the compiler verification.In this paper,we discuss optimization schemas in rule program compilation,and prove the semantic equivalence theorems of these schemas.Firstly,the structure of RETE network and its PVS specification are represented.Secondly,three kinds of optimization schemas are listed.Then algorithms evaluating semantics of target RETE network are given.Finally,we prove the semantic equivalence theorems with theorem prover PVS (Prototype Verification System).     

Formal Derivation of Graph AlgorithmicPrograms Using Partition-and-Recur

In this paper,we derive,by presenting some suitable notations,three typical graph algorithms and corresponding programs using a unified approach,partition-and-recur.We putemphasis on the derivation rather than the algorithms themselves.The main ideas and ingenuity of these algorithms are revealed by formula deduction.Success in these examples gives us more evidence that partition-and-recur is a simple and practical approach and developing enough suitable notations is the key in designing and deriving efficient and correct algorithmic programs.     

Formal Reasoning About Finite-State Discrete-Time Markov Chains in HOL

Markov chains are extensively used in modeling different aspects of engineering and scientific systems, such as performance of algorithms and reliability of systems. Different techniques have been developed for analyzing Markovian models, for example, Markov Chain Monte Carlo based simulation, Markov Analyzer, and more recently probabilistic model-checking. However, these techniques either do not guarantee accurate analysis or are not scalable. Higher-order-logic theorem proving is a formal method that has the ability to overcome the above mentioned limitations. However, it is not mature enough to handle all sorts of Markovian models. In this paper, we propose a formalization of Discrete-Time Markov Chain (DTMC) that facilitates formal reasoning about time-homogeneous finite-state discrete-time Markov chain. In particular, we provide a formal verification on some of its important properties, such as joint probabilities, Chapman-Kolmogorov equation, reversibility property, using higher-order logic. To demonstrate the usefulness of our work, we analyze two applications: a simplified binary communication channel and the Automatic Mail Quality Measurement protocol.     

CAX-A Domestically Developed CAD/CAM System

This paper introduces a domestically developed CAD/CAM system,CAX,which is ableto meet the needs of small and medium sized enterprises.Firstly,the motivations and principles for thedeveloping of the system are presented.Then,the functions and features of CAX are described.In the3rd section,the algorithms for generating blending surfaces with both constant radius and variant radiiare detailed.Six color plates showing the applications of CAX are included in section 4.Finally,dis-cussed are some enhancements being added to CAX in th future.     

Approaches for scaling DBSCAN algorithm to large spatial databases

The huge amount of information stored in datablases owned by coporations(e.g.retail,financial,telecom) has spurred a tremendous interest in the area of knowledge discovery and data mining.Clustering.in data mining,is a useful technique for discovering intersting data distributions and patterns in the underlying data,and has many application fields,such as statistical data analysis,pattern recognition,image processsing,and other business application,s Although researchers have been working on clustering algorithms for decades,and a lot of algorithms for clustering have been developed,there is still no efficient algorithm for clustering very large databases and high dimensional data,As an outstanding representative of clustering algorithms,DBSCAN algorithm shows good performance in spatial data clustering.However,for large spatial databases,DBSCAN requires large volume of memory supprot and could incur substatial I/O costs because it operates directly on the entrie database,In this paper,several approaches are proposed to scale DBSCAN algorithm to large spatial databases.To begin with,a fast DBSCAN algorithm is developed.which considerably speeeds up the original DBSCAN algorithm,Then a sampling based DBSCAN algorithm,a partitioning-based DBSCAN algorithm,and a parallel DBSCAN algorithm are introduced consecutively.Following that ,based on the above-proposed algorithms,a synthetic algorithm is also given,Finally,some experimental results are given to demonstrate the effectiveness and efficiency of these algorithms.     

Kernel Projection Algorithm for Large-Scale SVM Problems

Support Vector Machine (SVM) has become a very effective method in statistical machine learning and it has proved that training SVM is to solve Nearest Point pair Problem (NPP) between two disjoint closed convex sets.Later Keerthi pointed out that it is difficult to apply classical excellent geometric algorithms directly to SVM and so designed a new geometric algorithm for SVM.In this article,a new algorithm for geometrically solving SVM,Kernel Projection Algorithm,is presented based on the theorem on fixed-points of projection mapping.This new algorithm makes it easy to apply classical geometric algorithms to solving SVM and is more understandable than Keerthi‘s.Experiments show that the new algorithm can also handle large-scale SVM problems.Geometric algorithms for SVM,such as Keerthi‘s algorithm,require that two closed convex sets be disjoint and otherwise the algorithms are meaningless.In this article,this requirement will be guaranteed in theory be using the theoretic result on universal kernel functions.     

二进制可辨矩阵的变换及高效属性约简算法的构造

This paper dose a lot of mathematics transformation to Binary Disernibility Matrix,it is called BDM too.Though these transformations,we may both decrease a lot of memory space of BDM and contribute to make high efficiency attributes reduction algorithms.Based on BDM,we also give three algorithms which are in turn used to reduce BDM,attribute‘‘‘‘s reduction and judge reduction.Finally,ew give three examples to illuminate the feasibility of three algorithms and analyze the complexity of algorithms.     

应用吴方法进行高层次定界模型检验

以吴方法为理论基础,提出一种针对高层次设计验证的定界模型检验方法.通过使用多项式等式建模高层次设计和待验证性质,将定界模型检验问题转化为定理证明问题,并用吴方法有效地解决该定理证明问题.实验结果表明,与基于布尔SAT、基于LP的RTL SAT以及基于非线性求解器的性质检验方法相比,该方法在时间消耗上具有相当大的优势.     

基于吴方法的符号模型检验

模型检验技术广泛应用于验证并发系统的性质。它的瓶颈一直是内存爆炸问题,将BDD技术引入到模型检验中的方法能有效地缓和状态组合爆炸问题。然而,随着系统规模的增大,BDD的大小仍呈指数增长。吴方法是一种处理多项式的符号计算方法,能有效地求解代数方程组并成功地应用于几何定理机器证明。给出应用吴方法计算表示Kripke结构和CTL公式的多项式的特征列的方法,从而实现对较大规模的系统性质的验证,进一步缓和状态组合爆炸问题。     

Mathematical Programming Embeddings of Logic

Can theorem proving in mathematical logic be addressed by classical mathematical techniques like the calculus of variations? The answer is surprisingly in the affirmative, and this approach has yielded rich dividends from the dual perspective of better understanding of the mathematical structure of deduction and in improving the efficiency of algorithms for deductive reasoning. Most of these results have been for the case of propositional and probabilistic logics. In the case of predicate logic, there have been successes in adapting mathematical programming schemes to realize new algorithms for theorem proving using partial instantiation techniques. A structural understanding of mathematical programming embeddings of predicate logic would require tools from topology because of the need to deal with infinite-dimensional embeddings. This paper describes the first steps in this direction. General compactness theorems are proved for the embeddings, and some specialized results are obtained in the case of Horn logic.     

超长整数运算的PVS规范与验证

超长整数的运算是现代密码系统的应用基础,运算的正确性关系到密码系统的应用价值。为了验证超长整数算法的设计与需求目标之间的一致性,利用原型验证工具PVS对算法的正确性进行了证明。在介绍了超长整数的加法和减法算法并分析了其设计思想之后,给出了超长整数及其算法的形式规范,通过把算法需要满足的性质描述为定理,将算法的一致性验证问题转化为逻辑定理证明的问题,在PVS定理证明器上完成了相关定理的证明,从而表明这些算法是满足设计需求的。     

基于演化Agent的推理模型

本文描述了一种基于演化 agent的推理模型 ,并用这种推理模型来处理定理机器证明 .传统上 ,定理机器证明常常使用某种逻辑表示 ,然后再进行推理 ,这些方法往往缺乏灵活性 ,且证明过程难以理解 .在本文所叙述的方法中 ,演化 agent能将目标即待证定理分解成越来越小且越来越容易证明的子目标 ,最后完成定理证明 .这种方法非常类似于人类在证明定理时一般所采用的思维方式 ,因而 ,显得更灵活、更具有适应性     

Transcendental functions and mechanical theorem proving in elementary geometries

We present a new approach to dealing with certain problems about trigonometric and hyperbolic function using Wu's method by transforming the two kinds of transcendental functions into polynomials. This approach has been used for mechanical theorem proving in Euclidean and several Non-Euclidean geometries. Based on our approach, several meta-theorems are established for four Non-Euclidean geometries. These meta-theorems assert that certain kinds of geometry statements that can be confirmed by our approach in one geometry can also be confirmed in three other geometries. We also proved a meta-theorem which permits us to obtain all hyperbolic identities from trigonometric identities through certain kinds of transformation and vice versa.The revision was supported by the NSF grant CCR-8702108.     

A general technique for proving lock-freedom

Lock-freedom is a property of concurrent programs which states that, from any state of the program, eventually some process will complete its operation. Lock-freedom is a weaker property than the usual expectation that eventually all processes will complete their operations. By weakening their completion guarantees, lock-free programs increase the potential for parallelism, and hence make more efficient use of multiprocessor architectures than lock-based algorithms. However, lock-free algorithms, and reasoning about them, are considerably more complex.In this paper we present a technique for proving that a program is lock-free. The technique is designed to be as general as possible and is guided by heuristics that simplify the proofs. We demonstrate our theory by proving lock-freedom of two non-trivial examples from the literature. The proofs have been machine-checked by the PVS theorem prover, and we have developed proof strategies to minimise user interaction.     

Complexity Bounds for Some Finite Forms of Kruskal's Theorem

Well-founded (partial) orders form an important and convenient mathematical basis for proving termination of algorithms. Well-partial orders provide a powerful method for proving the well-foundedness of partial orders (and hence for proving termination), since every partial ordering which extends a given well-partial ordering on the same domain is automatically well-founded. In this article it is shown by purely combinatorial means that the maximal order type of the homeomorphic embeddability relation on a given set of terms over a finite signature yields an appropriate ordinal recursive Hardy bound on the lengths of bad sequences which satisfy an effective growth rate condition. This result yields theoretical upper bounds for the computational complexity of algorithms, for which termination can be proved by Kruskal's theorem.     

Formal Verification of a Partial-Order Reduction Technique for Model Checking

Mechanical theorem proving and model checking are the two main methods of formal verification, each with its own strengths and weaknesses. While mechanical theorem proving is more general, it requires intensive human guidance. Model checking is automatic, but is applicable to a more restricted class of problems. It is appealing to combine these two methods in order to take advantage of their different strengths. Prior research in this direction has focused on how to decompose a verification problem into parts each of which is manageable by one of the two methods. In this paper we explore another possibility: we use mechanical theorem proving to formally verify a meta-theory of model checking. As a case study, we use the mechanical theorem prover HOL to verify the correctness of a partial-order reduction technique for cutting down the amount of state search performed by model checkers. We choose this example for two reasons. First, this reduction technique has been implemented in the protocol analysis tool SPIN to significantly speed up the analysis of many practical protocols; hence its correctness has important practical consequences. Second, the correctness arguments involve nontrivial mathematics, the formalization of which we hope will become the basis of a formal meta-theory of other model-checking algorithms and techniques. Interestingly, our formalization led to a nontrivial generalization of the original informal theory. We discuss the lessons, both encouraging and discouraging, learned from this exercise. In the appendix we highlight the important definitions and theorems from each of our HOL theories. The complete listing of our HOL proof is given in a separate document because of space limitations.