模态归结弱包含删除策略

本文提出了一种模态归结的弱包含删除策略，证明了使用弱包含删除策略模态归结的完备性．从而，将Ａｕｆｆｒａｙ等人提出的开问题（ＯｐｅｎＰｒｏｂｌｅｍ）——模态归结包含删除策略的完备性向前推进了一步．     

The subsumption lattice and query learning

The paper identifies several new properties of the lattice induced by the subsumption relation over first-order clauses and derives implications of these for learnability. In particular, it is shown that the length of subsumption chains of function free clauses with bounded size can be exponential in the size. This suggests that simple algorithmic approaches that rely on repeating minimal subsumption-based refinements may require a long time to converge. It is also shown that with bounded size clauses the subsumption lattice has a large branching factor. This is used to show that the class of first-order length-bounded monotone clauses is not properly learnable from membership queries alone. Finally, the paper studies pairing, a generalization operation that takes two clauses and returns a number of possible generalizations. It is shown that there are clauses with an exponential number of pairing results which are not related to each other by subsumption. This is used to show that recent pairing-based algorithms can make exponentially many queries on some learning problems.     

Recognizing unnecessary clauses in resolution based systems

We concentrate on the problem of unnecessary inference in the context of resolution based systems. In such systems several strategies have been developed that allow for the delection of clauses without sacrificing completeness. Unfortunately these strategies fail to recognize other frequently generated unnecessary formulas. We will present a generalized subsumption theorem that can be used to recognize such formulas and to develop new deletion methods which retain completeness.     

On generalization/specialization for conceptual graphs

Abstract

This paper centres on the generalization/specialization relation in the framework of conceptual graphs (this relation corresponds to logical subsumption when considering logical formulas associated with conceptual graphs). Results given here apply more generally to any model where knowledge is described by labelled graphs and reasoning is based on graph subsumption, as in semantic networks or in structural machine learning. The generalization/specialization relation, as defined by Sowa, is first precisely analysed, in particular its links with a graph morphism, called projection. Besides Sowa's specialization relation (which is a preorder), another one is actually used in some practical applications (which is an order). These are comparatively studied. The second topic of this paper is the design of efficient algorithms for computing these specialization relations. Since the associated problems are NP-hard, the form of the graphs is restricted in order to arrive at polynomial algorithms. In particular, polynomial algorithms are presented for computing a projection from a conceptual ‘tree’ to any conceptual graph, and for counting the number of such projections. The algorithms are also described in a generic way, replacing the projection by a parametrized graph morphism, and conceptual graphs by directed labelled graphs.     

A Disjunctive Positive Refinement of Model Elimination and its Application to Subsumption Deletion

The Model Elimination (ME) calculus is a refutationally complete,goal-oriented calculus for first-order clause logic. In this article, weintroduce a new variant called disjunctive positive ME (DPME); it improveson Plaisteds positive refinement of ME in that reduction steps areallowed only with positive literals stemming from clauses having at leasttwo positive literals (so-called disjunctive clauses). DPME is motivated byits application to various kinds of subsumption deletion: in order to applysubsumption deletion in ME equally successful as in resolution, it iscrucial to employ a version of ME that minimizes ancestor context (i.e., thenecessary A-literals to find a refutation). DPME meets this demand. Wedescribe several variants of ME with subsumption, the most important onesbeing ME with backward and forward subsumption and theT*-Context Check. We compare their pruning power, also takinginto consideration the well-known regularity restriction. All proofs aresupplied. The practicability of our approach is demonstrated with experiments.     

Redundancy in logic I: CNF propositional formulae

A knowledge base is redundant if it contains parts that can be inferred from the rest of it. We study some problems related to the redundancy of a CNF formula. In particular, any CNF formula can be made irredundant by deleting some of its clauses: what results is an irredundant equivalent subset. We study the complexity of problems related to irredundant equivalent subsets: verification, checking existence of an irredundant equivalent subset with a given size, checking necessary and possible presence of clauses in irredundant equivalent subsets, and uniqueness. We also consider the problem of redundancy with different definitions of equivalence.     

Filter-based resolution principle for lattice-valued propositional logic LP(X)

As one of most powerful approaches in automated reasoning, resolution principle has been introduced to non-classical logics, such as many-valued logic. However, most of the existing works are limited to the chain-type truth-value fields. Lattice-valued logic is a kind of important non-classical logic, which can be applied to describe and handle incomparability by the incomparable elements in its truth-value field. In this paper, a filter-based resolution principle for the lattice-valued propositional logic LP(X) based on lattice implication algebra is presented, where filter of the truth-value field being a lattice implication algebra is taken as the criterion for measuring the satisfiability of a lattice-valued logical formula. The notions and properties of lattice implication algebra, filter of lattice implication algebra, and the lattice-valued propositional logic LP(X) are given firstly. The definitions and structures of two kinds of lattice-valued logical formulae, i.e., the simple generalized clauses and complex generalized clauses, are presented then. Finally, the filter-based resolution principle is given and after that the soundness theorem and weak completeness theorems for the presented approach are proved.     

输入冗余在时间最优控制中的作用

随着冗余控制系统的不断出现, 本文主要研究了在可控线性系统中增加新的冗余控制通道所带来的优势. 对于时间最优控制问题, 这样的优势可以通过最优时间的缩短进行衡量. 本文证明了在最优控制存在且唯一的基础上, 如果增加的冗余控制通道中存在非空闲通道, 则对于任意的非零初始状态, 增加冗余控制通道后系统的最优时间将严格降低. 更进一步, 如果时间最优控制问题是正常的, 则最优时间也将严格下降. 另一方面, 如果忽略问题的正常性这个条件, 只要冗余控制通道中存在一个完全可控的通道, 最优时间同样也会严格下降. 最后, 我们通过两个数值例子印证了本文的理论结果.     

Tractability through symmetries in propositional calculus

Many propositional calculus problems — for example the Ramsey or the pigeon-hole problems — can quite naturally be represented by a small set of first-order logical clauses which becomes a very large set of propositional clauses when we substitute the variables by the constants of the domainD. In many cases the set of clauses contains several symmetries, i.e. the set of clauses remains invariant under certain permutations of variable names. We show how we can shorten the proof of such problems. We first present an algorithm which detects the symmetries and then we explain how the symmetries are introduced and used in the following methods: SLRI, Davis and Putnam and semantic evaluation. Symmetries have been used to obtain results on many known problems, such as the pigeonhole, Schur's lemma, Ramsey's, the eight queen, etc. The most interesting one is that we have been able to prove for the first time the unsatisfiability of Ramsey's problem (17 vertices and three colors) which has been the subject of much research.     

Redundancy resolution through local optimization: A review

Kinematically redundant manipulator arms and other robotic mechanisms provide a means for solving sophisticated motion tasks but require complex research on both mechanical and control problems. So far, many works have been published on kinematic redundancy, however, a systemization is missing. In this article an attempt for such a systemization is presented. It has been limited to methods for redundancy resolution through local optimization. Until now, these methods are most widely used, and it is expected also that they will prevail in the near future. A classification is suggested and the performance capabilities of the methods are discussed and compared. Two reference tables are provided; One of them lists references for different problems on kinematic redundancy as: mechanical design, dexterity measures, multicriteria optimization, global optimization, control design and computational considerations. The other table displays existing publications classified according to the application area of redundant robotic-mechanisms.     

Graph Traversal and Top-Down Evaluation of Logic Queries

In this paper,an optimal method to handle cyclic and acyclic data relations in the linear recursive queries is proposed.High efficiency is achieved by integrating graph traversal mechanisms into a top-down evaluation.In such a way,the subsumption checks and the identification of cyclic data can be done very efficiently.First,based on the subsumption checks,the search space can be reduced drastically by avoiding any redundant expansion operation.In fact,in the case of non-cyclic data,the proposed algorithm requires only linear time for evaluating a linear recursive query.On the other hand,in the case of cyclic data,by using the technique for isolaiting strongly connected components a lot of answers can be generatded directly in terms of the intermediate results and the relevant path information instead of evaluating them by performing algebraic operations.Since the cost of generating an answer in much less than that of evaluating an answer by algebraic operations,the bime consumption for cyclic data can be reduced by an order of magnitude or more.     

The anatomy of vampire

We present an implementation technique for a class of bottom-up logic procedures. The technique is based oncode trees. It is intended to speed up most important and costly operations, such as subsumption and resolution. As an example, we consider the forward subsumption problem which is the bottleneck of many systems implementing first-order logic.To efficiently implement subsumption, we specialize subsumption algorithms at run time, using theabstract subsumption machine. The abstract subsumption machine makes subsumption-check using sequences of instructions that are similar to the WAM instructions. It gives an efficient implementation of the clause at a time subsumption problem. To implement subsumption on the set at a time basis, we combine sequences of instructions incode trees.We show that this technique yields a new way of indexing clauses. Some experimental results are given.The code trees technique may be used in various procedures, including binary resolution, hyper-resolution, UR-resolution, the inverse method, paramodulation and rewriting, OLDT-resolution, SLD-AL-resolution, bottom-up evaluation of logic programs, and disjunctive logic programs.Supported by Swedish TFR grant No. 93–409     

模糊描述逻辑FALNUI的tableaux推理

分析了模糊描述逻辑FALNUI与模糊ER模型的关系,即模糊ER模型可以转化为FALNUI的知识库,并且模糊ER模型的可满足性、冗余性和包含关系等推理问题可以转化为FALNUI的包含推理问题,但FALNUI缺乏相应的推理算法.提出了一种基于描述逻辑tableaux的FALNUI的可满足性推理算法,证明了该推理算法的正确性,以及提出了FALNUI的Tbox扩展和去除方法,证明了FALNUI的包含推理问题可以转化为可满足性推理问题,并给出了FALNUI的包含推理算法.FALNUI的tableaux推理算法为模糊ER模型的可满足性、冗余性和包含关系等自动推理的实现提供了理论基础.     

S2R2:基于相关性与冗余性分析的半监督特征选择

特征选择是模式识别与数据挖掘的关键问题之一,它可以移除数据集中的冗余和不相关特征以提升学习性能。基于最大相关最小冗余准则,提出一种新的基于相关性与冗余性分析的半监督特征选择方法(S2R2),S2R2方法独立于任何分类学习算法。该方法首先对无监督相关度信息度量进行分析与扩充,然后结合信息增益,设计一种半监督特征相关性与冗余性度量,可以有效识别与移除不相关和冗余特征,最后采用增量搜索技术贪婪地构建特征子集,避免搜索指数级大小的解空间,提高算法的运行效率。本文还提出S2R2方法的快速过滤版本,FS2R2,以更好地应对大规模特征选择问题。多个标准数据集上的实验结果表明了所提方法的有效性和优越性。     

Generation of text from logical formulae

The paper addresses the problem of generating sentences from logical formulae. It describes a simple and efficient algorithm for generating text which has been developed for use in machine translation, but will have wider application in natural language processing. An important property of the algorithm is that the logical form used to generate a sentence need not be one which could have been produced by parsing the sentence: formal equivalence between logical forms is allowed for. This is necessary for a machine translation system, such as the one envisaged in this paper, which uses single declarative grammars of individual languages, and declarative statements of translation equivalences for transfer. In such a system, it cannot be guaranteed that transfer will produce a logical form in the same order as would have been produced by parsing some target-language sentence, and it is not practicable to define a normal form for the logical forms. The algorithm is demonstrated using a categorial grammar and a simple indexed logic, as this allows a particularly clear and elegant formulation. It is shown that the algorithm can be adapted to phrase-structure grammars, and to more complex semantic representations than that used here.     

Implementing the Davis–Putnam Method

The method proposed by Davis, Putnam, Logemann, and Loveland for propositional reasoning, often referred to as the Davis–Putnam method, is one of the major practical methods for the satisfiability (SAT) problem of propositional logic. We show how to implement the Davis–Putnam method efficiently using the trie data structure for propositional clauses. A new technique of indexing only the first and last literals of clauses yields a unit propagation procedure whose complexity is sublinear to the number of occurrences of the variable in the input. We also show that the Davis–Putnam method can work better when unit subsumption is not used. We illustrate the performance of our programs on some quasigroup problems. The efficiency of our programs has enabled us to solve some open quasigroup problems.     

基于时序聚类的北斗位置冗余数据压缩算法

在北斗用户机的位置数据采集过程中,容易出现数据冗余现象。为此,分析导致数据冗余的原因,提出一种基于时序聚类的冗余数据压缩算法。该算法采用基于密度的聚类方法将数据集进行分簇,把属于同一类运动特征的位置数据归为一类,根据簇直径判断该簇是否为冗余数据,并对冗余数据进行压缩。实验结果表明,该算法可以正确标识冗余数据,实现数据压缩。     

On finding short resolution refutations and small unsatisfiable subsets

We consider the parameterized problems of whether a given set of clauses can be refuted within k resolution steps, and whether a given set of clauses contains an unsatisfiable subset of size at most k  . We show that both problems are complete for the class W[1]$\mathrm{W}[1]$, the first level of the W-hierarchy of fixed-parameter intractable problems. Our results remain true if restricted to 3-SAT instances and/or to various restricted versions of resolution including tree-like resolution, input resolution, and read-once resolution. Applying a metatheorem of Frick and Grohe, we show that, restricted to classes of sets of clauses of locally bounded treewidth, the considered problems are fixed-parameter tractable. For example, the problems are fixed-parameter tractable for planar CNF formulas.     

Logic mining in neural network: reverse analysis method

Neural networks are becoming very popular with data mining practitioners because they have proven through comparison their predictive power with statistical techniques using real data sets. Based on this idea, we will present a method for inducing logical rules from empirical data—Reverse Analysis. When the values of the connections of a neural network resulting from Hebbian learning for the data are given, we hope to know what logical rules are entrenched in it. This method is tested with some real life data sets. In real life data sets, logical rules are assumed to be in conjunctive normal form (CNF) since Horn clauses are inadequate.     

Resolution theorem proving in reified modal logics

This paper is concerned with the application of the resolution theorem proving method to reified logics. The logical systems treated include the branching temporal logics and logics of belief based on K and its extensions. Two important problems concerning the application of the resolution rule to reified systems are identified. The first is the redundancy in the representation of truth functional relationships and the second is the axiomatic reasoning about modal structure. Both cause an unnecessary expansion in the search space. We present solutions to both problems which allow the axioms defining the reified logic to be eliminated from the database during theorem proving hence reducing the search space while retaining completeness. We describe three theorem proving methods which embody our solutions and support our analysis with empirical results.Much of the research reported in this paper was supported by DTI IED SERC grant No. GR/F 35968, and was carried out whilst Han Reichgelt was at the University of Nottingham.