Publication

LISA – A Modern Proof System

Publications associées (30)

Orthologic with Axioms

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

Association for Computing Machinery2024

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

Simon Guilloud

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

2024

Analytical Computation of the Sensitivity Coefficients in Hybrid AC/DC Networks

Mario Paolone, Willem Lambrichts

In this paper, we present a model for the analytical computation of the power flow sensitivity coefficients (SCs) for hybrid AC/DC networks. The SCs are defined as the partial derivates of the nodal voltages with respect to the active and reactive power in ...

2024

Non-planarity of Markoff graphs mod p

Matthew De Courcy-Ireland

We prove the non-planarity of a family of 3-regular graphs constructed from the solutions to the Markoff equation x2 + y2 + z2 = xyz modulo prime numbers greater than 7. The proof uses Euler characteristic and an enumeration of the short cycles in these gr ...

European Mathematical Soc-Ems2024

A Streamline Upwind Petrov-Galerkin Reduced Order Method for Advection-Dominated Partial Differential Equations Under Optimal Control

Gianluigi Rozza, Fabio Zoccolan

In this paper we will consider distributed Linear-Quadratic Optimal Control Problems dealing with Advection-Diffusion PDEs for high values of the Peclet number. In this situation, computational instabilities occur, both for steady and unsteady cases. A Str ...

Walter De Gruyter Gmbh2024

Secure Interface Design Leveraging Hardware/Software Support

Atri Bhattacharyya

Computer systems rely heavily on abstraction to manage the exponential growth of complexity across hardware and software. Due to practical considerations of compatibility between components of these complex systems across generations, developers have favou ...

EPFL2024

Measurement of the K+ → π+γγ decay

Alessandro Mapelli, Radoslav Marchevski, Alina Kleimenova

A sample of 3984 candidates of the K+ -> pi(+)gamma gamma decay, with an estimated background of 291 +/- 14 events, was collected by the NA62 experiment at CERN during 2017-2018. In order to describe the observed di-photon mass spectrum, the next-to-leadin ...

Elsevier2024

Computer-assisted proof of kernel inequalities

Maryna Viazovska, Abhinav Kumar

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

EPFL Infoscience2023

A Gapless Post-quantum Hash Proof System in the Hamming Metric

Serge Vaudenay, Bénédikt Minh Dang Tran

A hash proof system (HPS) is a form of implicit proof of membership to a language. Out of the very few existing post-quantum HPS, most are based on languages of ciphertexts of code-based or lattice-based cryptosystems and inherently suffer from a gap cause ...

2023

Public-Key Encryption with Quantum Keys

Khashayar Barooti

In the framework of Impagliazzo's five worlds, a distinction is often made between two worlds, one where public-key encryption exists (Cryptomania), and one in which only one-way functions exist (MiniCrypt). However, the boundaries between these worlds can ...

Springer International Publishing Ag2023

Effective Inhibition of TDP-43 Aggregation by Native State Stabilization

Hilal Lashuel, Lixin Yang, Yllza Jasiqi

Preventing the misfolding or aggregation of transactive response DNA binding protein with 43 kDa (TDP-43) is the most actively pursued disease-modifying strategy to treat amyotrophic lateral sclerosis and other neurodegenerative diseases. In this work, we ...

Wiley-VCH Verlag GmbH2024

End-to-end kernel learning via generative random Fourier features

Jie Yang, Fanghui Liu

Random Fourier features (RFFs) provide a promising way for kernel learning in a spectral case. Current RFFs-based kernel learning methods usually work in a two-stage way. In the first-stage process, learn-ing an optimal feature map is often formulated as a ...

ELSEVIER SCI LTD2023

Wide-scale identification of novel/eliminated genes responsible for evolutionary transformations

Daria Korotkova

BackgroundIt is generally accepted that most evolutionary transformations at the phenotype level are associated either with rearrangements of genomic regulatory elements, which control the activity of gene networks, or with changes in the amino acid conten ...

2023

Byzantine-Resilient Learning Beyond Gradients: Distributing Evolutionary Search

Rachid Guerraoui, Andrei Kucharavy, Matteo Monti

Modern machine learning (ML) models are capable of impressive performances. However, their prowess is not due only to the improvements in their architecture and training algorithms but also to a drastic increase in computational power used to train them.|S ...

Assoc Computing Machinery2023

Graph-based approximate message passing iterations

Raphaël Jean Berthier

Approximate message passing (AMP) algorithms have become an important element of high-dimensional statistical inference, mostly due to their adaptability and concentration properties, the state evolution (SE) equations. This is demonstrated by the growing ...

OXFORD UNIV PRESS2023

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

Mean flow modeling in high-order nonlinear Schrodinger equations

Debbie Eeltink

The evaluation and consideration of the mean flow in wave evolution equations are necessary for the accurate prediction of fluid particle trajectories under wave groups, with relevant implications in several domains, from the transport of pollutants in the ...

2023

Duality and bicrystals on infinite binary matrices

Thomas Gerber

The set of finite binary matrices of a given size is known to carry a finite type AA bicrystal structure. We first review this classical construction, explain how it yields a short proof of the equality between Kostka polynomials and one-dimensional sums t ...

2023

Shafranov shift correction to the Furth-Yoshikawa scaling of tokamak adiabatic compression

Olivier Sauter

In 1970, Furth and Yoshikawa (1970 Phys. Fluids 13 2593-6) introduced the scalings of adiabatic plasma compression. Basically, if the shape of the external plasma boundary and the aspect ratio are preserved during the compression, then the density, kinetic ...

2023

Measurement of the 171Tm beta spectrum

Alexey Boyarsky, Lesya Shchutska

The beta spectrum of the main transition of the 171Tm was measured using a double focalizing spectrometer. The instrument was lately improved in order to reduce its low energy threshold to 34 keV. We used the spectrometer to measure the energy end-point of ...

2023