Publication
Some planar isospectral domains
Publications associées (39)
SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus
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 ...
2024LISA – 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 ...
2023A 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 ...
2023A comment on performance guarantees of a greedy algorithm for minimizing a supermodular set function on comatroid
Maryam Kamgarpour, Baiwei Guo, Orcun Karaca
We provide a counterexample to the performance guarantee obtained in the paper "Il'ev, V., Linker, N., 2006. Performance guarantees of a greedy algorithm for minimizing a supermodular set function on comatroid", which was published in Volume 171 of the Eur ...
ELSEVIER2021A dependence of the cost of fast controls for the heat equation on the support of initial datum
The controllability cost for the heat equation as the control time goes to 0 is well-known of the order for some positive constant , depending on the controlled domain and for all initial datum. In this paper, we prove that the constant $C ...
2021Scaling Functional Synthesis and Repair
Program synthesis was first proposed a few decades ago, but in the last decade it has gained increased momentum in the research community. The increasing complexity of software has dictated the urgent need for improved supporting tools that verify the soft ...
EPFL2019A proof of a sumset conjecture of Erdős
In this paper we show that every set A ⊂ ℕ with positive density contains B + C for some pair B, C of infinite subsets of ℕ , settling a conjecture of Erdős. The proof features two different decompositions of an arbitrary bounded sequence into a structured ...
2019Corpora Delicti
CORPORA DELICTI, The Significant Detail. The Corpus Delicti is the evidence of a crime. The term denotes the formation of a proof that allows the unmasking of a perpetrator. In the realm of interpretation and language, it could reveal matter on which an ac ...
MANSLAB2017Localization of emergency acoustic sources by micro aerial vehicles
Dario Floreano, Felix Stephan Schill, Meysam Basiri
For micro aerial vehicles (MAVs) involved in search and rescue missions, the ability to locate the source of a distress sound signal is significantly important and allows fast localization of victims and rescuers during nighttime, through foliage and in du ...
John Wiley & Sons2017Cloaking using complementary media in the quasistatic regime
Cloaking using complementary media was suggested by Lai et al. in [8]. The study of this problem faces two difficulties. Firstly, this problem is unstable since the equations describing the phenomenon have sign changing coefficients, hence the ellipticity ...
2016