Concept
Élimination des quantificateurs
Publications associées (33)
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 ...
2024Interpolation 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 ...
Cham2024Decision Procedures for Power Structures
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 ...
EPFL2023NP Satisfiability for Arrays as Powers
We show that the satisfiability problem for the quantifier-free theory of product structures with the equicardinality relation is inNP. As an application, we extend the combinatory array logic fragmentto handle cardinality constraints. The resulting fragme ...
Springer, Cham2022Scaling Language Features for Program Verification
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 ...
EPFL2022Complexity of linear relaxations in integer programming
For a set X of integer points in a polyhedron, the smallest number of facets of any polyhedron whose set of integer points coincides with X is called the relaxation complexity rc(X). This parameter was introduced by Kaibel & Weltge (2015) and captures the ...
2020Experimental study of impulse waves generated by viscoplastic fluid
Landslide-generated waves, also called impulse waves, occur as a result of the intrusion of landslides (such as rock falls, debris flows, and avalanches) into bodies of water (such as lakes, reservoirs, and seas). The objective of this thesis was to study ...
EPFL2020Data-driven integration of hippocampal CA1 synaptic physiology in silico
Eilif Benjamin Muller, Srikanth Ramaswamy, Michael Reimann, Armando Romani, András Ecker, Michele Migliore, Szabolcs Kali, Sàra Sàray, Audrey Mercer
The anatomy and physiology of monosynaptic connections in rodent hippocampal CA1 have been extensively studied in recent decades. Yet, the resulting knowledge remains disparate and difficult to reconcile. Here, we present a data-driven approach to integrat ...
2020Verified Functional Programming
In this thesis, we present Stainless, a verification system for an expressive subset of the Scala language.
Our system is based on a dependently-typed language and an algorithmic type checking procedure
which ensures total correctness. We rely on SMT solve ...
EPFL2019Solving quantified linear arithmetic by counterexample-guided instantiation
Viktor Kuncak, Andrew Joseph Reynolds
This paper presents a framework to derive instantiation-based decision procedures for satisfiability of quantified formulas in first-order theories, including its correctness, implementation, and evaluation. Using this framework we derive decision procedur ...
2017