Publications related to Intuitionistic logic

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

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

Giovanni De Micheli, Paolo Ienne, Mathias Soeken, Grace Zgheib, Xifan Tang, Pierre-Emmanuel Julien Marc Gaillardon, Ana Petkovska, Luca Gaetano Amarù, 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

Configuration logics: Modeling architecture styles

Joseph Sifakis, Simon Bliudze, Anastasia Mavridou, Eduard Baranov

We study a framework for the specification of architecture styles as families of architectures involving a common set of types of components and coordination mechanisms. The framework combines two logics: 1) interaction logics for the specification of arch ...

Elsevier Science Inc2017

NAND-NOR: A Compact, Fast, and Delay Balanced FPGA Logic Element

Paolo Ienne, Grace Zgheib, Yu Lin, Wei Li

The And-Inverter Cone has been introduced as an alternative logic element to the look-up table in FPGAs, since it improves their performance and resource utilization. However, further analysis of the AIC design showed that it suffers from the delay discrep ...

ACM2017

System and Method for Optimization of Digital Circuits with Timing and Behavior Co-Designed by Introduction and Exploitation of False Paths

Christian Enz, Vincent Frédéric Camus, Jérémy Lucien Maurice Schlachter

A digital circuit including a signal path with a false path, whereby the signal path includes at least 3 logic instances, the digital circuit further including a logic monitoring element for monitoring a part of the digital circuit, and for outputting a cu ...

2017

Higher-Order Subtyping with Type Intervals

Sandro Stucki

Modern, statically typed programming languages provide various abstraction facilities at both the term- and type-level. Common abstraction mechanisms for types include parametric polymorphism -- a hallmark of functional languages -- and subtyping -- which ...

EPFL2017

Configuration Logics: Modelling Architecture Styles

Joseph Sifakis, Simon Bliudze, Anastasia Mavridou, Eduard Baranov

We study a framework for the specification of architecture styles as families of architectures involving a common set of types of components and coordination mechanisms. The framework combines two logics: 1) interaction logics for the specification of arch ...

Springer Int Publishing Ag2015

Cadres de vie, modes de vie et mobilités de loisirs : les vertus de la ville compacte remises en cause?

Sébastien Munafò

This thesis aims to examine the causal mechanisms of living environments on leisure mobilities and verify whether their inclusion is actually able to challenge the compact city as a sustainable urban form. The research focuses on the Swiss case and in part ...

EPFL2015

Multiple Independent Gate FETs: How Many Gates Do We Need?

Giovanni De Micheli, Pierre-Emmanuel Julien Marc Gaillardon, Subhasish Mitra, Luca Gaetano Amarù

Multiple Independent Gate Field Effect Transistors (MIGFETs) are expected to push FET technology further into the semiconductor roadmap. In a MIGFET, supplementary gates either provide (i) enhanced conduction properties or (ii) more intelligent sw ...

IEEE2015

Interpolation for Synthesis on Unbounded Domains

Viktor Kuncak, Régis William Blanc

Synthesis procedures compile relational specifications into functions. In addition to bounded domains, synthesis procedures are applicable to domains such as mathematical integers, where the domain and range of relations and synthesized code is unbounded. ...

Ieee2013

Qualitative Spatial and Temporal Reasoning with Answer Set Programming

Jingshi Li

Representing and reasoning spatial and temporal information is a key research issue in Computer Science and Artificial Intelligence. In this paper, we introduce tools that produce three novel encodings which translate problems in qualitative spatial and te ...

2012