Related papers: Formalization of Transform Methods using HOL Light
Simulink is a graphical environment that is widely adapted for the modeling and the Laplace transform based analysis of linear analog circuits used in signal processing architectures. However, due to the involvement of the numerical…
Cell injection is an approach used for the delivery of small sample substances into a biological cell and is widely used in drug development, gene injection, intracytoplasmic sperm injection (ICSI) and in-virto fertilization (IVF). Robotic…
This set of theories presents an Isabelle/HOL+Isar formalisation of stream processing components introduces in Focus, a framework for formal specification and development of interactive systems. This is an extended and updated version of…
We study the properties of different type of transforms by means of operational methods and discuss the relevant interplay with many families of special functions. We consider in particular the binomial transform and its generalizations. A…
Despite the considerable interest in new dependent type theories, simple type theory (which dates from 1940) is sufficient to formalise serious topics in mathematics. This point is seen by examining formal proofs of a theorem about…
In this paper, we focus on Fourier analysis and holographic transforms for signal representation. For instance, in the case of image processing, the holographic representation has the property that an arbitrary portion of the transformed…
Higher-Order Hypergraph Learning (HOHL) was recently introduced as a principled alternative to classical hypergraph regularization, enforcing higher-order smoothness via powers of multiscale Laplacians induced by the hypergraph structure.…
We introduce a proof recommender system for the HOL4 theorem prover. Our tool is built upon a transformer-based model [2] designed specifically to provide proof assistance in HOL4. The model is trained to discern theorem proving patterns…
We study Fourier transforms of holonomic D-modules on the complex affine line and show that their enhanced solution complexes are described by a twisted Morse theory. We thus recover and even strengthen the well-known formula for their…
We present a generic framework that facilitates object level reasoning with logics that are encoded within the Higher Order Logic theorem proving environment of HOL Light. This involves proving statements in any logic using intuitive…
Autoformalization has emerged as a term referring to the automation of formalization - specifically, the formalization of mathematics using interactive theorem provers (proof assistants). Its rapid development has been driven by progress in…
In this paper, we utilize Isabelle/HOL to develop a formal framework for the basic theory of double-pushout graph transformation. Our work includes defining essential concepts like graphs, morphisms, pushouts, and pullbacks, and…
Hierarchical proof trees (hiproofs for short) add structure to ordinary proof trees, by allowing portions of trees to be hierarchically nested. The additional structure can be used to abstract away from details, or to label particular…
This paper focuses on the mathematical approaches to the analysis of stability that is a crucial step in the design of dynamical systems. Three methods are presented, namely, absolutely integrable impulse response, Fourier integral, and…
Laplace transforms which admit a holomorphic extension to some sector strictly containing the right half plane and exhibiting a potential behavior are considered. A spectral order, parallelizable method for their numerical inversion is…
Regularization methods are a key tool in the solution of inverse problems. They are used to introduce prior knowledge and make the approximation of ill-posed (pseudo-)inverses feasible. In the last two decades interest has shifted from…
The objective in this paper is to demonstrate that four of the most used techniques in applied mathematics, viz., Fourier series, Fourier transform, Laplace transform and the Fourier-Laplace transform can be introduced using eigenvalue…
This paper presents a new system of logic, LF, that is intended to be used as the foundation of the formalization of science. That is, deductive validity according to LF is to be used as the criterion for assessing what follows from the…
In this study, we introduce and explore a delay differential equation that lends itself to explicit solutions in the Fourier-transformed space. Through the careful alignment of the initial function, we can construct a highly accurate…
This set of theories presents a formalisation in Isabelle/HOL+Isar of data dependencies between components. The approach allows to analyse system structure oriented towards efficient checking of system: it aims at elaborating for a concrete…