Related papers: Towards the Certification of Complexity Proofs
We present in this paper some fundamental tools for developing matrix analysis over the complex quaternion algebra. As applications, we consider generalized inverses, eigenvalues and eigenvectors, similarity, determinants of complex…
The problem of finding a canonical form of complex matrices up to conjugacy with the set of canonical matrices being a union of affine planes in the matrix space is considered. A solution of the problem is given producing a new canonical…
We survey recent progress on efficient algorithms for approximately diagonalizing a square complex matrix in the models of rational (variable precision) and finite (floating point) arithmetic. This question has been studied across several…
Many facts possess symmetrical counterparts that often require a separate formal proof, depending on the nature of the involved symmetry. We introduce a method in Isabelle/HOL which produces such a symmetrical fact for the list datatype and…
We construct explicit Boolean square matrices whose rectifier complexity (OR-complexity) differs significantly from the complexity of their complement matrices.
We discuss an extension of the almost Hadamard matrix formalism, to the case of complex matrices. Quite surprisingly, the situation here is very different from the one in the real case, and our conjectural conclusion is that there should be…
We describe our ongoing project of formalization of algebraic methods for geometry theorem proving (Wu's method and the Groebner bases method), their implementation and integration in educational tools. The project includes formal…
This report describes three particular technological advances in formal proofs. The HOL Light proof assistant will be used to illustrate the design of a highly reliable system. Today, proof assistants can verify large bodies of advanced…
Context: The complexity of modern safety-critical systems in industries keep on increasing due to the rising number of features and functionalities. This calls for formal methods in order to entrust confidence in such systems. Nevertheless,…
We use algebraic geometry to study matrix rigidity, and more generally, the complexity of computing a matrix-vector product, continuing a study initiated by Kumar, et. al. We (i) exhibit many non-obvious equations testing for (border)…
We consider Proof Complexity in light of the unusual binary encoding of certain combinatorial principles. We contrast this Proof Complexity with the normal unary encoding in several refutation systems, based on Resolution and Integer Linear…
We show that the decision problem for the basic system of interpretability logic IL is PSPACE-complete. For this purpose we present an algorithm which uses polynomial space with respect to the complexity of a given formula. The existence of…
In various provers and deductive verification tools, logical transformations are used extensively in order to reduce a proof task into a number of simpler tasks. Logical transformations are often part of the trusted base of such tools. In…
A principled approach to the design of program verification and con- struction tools is applied to separation logic. The control flow is modelled by power series with convolution as separating conjunction. A generic construction lifts…
The R-matrix formalism for the construction of integrable systems with infinitely many degrees of freedom is reviewed. Its application to Poisson, noncommutative and loop algebras as well as central extension procedure are presented. The…
In this paper we describe an algorithm for implicitizing rational hypersurfaces in case there exists at most a finite number of base points. It is based on a technique exposed in math.AG/0210096, where implicit equations are obtained as…
The linearization of complex ordinary differential equations is studied by extending Lie's criteria for linearizability to complex functions of complex variables. It is shown that the linearization of complex ordinary differential equations…
In this paper, we assess the complexity results of formalisms that describe the feature theories used in computational linguistics. We show that from these complexity results no immediate conclusions can be drawn about the complexity of the…
In this paper, we determine the complexity of the satisfiability problem for various logics obtained by adding numerical quantifiers, and other constructions, to the traditional syllogistic. In addition, we demonstrate the incompleteness of…
We present a framework in Isabelle for verifying asymptotic time complexity of imperative programs. We build upon an extension of Imperative HOL and its separation logic to include running time. In addition to the basic arguments, our…