Interpolation and Quantifiers in Ortholattices

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

We study the proof theory and algorithms for orthologic, a logical system based on ortholattices, which have shown practical relevance in simplification and normalization of verification conditions. Ortholattices weaken Boolean algebras while having polyno ...

Motivated by the transfer of proofs between proof systems, and in particular from first order automated theorem provers (ATPs) to interactive theorem provers (ITPs), we specify an extension of the TPTP derivation text format to describe proofs in first-ord ...

The goal of this thesis is the development and the analysis of numerical methods for problems where the unknown is a curve on a smooth manifold. In particular, the thesis is structured around the three following problems: homotopy continuation, curve inter ...

This paper presents a theoretical analysis of linear interpolation as a principled method for stabilizing (large-scale) neural network training. We argue that instabilities in the optimization process are often caused by the nonmonotonicity of the loss lan ...

The accurate, robust and efficient transfer of the deformation gradient tensor between meshes of different resolution is crucial in cardiac electromechanics simulations. This paper presents a novel method that combines rescaled localized Radial Basis Funct ...

This data set provides a computer-assisted proof for the kernel inequalities needed to prove universal optimality in the paper "Universal optimality of the E_8 and Leech lattices and interpolation formulas" (by Cohn, Kumar, Miller, Radchenko, and Viazovska ...

Detailed chemical abundances of very metal-poor (VMP; [Fe/H] < -2) stars are important for better understanding the first stars, early star formation, and chemical enrichment of galaxies. Big on-going and coming high-resolution spectroscopic surveys provid ...

This paper focuses on over-parameterized deep neural networks (DNNs) with ReLU activation functions and proves that when the data distribution is well-separated, DNNs can achieve Bayesoptimal test error for classification while obtaining (nearly) zero-trai ...

Reduced-order models are indispensable for multi-query or real-time problems. However, there are still many challenges to constructing efficient ROMs for time-dependent parametrized problems. Using a linear reduced space is inefficient for time-dependent n ...

We obtain new Fourier interpolation and uniqueness results in all dimensions, extending methods and results by the first author and M. Sousa [11] and the second author [12]. We show that the only Schwartz function which, together with its Fourier transform ...

Let K be a totally real number field of degree n >= 2. The inverse different of K gives rise to a lattice in Rn. We prove that the space of Schwartz Fourier eigenfunctions on R-n which vanish on the "component-wise square root" of this lattice, is infinite ...

We propose a new approach for normalization and simplification of logical formulas. Our approach is based on algorithms for lattice-like structures. Specifically, we present two efficient algorithms for computing a normal form and deciding the word problem ...

Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we m ...

Fourier transforms are an often necessary component in many computational tasks, and can be computed efficiently through the fast Fourier transform (FFT) algorithm. However, many applications involve an underlying continuous signal, and a more natural choi ...

In several machine learning settings, the data of interest are well described by graphs. Examples include data pertaining to transportation networks or social networks. Further, biological data, such as proteins or molecules, lend themselves well to graph- ...

The underlying geometrical structure of the latent space in deep generative models is in most cases not Euclidean, which may lead to biases when comparing interpolation capabilities of two models. Smoothness and plausibility of linear interpolations in lat ...

In every dimension d >= 2, we give an explicit formula that expresses the values of any Schwartz function on R-d only in terms of its restrictions, and the restrictions of its Fourier transform, to all origin-centered spheres whose radius is the square roo ...

This work is concerned with approximating a trivariate function defined on a tensor-product domain via function evaluations. Combining tensorized Chebyshev interpolation with a Tucker decomposition of low multilinear rank yields function approximations tha ...

This paper should be considered as an addendum to [A. Buffa and C. Giannelli, Adaptive isogeometric methods with hierarchical splines: Error estimator and convergence, Math. Models Methods Appl. Sci. 26 (2016) 1-25] and [A. Buffa and C. Giannelli, Adaptive ...

Many engineering fields rely on frequency-domain dynamical systems for the mathematical modeling of physical (electrical/mechanical/etc.) structures. With the growing need for more accurate and reliable results, the computational burden incurred by frequen ...

Interpolation and Quantifiers in Ortholattices

Chat with Graph Search

Orthologic with Axioms

SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus

Retraction-based numerical methods for continuation, interpolation and time integration on manifolds

Stable Nonconvex-Nonconcave Training via Linear Interpolation

Preserving the positivity of the deformation gradient determinant in intergrid interpolation by combining RBFs and SVD: Application to cardiac electromechanics

Computer-assisted proof of kernel inequalities

Analysis of accretion disc structure and stability using open code for vertical structure

Benign Overfitting in Deep Neural Networks under Lazy Training

Non-intrusive data-driven reduced-order modeling for time-dependent parametrized problems

Perturbed Fourier uniqueness and interpolation results in higher dimensions

Fourier non-uniqueness sets from totally real number fields

Formula Normalizations in Verification

Scaling Language Features for Program Verification

pyFFS: A Python Library for Fast Fourier Series Computation and Interpolation with GPU Acceleration

Graph Representation Learning with Optimal Transport: Analysis and Applications

On Linear Interpolation in the Latent Space of Deep Generative Models

Fourier Interpolation From Spheres

Functional Tucker Approximation Using Chebyshev Interpolation

Remarks on Poincare and interpolation estimates for Truncated Hierarchical B-splines

Model order reduction based on functional rational approximants for parametric PDEs with meromorphic structure