Möbius transforms, coincident Boolean functions and non-coincidence property of Boolean functions

Boolean functions and their Möbius transforms are involved in logical calculation, digital communications, coding theory and modern cryptography. So far, little is known about the relations of Boolean functions and their Möbius transforms. This work is composed of three parts. In the first part, we present relations between a Boolean function and its Möbius transform so as to convert the truth table/algebraic normal form (ANF) to the ANF/truth table of a function in different conditions. In the second part, we focus on the special case when a Boolean function is identical to its Möbius transform. We call such functions coincident. In the third part, we generalize the concept of coincident functions and indicate that any Boolean function has the coincidence property even it is not coincident.

On linear order and computation : The expressiveness of interactive computations on linear orders and computations indexed by ordinals

We solve the Dynamic Ehrenfeucht-Fra\"iss\'e Game on linear orders for both players, yielding a normal form for quantifier-rank equivalence classes of linear orders in first-order logic, infinitary logic, and generalized-infinitary logics with linearly ordered clocks. We show that Scott Sentences can be manipulated quickly, classified into local information, and consistency can be decided effectively in the length of the Scott Sentence. We describe a finite set of linked automata moving continuously on a linear order. Running them on ordinals, we compute the ordinal truth predicate and compute truth in the constructible universe of set-theory. Among the corollaries are a study of semi-models as efficient database of both model-theoretic and formulaic information, and a new proof of the atomicity of the Boolean algebra of sentences consistent with the theory of linear order -- i.e., that the finitely axiomatized theories of linear order are dense.

Algebraic Cryptanalysis of CTRU Cryptosystem

CTRU, a public key cryptosystem was proposed by Gaborit, Ohler and Sole. It is analogue of NTRU, the ring of integers replaced by the ring of polynomials $\mathbb{F}_2[T]$ . It attracted attention as the attacks based on either LLL algorithm or the Chinese Remainder Theorem are avoided on it, which is most common on NTRU. In this paper we presents a polynomial-time algorithm that breaks CTRU for all recommended parameter choices that were derived to make CTRU secure against popov normal form attack. The paper shows if we ascertain the constraints for perfect decryption then either plaintext or private key can be achieved by polynomial time linear algebra attack.

Elastic behaviour of matter under very high pressures - Uniform compression

In order to study the elastic behaviour of matter when subjected to very large pressures, such as occur for example in the interior of the earth, and to provide an explanation for phenomena like earthquakes, it is essential to be able to calculate the values of the elastic constants of a substance under a state of large initial stress in terms of the elastic constants of a natural or stress-free state. An attempt has been made in this paper to derive expressions for these quantities for a substance of cubic symmetry on the basis of non-linear theory of elasticity and including up to cubic powers of the strain components in the strain energy function. A simple method of deriving them directly from the energy function itself has been indicated for any general case and the same has been applied to the case of hydrostatic compression. The notion of an effective elastic energy-the energy require to effect an infinitesimal deformation over a state of finite strain-has been introduced, the coefficients in this expression being the effective elastic constants. A separation of this effective energy function into normal co-ordinates has been given for the particular case of cubic symmetry and it has been pointed out, that when any of such coefficients in this normal form becomes negative, elastic instability will set in, with associated release of energy.

Solution concepts in two-person multicriteria games

In this paper, we propose new solution concepts for multicriteria games and compare them with existing ones. The general setting is that of two-person finite games in normal form (matrix games) with pure and mixed strategy sets for the players. The notions of efficiency (Pareto optimality), security levels, and response strategies have all been used in defining solutions ranging from equilibrium points to Pareto saddle points. Methods for obtaining strategies that yield Pareto security levels to the players or Pareto saddle points to the game, when they exist, are presented. Finally, we study games with more than two qualitative outcomes such as combat games. Using the notion of guaranteed outcomes, we obtain saddle-point solutions in mixed strategies for a number of cases. Examples illustrating the concepts, methods, and solutions are included.

An integer arithmetic method to compute generalized matrix inverse and solve linear equations exactly

An algorithm that uses integer arithmetic is suggested. It transforms anm ×n matrix to a diagonal form (of the structure of Smith Normal Form). Then it computes a reflexive generalized inverse of the matrix exactly and hence solves a system of linear equations error-free.

Geosphere laminations in free groups

We construct for free groups, which are codimension one analogues of geodesic laminations on surfaces. Other analogues that have been constructed by several authors are dimension-one instead of codimension-one. Our main result is that the space of such laminations is compact. This in turn is based on the result that crossing, in the sense of Scott-Swarup, is an open condition. Our construction is based on Hatcher's normal form for spheres in the model manifold.

About generalized scaling for passive scalars in fully developed turbulence

In this paper we use a simple normal form approach of scale invariant fields to investigate scaling laws of passive scalars in turbulence. The coupling equations for velocity and passive scalar moments are scale covariant. Their solution shows that passive scalars in turbulence do not generically follow a general scaling observed for velocity field because of coupling effects.

Invariant-free deduction systems for temporal logic

In this thesis we propose a new approach to deduction methods for temporal logic. Our proposal is based on an inductive definition of eventualities that is different from the usual one. On the basis of this non-customary inductive definition for eventualities, we first provide dual systems of tableaux and sequents for Propositional Linear-time Temporal Logic (PLTL). Then, we adapt the deductive approach introduced by means of these dual tableau and sequent systems to the resolution framework and we present a clausal temporal resolution method for PLTL. Finally, we make use of this new clausal temporal resolution method for establishing logical foundations for declarative temporal logic programming languages. The key element in the deduction systems for temporal logic is to deal with eventualities and hidden invariants that may prevent the fulfillment of eventualities. Different ways of addressing this issue can be found in the works on deduction systems for temporal logic. Traditional tableau systems for temporal logic generate an auxiliary graph in a first pass.Then, in a second pass, unsatisfiable nodes are pruned. In particular, the second pass must check whether the eventualities are fulfilled. The one-pass tableau calculus introduced by S. Schwendimann requires an additional handling of information in order to detect cyclic branches that contain unfulfilled eventualities. Regarding traditional sequent calculi for temporal logic, the issue of eventualities and hidden invariants is tackled by making use of a kind of inference rules (mainly, invariant-based rules or infinitary rules) that complicates their automation. A remarkable consequence of using either a two-pass approach based on auxiliary graphs or aone-pass approach that requires an additional handling of information in the tableau framework, and either invariant-based rules or infinitary rules in the sequent framework, is that temporal logic fails to carry out the classical correspondence between tableaux and sequents. In this thesis, we first provide a one-pass tableau method TTM that instead of a graph obtains a cyclic tree to decide whether a set of PLTL-formulas is satisfiable. In TTM tableaux are classical-like. For unsatisfiable sets of formulas, TTM produces tableaux whose leaves contain a formula and its negation. In the case of satisfiable sets of formulas, TTM builds tableaux where each fully expanded open branch characterizes a collection of models for the set of formulas in the root. The tableau method TTM is complete and yields a decision procedure for PLTL. This tableau method is directly associated to a one-sided sequent calculus called TTC. Since TTM is free from all the structural rules that hinder the mechanization of deduction, e.g. weakening and contraction, then the resulting sequent calculus TTC is also free from this kind of structural rules. In particular, TTC is free of any kind of cut, including invariant-based cut. From the deduction system TTC, we obtain a two-sided sequent calculus GTC that preserves all these good freeness properties and is finitary, sound and complete for PLTL. Therefore, we show that the classical correspondence between tableaux and sequent calculi can be extended to temporal logic. The most fruitful approach in the literature on resolution methods for temporal logic, which was started with the seminal paper of M. Fisher, deals with PLTL and requires to generate invariants for performing resolution on eventualities. In this thesis, we present a new approach to resolution for PLTL. The main novelty of our approach is that we do not generate invariants for performing resolution on eventualities. Our method is based on the dual methods of tableaux and sequents for PLTL mentioned above. Our resolution method involves translation into a clausal normal form that is a direct extension of classical CNF. We first show that any PLTL-formula can be transformed into this clausal normal form. Then, we present our temporal resolution method, called TRS-resolution, that extends classical propositional resolution. Finally, we prove that TRS-resolution is sound and complete. In fact, it finishes for any input formula deciding its satisfiability, hence it gives rise to a new decision procedure for PLTL. In the field of temporal logic programming, the declarative proposals that provide a completeness result do not allow eventualities, whereas the proposals that follow the imperative future approach either restrict the use of eventualities or deal with them by calculating an upper bound based on the small model property for PLTL. In the latter, when the length of a derivation reaches the upper bound, the derivation is given up and backtracking is used to try another possible derivation. In this thesis we present a declarative propositional temporal logic programming language, called TeDiLog, that is a combination of the temporal and disjunctive paradigms in Logic Programming. We establish the logical foundations of our proposal by formally defining operational and logical semantics for TeDiLog and by proving their equivalence. Since TeDiLog is, syntactically, a sublanguage of PLTL, the logical semantics of TeDiLog is supported by PLTL logical consequence. The operational semantics of TeDiLog is based on TRS-resolution. TeDiLog allows both eventualities and always-formulas to occur in clause heads and also in clause bodies. To the best of our knowledge, TeDiLog is the first declarative temporal logic programming language that achieves this high degree of expressiveness. Since the tableau method presented in this thesis is able to detect that the fulfillment of an eventuality is prevented by a hidden invariant without checking for it by means of an extra process, since our finitary sequent calculi do not include invariant-based rules and since our resolution method dispenses with invariant generation, we say that our deduction methods are invariant-free.

Diagonal forms, linear algebraic methods and Ramsey-type problems

This thesis focuses mainly on linear algebraic aspects of combinatorics. Let N_t(H) be an incidence matrix with edges versus all subhypergraphs of a complete hypergraph that are isomorphic to H. Richard M. Wilson and the author find the general formula for the Smith normal form or diagonal form of N_t(H) for all simple graphs H and for a very general class of t-uniform hypergraphs H.

As a continuation, the author determines the formula for diagonal forms of integer matrices obtained from other combinatorial structures, including incidence matrices for subgraphs of a complete bipartite graph and inclusion matrices for multisets.

One major application of diagonal forms is in zero-sum Ramsey theory. For instance, Caro's results in zero-sum Ramsey numbers for graphs and Caro and Yuster's results in zero-sum bipartite Ramsey numbers can be reproduced. These results are further generalized to t-uniform hypergraphs. Other applications include signed bipartite graph designs.

Research results on some other problems are also included in this thesis, such as a Ramsey-type problem on equipartitions, Hartman's conjecture on large sets of designs and a matroid theory problem proposed by Welsh.

Conditions for the local manipulation of tripartite Gaussian states

We present the normal form of the covariance matrix for three-mode tripartite Gaussian states. By means of this result, the general form of a necessary and sufficient criterion for the possibility of a state transformation from one tripartite entangled Gaussian state to another with three modes is found. Moreover, we show that the conditions presented include not only inequalities but equalities as well.

CSRe束流动力学研究

非线性动力学对于环形加速器，尤其是对现代新型的加速器来说，起着越来越重要的作用。非线性力的引入使得束流在真空管道中的稳定性大大降低，对物理实验产生较大的影响。所以对束流动力学尤其是非线性动力学的研究已成为加速器研究中的一个必要的、重要的课题。 本文首先对加速器物理的基础知识和兰州重离子加速器冷却储存环及其实验环（HIRFL-CSRe）做了一定的介绍。然后给出了非线性力存在时的动力学孔径的理解和此时动力学孔径的多种研究方法。 接着本论文对束流的共振情况做了推导和描述，用映射的观点，通过Normal Form这一数学工具研究了CSRe的非线性动力学。然后用加速器常用的软件（COSY INFINITY）研究了HIRFL-CSRe在各种状态下由于高阶场误差带来的非线性力对各阶共振力的影响。 最后，也是本文的核心部分。用MAD程序研究了CSRe横向动力学。对CSRe色品进行了校正，并计算了色品六极铁对CSRe Lattice的影响。对CSRe理想Lattice的动力学孔径进行了计算，然后根据实际测磁数据计算了CSRe在有二极铁和四极铁高阶误差等多种情况下的动力学孔径，最后通过实际实验时的束流的各种参数的测量说明了理论计算和实际情况一致，强度和稳定性都能够满足物理实验的要求。 本论文对CSRe系统的运行和CSRe各项实验有着一定的实际意义

CSRm横向动力学研究

随着现代加速器向高能、强流、长寿命束流方向的发展，非线性动力学己成为现代加速器研究中一个非常重要的课题。本文从解析和数值模拟两方面对CSRm在存在各种场缺陷和安装准直误差情况下的非线性动力学进行了研究，并探讨研究了环型加速器中随时间变化驱动力-tune调制对粒子稳定性的影响。在解析研究方面，本文给出了储存环非线性束流动力学中基本理论、常用的表达式及研究方法做了详细介绍和推导。作为对非线性束流动力学解析研究的典型例子，本文给出了高杰推导出的存在不同非线性磁铁高阶场时动力学孔径解析表达式的详细推导过程。解析表达式能直观表示影响粒子运动稳定性的关键因素，但解析表达式所描述的lattice结构过子简单，只能看作是实际储存环lottice的近似。通过解析法可以研究主导粒子运动不稳定性的机制，但用来确定储存环动力学孔径强有力的工具是数值跟踪。用映射的观点，通过非线性变换，将表示通常粒子非线性运动的单圈映射用Normal Form来表示。用Normal Form这一数学工具，通过计算粒子运动稳定相空间体积确定了CSRm动力学孔径，求出了CSRm的高阶共振参数，半解析的研究了CSRm中tune随粒子振荡振幅的变换-Detuning效应。同时，跟用其他的数值方法的计算结果进行了比较。储存环中影响粒子运动稳定性的因素，除各种场缺陷和安装准直误差外，还有电源纹波效应等所引起随时间变化驱动力的影响。本文先从理论上分析研究了tune调制所引起的随机层宽度，扩散速度等，然后通过单粒子跟踪研究了tune调制对简单的FODo 1 ottice和CSRm的影响。用加速器中常用的MAD程序研究了CSRm横向动力学。对CSRm色品进行校正，并计算了色品六极铁对CSRmlattice的影响。通过实际的测量数据计算了二极铁的离散性和四极铁的安装准直误差所引起的闭轨畸变。由于CsRm二极铁黔的四极分量所引起 Tune移动时粒子在加速过程中经过共振线，所以对lattice黔行了修正。最后跟踪研究了lattice修正后的动力学孔径。

Deciding Isomorphisms of Simple Types in Polynomial Time

The isomorphisms holding in all models of the simply typed lambda calculus with surjective and terminal objects are well studied - these models are exactly the Cartesian closed categories. Isomorphism of two simple types in such a model is decidable by reduction to a normal form and comparison under a finite number of permutations (Bruce, Di Cosmo, and Longo 1992). Unfortunately, these normal forms may be exponentially larger than the original types so this construction decides isomorphism in exponential time. We show how using space-sharing/hash-consing techniques and memoization can be used to decide isomorphism in practical polynomial time (low degree, small hidden constant). Other researchers have investigated simple type isomorphism in relation to, among other potential applications, type-based retrieval of software modules from libraries and automatic generation of bridge code for multi-language systems. Our result makes such potential applications practically feasible.