Publications associées à Logique intuitionniste

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

Springer International Publishing Ag2024

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

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

Association for Computing Machinery2024

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

Formula Normalizations in Verification

Viktor Kuncak, Simon Guilloud, Mario Bucev, Dragana Milovancevic

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

2023

Article Structure and functionality of a multimeric human COQ7:COQ9 complex

Matteo Dal Peraro, Luciano Andres Abriata

Coenzyme Q (CoQ) is a redox-active lipid essential for core metabolic pathways and antioxidant defense. CoQ is synthesized upon the mitochondrial inner membrane by an ill-defined "complex Q" metabolon. Here, we present structure-function analyses of a lipi ...

CELL PRESS2022

Working on mobility from people

Vincent Kaufmann

Describing, understanding, explaining and regulating mobility requires transversal approaches. Traditionally, mobility analysis proceeds by partitioning into four differentiated forms according to two dimensions: the temporality of which it is based and th ...

Routledge2021

chi-Shell, a new spatial deployable lattice compared to traditional reticulated shells

Mark Pauly, Florin Isvoranu, Etienne Bouleau, Francis Julian Panetta

The chi-Shells is a new kind of deployable reticulated shells that has features comparable to other traditional shells. Its deployment uses the mechanical properties of a beam grid to generate a three-dimensional shape. This new generation of reticulated s ...

INT CENTER NUMERICAL METHODS ENGINEERING2019

X-Shell, a new spatial deployable lattice compared to traditional reticulated shells

Mark Pauly, Florin Isvoranu, Francis Julian Panetta, Etienne Bouleau

The χ-Shells is a new kind of deployable reticulated shells that has features comparable to other traditional shells. Its deployment uses the mechanical properties of a beam grid to generate a three-dimensional shape. This new generation of reticulated she ...

International Association for Shell and Spatial Structures (IASS)2019

Scaling-up ESOP Synthesis for Quantum Compilation

Giovanni De Micheli, Mathias Soeken, Bruno Schmitt Antunes

Today's rapid advances in quantum computing hardware call for scalable synthesis methods to map combinational logic represented as multi-level Boolean networks (e.g., an and inverter graph, AIG) to quantum circuits. Such synthesis process must yield revers ...

IEEE2019