Concept

Constructive proof

Related publications (111)

Graph Chatbot

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.

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

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

From concrete waste to walls An investigation of reclamation and digital technologies for new load-bearing structures

Corentin Jean Dominique Fivet, Stefana Parascho, Maxence Grangeot

Our research explores opportunities in using unaltered concrete rubbles from demolition for the digital construction of structural walls. Through research by iterative making, we identify relevant upcycling processes and design strategies and explore new t ...

2023

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

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

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

Impact of Redundancy on Resilience in Distributed Optimization and Learning

Nirupam Gupta, Shuo Liu

This paper considers the problem of resilient distributed optimization and stochastic learning in a server-based architecture. The system comprises a server and multiple agents, where each agent has its own local cost function. The agents collaborate with ...

New York2023

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

Gradient flow dynamics of shallow ReLU networks for square loss and orthogonal inputs

Nicolas Henri Bernard Flammarion, Etienne Patrice Boursier, Loucas Pillaud-Vivien

The training of neural networks by gradient descent methods is a cornerstone of the deep learning revolution. Yet, despite some recent progress, a complete theory explaining its success is still missing. This article presents, for orthogonal input vectors, ...

2022

Further Collapses in TFNP

Mika Tapani Göös, Gilbert Théodore Maystre, Alexandros Paul Hollender, Siddhartha Jain, Ran Tao

We show EOPL = PLS ∩ PPAD. Here the class EOPL consists of all total search problems that reduce to the End-of-Potential-Line problem, which was introduced in the works by Hubáček and Yogev (SICOMP 2020) and Fearnley et al. (JCSS 2020). In particular, our ...

Schloss Dagstuhl - Leibniz-Zentrum für Informatik2022