Publication

Interpolation for Synthesis on Unbounded Domains

Publications associées (26)

Graph Chatbot

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

Connectez-vous pour utiliser Chat avec Graph Search

Orthologic with Axioms

Viktor Kuncak, Simon Guilloud

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

2024

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

2023

On Polynomial Algorithms for Normalizing Formulas

Viktor Kuncak, Simon Guilloud, Mario Bucev

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

2022

BLOOM: Bimodal Lattice One-out-of-Many Proofs and Applications

Ngoc Khanh Karol Nguyen

We give a construction of an efficient one-out-of-many proof system, in which a prover shows that he knows the pre-image for one element in a set, based on the hardness of lattice problems. The construction employs the recent zero-knowledge framework of Ly ...

SPRINGER INTERNATIONAL PUBLISHING AG2022

A decomposition of multicorrelation sequences for commuting transformations along primes

Florian Karl Richter

A decomposition of multicorrelation sequences for commuting transformations along primes, Discrete Analysis 2021:4, 27 pp. Szemerédi's theorem asserts that for every positive integer

k

and every

\delta>0

there exists

n

such that every subset of ${1, ...

2021

Local invertibility and sensitivity of atomic structure-feature mappings

Michele Ceriotti, Sergey Pozdnyakov

Background: The increasingly common applications of machine-learning schemes to atomic-scale simulations have triggered efforts to better understand the mathematical properties of the mapping between the Cartesian coordinates of the atoms and the variety o ...

2021

An Ink–and–Paper Automaton: The Conceptual Mechanization of Cognition and the Practical Automation of Reasoning in Leibniz’s De Affectibus (1679)

Simon François Dumas Primbault

On ten loose handwritten folios dating back from April 1679, Leibniz gradually devised, in the course of three days, a full-blown theory of thought that nonetheless remained unpublished and still has received little attention from scholars. Conceiving of a ...

2020

Improving Circuit Mapping Performance Through MIG-based Synthesis for Carry Chains

Giovanni De Micheli, Paolo Ienne, Mathias Soeken, Grace Zgheib, Pierre-Emmanuel Julien Marc Gaillardon, Luca Gaetano Amarù, Xifan Tang, Ana Petkovska, Zhufei Chu

Hard-wired carry chains in FPGAs are designed to improve efficiency of important arithmetic primitives. Although they are proven to be effective for arithmetic-rich functions, there are very few studies on the optimization opportunities of carry chains for ...

ACM2017

Synthesizing efficient systems in probabilistic environments

Barbara Jobstmann, David Parker

We present a formalism, algorithms and tools to synthesise reactive systems that behave efficiently, i.e., which achieve an optimal trade-off between a given cost and reward model. Synthesis aims to automatically generate a program from a specification. Mo ...

Springer2016

Small subset sums

Gergely Ambrus

Let parallel to.parallel to be a norm in R-d whose unit ball is B. Assume that V subset of B is a finite set of cardinality n, with Sigma(v is an element of V) v = 0. We show that for every integer k with 0

Elsevier Science Inc2016

A decomposition of multicorrelation sequences for commuting transformations along primes

Florian Karl Richter

A decomposition of multicorrelation sequences for commuting transformations along primes, Discrete Analysis 2021:4, 27 pp. Szemerédi's theorem asserts that for every positive integer

k

and every

\delta>0

there exists

n

such that every subset of ${1, ...

2021