Publications associées à Calcul des prédicats

Efficient Continual Finite-Sum Minimization

Volkan Cevher, Efstratios Panteleimon Skoulakis, Leello Tadesse Dadi

Given a sequence of functions

f_1,\ldots,f_n

with

f_i:\mathcal{D}\mapsto \mathbb{R}

, finite-sum minimization seeks a point

{x}^\star \in \mathcal{D}

minimizing

\sum_{j=1}^nf_j(x)/n

. In this work, we propose a key twist into the finite-sum minimizat ...

2024

Scalable Logic Rewriting Using Don’t Cares

Giovanni De Micheli, Alessandro Tempia Calvino

Logic rewriting is a powerful optimization technique that replaces small sections of a Boolean network with better implementations. Typically, exact synthesis is used to compute optimum replacement on-the-fly, with possible support for Boolean don't cares. ...

2024

A Reduced Order Model for Domain Decompositions with Non-conforming Interfaces

Alfio Quarteroni, Andrea Manzoni

In this paper, we propose a reduced-order modeling strategy for two-way Dirichlet-Neumann parametric coupled problems solved with domain-decomposition (DD) sub-structuring methods. We split the original coupled differential problem into two sub-problems wi ...

Springer/Plenum Publishers2024

Interpolation and Quantifiers in Ortholattices

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We study quantifiers and interpolation properties in ortho- logic, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical logic, yet has a quadratic-time decision procedure. We present a sequent-based p ...

2024

Interpolation and Quantifiers in Ortholattices

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We study quantifiers and interpolation properties in orthologic, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical logic, yet has a quadratic-time decision procedure. We present a sequent-based pro ...

Springer International Publishing Ag2024

Decision Procedures for Power Structures

Rodrigo Raya

We study the decision problem for the existential fragment of the theory of power structures. We prove complexity results that parallel the decidability results of Feferman-Vaught for the theories of product structures thereby showing that the construction ...

EPFL2023

LISA – A Modern Proof System

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We present LISA, a proof system and proof assistant for constructing proofs in schematic first-order logic and axiomatic set theory. The logical kernel of the system is a proof checker for first-order logic with equality and schematic predicate and fun ...

Dagstuhl, Germany, Schloss Dagstuhl - Leibniz-Zentrum fur Informatik2023

Energy Efficient Logic and Memory Design With Beyond-CMOS Magnetoelectric Spin-Orbit (MESO) Technology Toward Ultralow Supply Voltage

Kyojin Choo

Devices based on the spin as the fundamental computing unit provide a promising beyond-complementary metal-oxide-semiconductor (CMOS) device option, thanks to their energy efficiency and compatibility with CMOS. One such option is a magnetoelectric spin-or ...

Ieee-Inst Electrical Electronics Engineers Inc2023

Validating functional redundancy with mixed generative adversarial networks

Thanh Trung Huynh, Quoc Viet Hung Nguyen, Thành Tâm Nguyên, Trung-Dung Hoang

Data redundancy has been one of the most important problems in data-intensive applications such as data mining and machine learning. Removing data redundancy brings many benefits in efficient data updating, effective data storage, and error-free query proc ...

ELSEVIER2023

Adaptive Symplectic Model Order Reduction Of Parametric Particle-Based Vlasov-Poisson Equation

Jan Sickmann Hesthaven, Nicolò Ripamonti, Cecilia Pagliantini

. High-resolution simulations of particle-based kinetic plasma models typically require a high number of particles and thus often become computationally intractable. This is exacerbated in multi-query simulations, where the problem depends on a set of para ...

AMER MATHEMATICAL SOC2023

Power variations in fractional Sobolev spaces for a class of parabolic stochastic PDEs

Robert Dalang, Carsten Hao Ye Chong

We consider a class of parabolic stochastic PDEs on bounded domains D c Rd that includes the stochastic heat equation but with a fractional power gamma of the Laplacian. Viewing the solution as a process with values in a scale of fractional Sobolev spaces ...

INT STATISTICAL INST2023

Snap buckling of bistable beams under combined mechanical and magnetic loading

Pedro Miguel Nunes Pereira de Almeida Reis, Dong Yan, Tomohiko Sano, Arefeh Abbasi

We investigate the mechanics of bistable, hard-magnetic, elastic beams, combining experiments, finite-element modelling (FEM) and a reduced-order theory. The beam is made of a hard magneto-rheological elastomer, comprising two segments with antiparallel ma ...

ROYAL SOC2023

Higher-order organization of multivariate time series

Enrico Amico, Andrea Santoro

Time series analysis has proven to be a powerful method to characterize several phenomena in biology, neuroscience and economics, and to understand some of their underlying dynamical features. Several methods have been proposed for the analysis of multivar ...

NATURE PORTFOLIO2023

Efficient approximation of cardiac mechanics through reduced-order modeling with deep learning-based operator approximation

Alfio Quarteroni, Andrea Manzoni

Reducing the computational time required by high-fidelity, full-order models (FOMs) for the solution of problems in cardiac mechanics is crucial to allow the translation of patient-specific simulations into clinical practice. Indeed, while FOMs, such as th ...

Wiley2023

Scaling Language Features for Program Verification

Georg Stefan Schmid

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 ...

EPFL2022

Reduced basis methods for numerical room acoustic simulations with parametrized boundaries

Jan Sickmann Hesthaven, Hermes Sampedro Llopis

The use of model-based numerical simulations of wave propagation in rooms for engineering applications requires that acoustic conditions for multiple parameters are evaluated iteratively, which is computationally expensive. We present a reduced basis metho ...

ACOUSTICAL SOC AMER AMER INST PHYSICS2022

Three-Input Gates for Logic Synthesis

Giovanni De Micheli, Mathias Soeken, Dewmini Sudara Marakkalage, Eleonora Testa, Heinz Riener

Most logic synthesis algorithms work on graph representations of logic functions with nodes associated with arbitrary logic expressions or simple logic functions and iteratively optimize such graphs. While recent multilevel logic synthesis efforts focused ...

IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC2021

Reduced-order Models for Simulating Coupled Geometric Instabilities in Steel Beam-columns Under Inelastic Cyclic Straining

Alexander Riley Hartloper

Numerical models that can simulate coupled geometric instabilities in steel beam-columns are required for the seismic assessment of certain steel moment-resisting frames. Reliably simulating coupled instabilities requires that the steel material is precise ...

EPFL2021

Finding Second-Order Stationary Points in Constrained Minimization: A Feasible Direction Approach

Shaul Nadav Hallak

This paper introduces a method for computing points satisfying the second-order necessary optimality conditions for nonconvex minimization problems subject to a closed and convex constraint set. The method comprises two independent steps corresponding to t ...

SPRINGER/PLENUM PUBLISHERS2020

Towards the K(2)-local homotopy groups of Z

Philip Egger

Previously (Adv. Math. 360 (2020) art. id. 106895), we introduced a class (Z) over tilde of 2-local finite spectra and showed that all spectra Z is an element of (Z) over tilde admit a v(2)-self-map of periodicity 1. The aim here is to compute the K(2)-loc ...

GEOMETRY & TOPOLOGY PUBLICATIONS2020