The general state-space model for a two-dimensional linear digital system

The general state-space model for a 2-D linear digital system is presented. A new definition of state-transition matrix is given. Based on the definition, it is easy to calculate the state-transition matrix for any linear digital system. The general response formula for a system follows simply from the definition. A new definition of the characteristic function of a system and a theorem parallel to the Cayley-Hamilton theorem are also given. The presented results apply to any linear causal system.     

神经网络BP学习算法动力学分析

研究神经网络BP学习算法与微分动力系统的关系.指出BP学习算法的迭代式与相 应的微分动力系统数值解Euler方法在一定条件下等价,且二者在解的渐近性方面是一致的. 给出了神经网络BP学习算法与相应的微分动力系统解的存在性、唯一性定理和微分动力系统 的零解稳定性定理.从理论上证明了神经网络的学习在一定条件下与微分动力系统的数值方法 所得的数值解在渐近意义下是等价的,从而借助于微分动力系统的数值方法可以解决神经网络 的学习问题.最后给出了用改进Euler方法训练BP网的例子.     

自治混沌系统普适广义投影同步理论及应用

针对自治混沌系统，基于系统稳定性理论，通过设计合适的非线性反馈控制器，给出了普适的广义投影同步定理．定理中函数的选择可以为系统的线性或非线性函数，更具灵活性和普适性；文中理论还可以通过调整参数提高广义投影同步的速度．数值仿真进一步验证了本文理论的有效性和实用性．     

LINUS - A Link Instantion Prover with Unit Support

LINUS is a theorem prover for clause logic based on hyperlinking. The main new feature of the system is the emphasis on the preference for unit clauses, which are generated as a by-product of the hyperlinking method. The mechanism of unit support also motivates a slightly different interpretation of hyperlinking, namely, as mate saturation. Mate saturation can be viewed as a generalization of unit-resulting resolution that is compatible with any set-of-support strategy. We give a survey on the theoretical background and the architecture of the system, and decribe its performance.     

A proof of the non-existence of a bounded-derivative continuous model for a discrete chaotic system

Takens' theorem states that for any dynamical system there exists a dimension in which the system can be embedded as a sampling of a continuous function. This paper presents a result which shows that a non-constant continuous model with a bounded time derivative does not exist when the system to be embedded is a discrete chaotic process. The result presented here does not contradict Takens' theorem which has no requirement of a bounded time derivative. The assumption of a bounded derivative is an important one since recurrent neural network learning rules usually implicitly assume that a bounded time derivative exists for the network dynamics equations which define the system model.     

时滞不确定系统的鲁律性分析

此文利用解的估计方法和比较定理，研究了线性时滞不确定系统的鲁棒性问题，得到了用状态反馈来镇定这类系统的充分条件，并给出了此类系统具有任意希望的鲁棒性条件．     

时滞不确定系统的鲁棒性分析

此文利用解的估计方法和比较定理,研究了线性时滞不确定系统的鲁棒性问题,得到了用 状态反馈来镇定这类系统的充分条件,并给出了此类系统具有任意希望的鲁棒性条件.     

集合论等式型定理机器证明系统的研究与开发

集合论定理机器证明,至今在国内外尚无相关研究。虽然集合论在数学领域中所处的基础地位显得在这一领域实现机械化极其重要,但是多年来尚无进展。到目前为止,还没有发现能产生可读证明的系统。通过对人工智能搜索算法的研究,提出了集合论等式型定理证明的机械化方法。实现的系统能自动生成定理的可读证明以及相关的说明。     

An autonomous multistrategy theorem proving system using knowledge-based techniques

Most general-purpose theorem-proving systems have weak search control. There is no alternative to the use of a large number of heuristics or strategies for search guidance. Choosing appropriate strategies for solving a given problem may require the knowledge of different strategies and may involve a lot of painstaking trial-and-error. To encourage the widespread use of computer reasoning systems, it is important that a theorem prover be usable by those with little knowledge of problem-solving strategies, and that a theorem prover be able to select good strategies for the user. An autonomous multistrategy theorem-proving system is developed, using knowledge-based techniques, to entirely free the user from the necessity of understanding the system or the merits of different strategies. All the user has to do is input his or her problem in first-order logic, and the system solves the problem efficiently for him or her without any manual intervention. The system embodies much of expert knowledge about how to solve problems. The knowledge is represented as metarules in knowledge base which guide a hyperlinking theorem prover to solve problems automatically and efficiently.     

An experiment with the Boyer-Moore theorem prover: A proof of Wilson's theorem

This paper describes the use of the Boyer-Moore theorem prover in mechanically generating a proof of Wilson's theorem: for any prime p, (p-1)! and p-1 are congruent modulo p. The input to the theorem prover consists of a sequence of three function definitions and forty-two propositions to be proved. The proofs generated by the system are based on a library of lemmas relating to list manipulation and number theory, including Fermat's theorem.     

一维云模型系统的逼近性研究

针对云模型的基本原理,提出了一类云模型系统的设计方法,并利用Stone-Weierstrass定理对在3σ 正态分布随机数条件下的云模型系统任意逼近紧集上的任意连续实函数进行了证明, 是对云模型应用于逼近任意连续非线性函数理论的创新,也是今后云模型系统用于系统辨识和控制的理论依据.     

The time-rescaling theorem and its application to neural spike train data analysis.

Measuring agreement between a statistical model and a spike train data series, that is, evaluating goodness of fit, is crucial for establishing the model's validity prior to using it to make inferences about a particular neural system. Assessing goodness-of-fit is a challenging problem for point process neural spike train models, especially for histogram-based models such as perstimulus time histograms (PSTH) and rate functions estimated by spike train smoothing. The time-rescaling theorem is a well-known result in probability theory, which states that any point process with an integrable conditional intensity function may be transformed into a Poisson process with unit rate. We describe how the theorem may be used to develop goodness-of-fit tests for both parametric and histogram-based point process models of neural spike trains. We apply these tests in two examples: a comparison of PSTH, inhomogeneous Poisson, and inhomogeneous Markov interval models of neural spike trains from the supplementary eye field of a macque monkey and a comparison of temporal and spatial smoothers, inhomogeneous Poisson, inhomogeneous gamma, and inhomogeneous inverse gaussian models of rat hippocampal place cell spiking activity. To help make the logic behind the time-rescaling theorem more accessible to researchers in neuroscience, we present a proof using only elementary probability theory arguments. We also show how the theorem may be used to simulate a general point process model of a spike train. Our paradigm makes it possible to compare parametric and histogram-based neural spike train models directly. These results suggest that the time-rescaling theorem can be a valuable tool for neural spike train data analysis.     

Conquering the Meredith Single Axiom

For more than three and one-half decades, beginning in the early 1960s, a heavy emphasis on proof finding has been a key component of the Argonne paradigm, whose use has directly led to significant advances in automated reasoning and important contributions to mathematics and logic. The theorems studied range from the trivial to the deep, even including some that corresponded to open questions. Often the paradigm asks for a theorem whose proof is in hand but that cannot be obtained in a fully automated manner by the program in use. The theorem whose hypothesis consists solely of the Meredith single axiom for two-valued sentential (or propositional) calculus and whose conclusion is the ukasiewicz three-axiom system for that area of formal logic was just such a theorem. Featured in this article is the methodology that enabled the program OTTER to find the first fully automated proof of the cited theorem, a proof with the intriguing property that none of its steps contains a term of the form n(n(t)) for any term t. As evidence of the power of the new methodology, the article also discusses OTTER's success in obtaining the first known proof of a theorem concerning a single axiom of ukasiewicz.     

Hierarchy Among Automata on Linear Orderings

In a preceding paper, automata and rational expressions have been introduced for words indexed by linear orderings, together with a Kleene-like theorem. We here pursue this work by proposing a hierarchy among the rational sets. Each class of the hierarchy is defined by a subset of the rational operations that can be used. We then characterize any class by an appropriate class of automata, leading to a Kleene theorem inside the class. A characterization by particular classes of orderings is also given.     

Simple criterion for testing non-minimum-phase systems

Simple sufficient conditions for non-minimum-phase systems are derived using the fundamental theorem of algebra. It is shown that the unstable poles or zeros of a control system can be tested directly from the coefficients of the characteristic polynomials without any calculation. This criterion is useful for the computer-aided design of control systems.     

一种核化图嵌入算法的快速求解模型

针对核化图嵌入算法对于人脸识别等高维小样本问题存在着计算量大且所需存储空间多的缺点,提出了一种核化图嵌入算法的快速求解模型。该模型的思想是首先对原始样本进行降维处理,对此给出了定理1和2。两个定理证明了样本先进行降维处理的可行性,同时也表明这一过程是不损失任何有效鉴别信息的。然后再对新的低维样本按核化图嵌入算法进行计算。人脸库上的实验结果表明,所提模型不但减少了算法的计算时间,同时也保证了算法的分类识别率。     

Ultimate periodicity of orbits for min-max systems

The ultimate periodicity theorem is an important result in min-max systems theory. It was first proved by Olsder and Perennes in their unpublished work. In this paper, we present a new proof. This proof is also based on two important theorems: the existence of cycle time for any min-max function and the Nussbaum-Sine theorem. However, two different techniques, pure min-max function and conditional redundancy, are used to obtain two important intermediate results. The purpose of this paper is to provide a simple alternate proof to the ultimate periodicity theorem.     

Resolution is Cut-Free

In this article, we show that the extension of the resolution proof system to deduction modulo is equivalent to the cut-free fragment of the sequent calculus modulo. The result is obtained through a syntactic translation, without using any cut-elimination procedure. Additionally, we show Skolem theorem and inversion/focusing results. Thanks to the expressiveness of deduction modulo, all these results also apply to the cases of higher-order resolution, Peano’s arithmetic and Gentzen’s LK.     

Replacing unification by constraint satisfaction to improve logic program expressiveness

Unification, the heart of resolution, was formulated to work in the Herbrand universe and hence does not incorporate any function evaluation. Matching is completely syntactic. In this paper, we study the replacement of unification by a constraints solver in automatic theorem proving systems using Prolog as our example. The generalization of unification into a constraint satisfaction algorithm allows the (limited) incorporation of function evaluation into unification. Constraints are also allowed as literals in the clause. We discuss the enhanced expressive power that results from incorporating an efficient constrained unifier into an automatic theorem proving system. An interpreter for the extended Prolog system (written in Prolog) incorporating a constraint solver is presented along with examples illustrating its capabilities.     

Causal graphs and structurally restricted planning

The causal graph is a directed graph that describes the variable dependencies present in a planning instance. A number of papers have studied the causal graph in both practical and theoretical settings. In this work, we systematically study the complexity of planning restricted by the causal graph. In particular, any set of causal graphs gives rise to a subcase of the planning problem. We give a complete classification theorem on causal graphs, showing that a set of graphs is either polynomial-time tractable, or is not polynomial-time tractable unless an established complexity-theoretic assumption fails; our theorem describes which graph sets correspond to each of the two cases. We also give a classification theorem for the case of reversible planning, and discuss the general direction of structurally restricted planning.