This thesis describes an efficient method for speeding up functional verification of arithmetic circuits namely linear network such as wallace trees, counters using linear algebra techniques. The circuit is represented as a network of half adders, full adders and inverters, and modeled as a system of linear equations. The proof of functional correctness of the design is obtained by computing its algebraic signature using standard linear programming (LP) solver and comparing it with the reference signature provided by the designer. Initial experimental results and comparison with Satisfiability Modulo Theorem (SMT) solvers show that the method is efficient, scalable and applicable to complex arithmetic designs, including large multipliers. It is intended to provide a new front end theory/engine to enhance SMT solvers.

[ES] Durante las primeras décadas del siglo pasado se estudiaron las inversas generalizadas que hoy en día se conocen como inversas generalizadas clásicas. Entre ellas cabe mencionar la inversa de Moore-Penrose (1955) y la inversa de Drazin (1958). Mientras que la inversa de Moore-Penrose se definió originalmente para matrices complejas rectangulares, la inversa de Drazin fue tratada, en un primer momento, únicamente para matrices cuadradas. Más tarde, en 1980, Cline y Greville realizaron la extensión del caso cuadrado al caso rectangular, mediante la consideración de una matriz de ponderación rectangular. Diferentes propiedades, caracterizaciones y aplicaciones fueron obtenidas para estos tipos de inversas generalizadas hasta finales del siglo pasado. En la última década, han aparecido nuevas nociones de inversas generalizadas. La primera de ellas fue la inversa core, introducida en el año 2010 por los autores Baksalary y Trenkler. La misma tuvo una amplia repercusión en la comunidad matemática debido a la sencillez de su definición, a su aplicación en la resolución de algunos sistemas lineales con restricciones que surgen en la teoría de redes eléctricas y también por su conexión con la inversa de Bott- Duffin. Muchos trabajos de investigación han surgido a partir de la inversa core, incluyendo sus extensiones a conjuntos más generales como el álgebra de operadores lineales acotados sobre espacios de Hilbert y/o al ámbito de anillos abstractos. El objetivo principal de esta tesis doctoral es definir y estudiar en profundidad una nueva inversa generalizada para matrices rectangulares, llamada inversa inversa de grupo débil ponderada, la cual extiende al caso rectangular la inversa de grupo débil recientemente definida (para el caso cuadrado) por Wang y Chen. También se considera un amplio estudio de la inversa core-EP ponderada definida por Ferreyra, Levis y Thome en el año 2018, y que extiende al caso rectangular inversa core-EP introducida por Manjunatha-Prasad y Mohana en el año 2014. Para ambas inversas generalizadas se obtienen nuevas propiedades, representaciones, caracterizaciones como así también su relación con otras inversas conocidas en la literatura. Además, se presentan dos algoritmos que permiten realizar un cálculo efectivo de las mismas. / [CA] Durant les primeres dècades del segle passat es van estudiar les inverses generalitzades que hui dia es coneixen com a inverses generalitzades clàssiques. Entre elles cal esmentar la inversa de Moore-Penrose (1955) i la inversa de Drazin (1958). Mentre que la inversa de Moore-Penrose es va definir originalment per a matrius complexes rectangulars, la inversa de Drazin va ser tractada, en un primer moment, únicament per a matrius quadrades. Més tard, en 1980, Cline i Greville van realitzar l'extensió del cas quadrat al cas rectangular, mitjançant la consideració d'una matriu de ponderació rectangular. Diferents propietats, caracteritzacions i aplicacions van ser obtingudes per a aquests tipus d'inverses generalitzades fins a finals del segle passat. En l'última dècada, han aparegut noves nocions d'inverses generalitzades. La primera d'elles va ser la inversa core, introduïda l'any 2010 pels autors Baksalary i Trenkler. La mateixa va tindre una àmplia repercussió en la comunitat matemàtica a causa de la senzillesa de la seua definició, a la seua aplicació en la resolució d'alguns sistemes lineals amb restriccions que sorgeixen en la teoria de xarxes elèctriques i també per la seua connexió amb la inversa de Bott-Duffinn. Molts treballs de recerca han sorgit a partir de la inversa core, incloent les seues extensions a conjunts més generals com l'àlgebra d'operadors lineals delimitats sobre espais de Hilbert i/o a l'àmbit d'anells abstractes. L'objectiu principal d'aquesta tesi doctoral és definir i estudiar en profunditat una nova inversa generalitzada per a matrius rectangulars, anomenada inversa inversa de grup feble ponderada, la qual estén al cas rectangular la inversa de grup feble recentment definida (per al cas quadrat) per Wang i Chen. Tamb é es considera un ampli estudi de la inversa core-EP ponderada definida per Ferreyra, Levis i Thome l'any 2018, i que estén al cas rectangular inversa core-EP introduïda per Manjunatha-Prasad i Mohana l'any 2014. Per a totes dues inverses generalitzades s'obtenen noves propietats, representacions, caracteritzacions com així també la seua relació amb altres inverses conegudes en la literatura. A més, es presenten dos algorismes que permeten realitzar un càlcul efectiu d'aquestes. / [EN] Generalized inverses, known today as Classical Generalized Inverses, were studied during the first decades of the last century. Two important classical generalized inverses are the Moore-Penrose inverse (1955) and the Drazin inverse (1958). The Moore-Penrose inverse was originally defined for complex rectangular matrices. In turn, the Drazin inverse was studied, at first, only for square matrices. It was in 1980 when Cline and Greville extended the case of square matrices to the case of rectangular matrices by considering a weight rectangular matrix. Throughout the entire past century there appeared difierent properties, characterizations and applications of these types of generalized inverses. This last decade gave rise to new notions of generalized inverses. The first of these new notions is known as the core inverse. Core inverses were introduced in 2010 by Baksalary and Trenkler. Their work had a wide repercussion in the mathematical community due to the simplicity of its denition and its application in the solution of some linear systems with restrictions. The core inverse further gain in interest due to their connection to the Bott-Duffin inverse. There is a large body of work on the core inverse, including extensions to more general sets if such as the algebra of bounded linear operators on Hilbert spaces and/or abstract rings. The main goal of this thesis is to define and study in depth a new generalized inverse for rectangular matrices. This new inverse is called weighted weak group inverse (or weighted WG inverse). Weighted WG inverses extend weak group inverse, recently defined for the square case by Wang and Chen, to the rectangular case. We also consider an extensive study of the weighted core-EP inverse. The latter type of inverse was dened by Ferreyra, Levis, and Thome in 2018. This inverse extends the core-EP inverse introduced by Manjunatha- Prasad and Mohana in 2014 to the rectangular case. This thesis presents new properties, representations, characterizations, as well as their relation with other inverses known in the literature are obtained, for weighted WG inverses and weighted core-EP inverse. In addition, the thesis presents two algorithms that allow for an efiective computation weighted WG inverses and weighted core-EP inverse. / Orquera, V. (2022). La inversa core-EP y la inversa de grupo débil para matrices rectangulares [Tesis doctoral]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/185227 / TESIS

Visualization of three-dimensional vector operations can be very helpful in understanding vector mathematics. However, creating these visualizations using traditional WIMP interfaces can be a troublesome exercise. In this thesis, we present VectorPad, a pen-based application for three-dimensional vector mathematics visualization. VectorPad allows users to define vectors and perform mathematical operations upon them through the recognition of handwritten mathematics. The VectorPad user interface consists of a sketching area, where the user can write vector definitions and other mathematics, and a 3D graph for visualization. After recognition, vectors are visualized dynamically on the graph, which can be manipulated by the user. A variety of mathematical operations can be performed, such as addition, subtraction, scalar multiplication, and cross product. Animations show how operations work on the vectors. We also performed a short, informal user study evaluating the user interface and visualizations of VectorPad. VectorPad's visualizations were generally well liked; results from the study show a need to provide a more comprehensive set of visualization tools as well as refinement to some of the animations.

No description available.

No description available.

No description available.

<p>Proofs are notoriously difficult. While the challenges students face when working on proofs are well-documented, more research is needed on what students do when working on proofs, especially in the context of linear algebra. My research focuses on student work on proofs in linear algebra through the lens of Tall's worlds of mathematics: the embodied world, the symbolic world, and the formal world. The embodied world consists of graphs, diagrams, and their properties. The symbolic world contains operations, formulas, and calculations. The formal world consists of axioms, formal definitions, and formal proofs. I conducted task-based interviews with linear algebra students in which they determined if given proofs were valid and then constructed their own proofs for different statements. In different interviews, I encouraged participants to use different worlds of mathematics. Through this study, I hoped to gain some understanding of how approaches to proof constructions and validations within the different worlds of mathematics affect students' personal proof constructions and validations. I also sought to understand what participants viewed as challenging or helpful about each world of mathematics with regards to proofs.</p> <p><br></p> <p>I found that participants often chose a world of mathematics based on the given topic rather than their preferred world or my encouragement to use a given world. Encouraging participants to use the embodied world resulted in their using generic examples. Encouraging participants to use the symbolic or formal worlds had little effect, likely due to participants' views of the symbolic and formal worlds which differed from my views of the symbolic and formal worlds. Participants said the embodied world was helpful for developing understanding, but felt limited by its specificity. A challenge of the symbolic world was the level of precision needed and the large number of variables. Participants viewed the formal world as helpful for proofs and its generality, but logic was a challenge. Reflecting on the study, participants said that the three-world framework was helpful for organizing their thoughts when working on problems.</p>

Krylov subspace iterative methods provide an effective tool for reducing the solution of large linear systems to a size for which a direct solver may be applied. However, the problems of limited storage and speed are still a concern. Therefore, in this dissertation work, we present iterative Krylov subspace algorithms for non-Hermitian systems which do have fixed memory requirements and have favorable convergence characteristics. This dissertation describes three projects. The first project concerns short-term recurrence Krylov subspace methods for nearly-Hermitian linear systems. In 2008, Beckermann and Reichel introduced a short-term recurrence progressive GMRES algorithm for nearly-Hermitian linear systems. However, we have found this method to be unstable. We document the instabilities and introduce a different fixed-memory algorithm to treat nearly-Hermitian problems. We present numerical experiments demonstrating that the performance of this algorithm is competitive. The other two projects involve extending a strategy called Krylov subspace recycling, introduced by Parks and colleagues in 2005. This method requires more overhead than other subspace augmentation methods but offers the ability to recycle subspace information between cycles for a single linear system and recycle information between related linear systems. In the first project, we extend subspace recycling to the block Krylov subspace setting. A block Krylov subspace is a generalization of Krylov subspace where a single starting vector is replaced with a block of linearly independent starting vectors. We then apply our method to a sequence of matrices arising in a Newton iteration applied to fluid density functional theory and present some numerical experiments. In the second project, we extend the methods of subspace recycling to a family of linear systems differing only by multiples of the identity. These problems arise in the theory of quantum chromodynamics, a theory of the behavior of subatomic particles. We wish to build on the class of Krylov methods which allow the simultaneous solution of all shifted linear systems while generating only one subspace. However, the mechanics of subspace recycling complicates this situation and interferes with our ability to simultaneously solve all systems using these techniques. Therefore, we introduce an algorithm which avoids this complication and present some numerical experiments demonstrating its effectiveness. / Mathematics

This thesis is concerned with the fast iterative solution of linear systems of equations of saddle point form. Saddle point problems are a ubiquitous class of matrices that arise in a host of computational science and engineering applications. The focus here is on improving the convergence of iterative methods for these problems by preconditioning. Preconditioning is a way to transform a given linear system into a different problem for which iterative methods converge faster. Saddle point matrices have a very specific block structure and many preconditioning strategies for these problems exploit this structure. The preconditioners considered in this thesis are constraint preconditioners. This class of preconditioner mimics the structure of the original saddle point problem. In this thesis, we prove norm- and field-of-values-equivalence for constraint preconditioners associated to saddle point matrices with a particular structure. As a result of these equivalences, the number of iterations needed for convergence of a constraint preconditioned minimal residual Krylov subspace method is bounded, independent of the size of the matrix. In particular, for saddle point systems that arise from the finite element discretization of partial differential equations (p.d.e.s), the number of iterations it takes for GMRES to converge for theses constraint preconditioned systems is bounded (asymptotically), independent of the size of the mesh width. Moreover, we extend these results when appropriate inexact versions of the constraint preconditioner are used. We illustrate this theory by presenting numerical experiments on saddle point matrices that arise from the finite element solution of coupled Stokes-Darcy flow. This is a system of p.d.e.s that models the coupling of a free flow to a porous media flow by conditions across the interface of the two flow regions. We present experiments in both two and three dimensions, using different types of elements (triangular, quadrilateral), different finite element schemes (continuous, discontinuous Galerkin methods), and different geometries. In all cases, the effectiveness of the constraint preconditioner is demonstrated. / Mathematics

Quantum random walks are a generalization of classical Markovian random walks to a quantum mechanical or quantum computing setting. Quantum walks have promising applications but are complicated by quantum decoherence. We prove that the long-time limiting behavior of the class of quantum operations which are the convex combination of norm one operators is governed by the eigenvectors with norm one eigenvalues which are shared by the operators. This class includes all operations formed by a coherent operation with positive probability of orthogonal measurement at each step. We also prove that any operation that has range contained in a low enough dimension subspace of the space of density operators has limiting behavior isomorphic to an associated Markov chain. A particular class of such operations are coherent operations followed by an orthogonal measurement. Applications of the convergence theorems to quantum walks are given. / Mathematics