Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Concept

Classical logic

Related publications (17)

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

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

Exact Synthesis of Boolean Functions in Majority-of-five Forms

Giovanni De Micheli, Mathias Soeken, Winston Jason Haaswijk

Recent studies show that majority-based logic synthesis is beneficial for both traditional and nanotechnology digital designs. However, most of the existing synthesis algorithms for majority logic generate majority-of-three (M-3) networks. The optimization ...

IEEE2019

Inverter Propagation and Fan-Out Constraints for Beyond-CMOS Majority-Based Technologies

Giovanni De Micheli, Mathias Soeken, Eleonora Testa

Traditional logic synthesis faces challenges of meeting the requirements demanded by the many emerging nanotech-nologies that are based on logic models different from standard CMOS. Several emerging nanodevices including Quantum-dot Cellular Automata (QCA) ...

IEEE2017

Notes on Majority Boolean Algebra

Giovanni De Micheli, Pierre-Emmanuel Julien Marc Gaillardon, Mathias Soeken, Luca Gaetano Amarù

A Majority-Inverter Graph (MIG) is a homogeneous logic network, where each node represents the majority function. Recently, a logic optimization package based on the MIG data-structure, with 3-input majority node (M3) has been proposed [2], [30]. It is dem ...

IEEE2016

A Sound and Complete Axiomatization of Majority-n Logic

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

Manipulating logic functions via majority operators recently drew the attention of researchers in computer science. For example, circuit optimization based on majority operators enables superior results as compared to traditional logic systems. Also, the B ...

Institute of Electrical and Electronics Engineers2016

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

Enhanced Quantification for 3D Energy Dispersive Spectrometry: Going Beyond the Limitation of Large Volume of X-Ray Emission

Cécile Hébert, Marco Cantoni, Pierre Burdet

This paper presents a method developed to quantify three-dimensional energy dispersive spectrometry (3D EDS) data with voxel size smaller than the volume from which X-rays are emitted. The influence of the neighboring voxels is corrected by applying recurs ...

Cambridge University Press2014

Majority Logic Representation and Satisfiability

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

Majority logic is a powerful generalization of common AND/OR logic. Original two-level and multi-level logic networks can use majority operators as primitive connective, in place of AND/ORs. In such a way, Boolean functions have novel means for compact rep ...

2014

MIXSyn: An Efficient Logic Synthesis Methodology for Mixed XOR-AND/OR Dominated Circuits

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

We present a new logic synthesis methodology, called MIXSyn, that produces area-efficient results for mixed XOR-AND/OR dominated logic functions. MIXSyn is a two step synthesis process. The first step is a hybrid logic optimization that enables selective a ...

2013

BDS-MAJ: A BDD-based Logic Synthesis Tool Exploiting Majority Logic Decomposition

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

Despite the impressive advance of logic synthesis during the past decades, a general methodology capable of efficiently synthesizing both control and datapath logic is still missing. Indeed, while synthe- sis techniques for random control logic (AND/OR-int ...

2013

Asymptotic Inference For Partially Observed Branching Processes

Victor Panaretos, Andrea Kraus

We consider the problem of estimation in a partially observed discrete-time Galton-Watson branching process, focusing on the first two moments of the offspring distribution. Our study is motivated by modelling the counts of new cases at the onset of a stoc ...

Applied Probability Trust2011

Ordered Sets in the Calculus of Data Structures

Viktor Kuncak, Philippe Paul Henri Suter, Ruzica Piskac

Our goal is to identify families of relations that are useful for reasoning about software. We describe such families using decidable quantifier-free classes of logical constraints with a rich set of operations. A key challenge is to define such classes of ...

Springer2010

Full Functional Verification of Linked Data Structures

Viktor Kuncak

We present the first verification of full functional correctness for a range of linked data structure implementations, including mutable lists, trees, graphs, and hash tables. Specifically, we present the use of the Jahob verification system to verify form ...

2008

Efficient static analysis of XML paths and types

We present an algorithm to solve XPath decision problems under regular tree type constraints and show its use to statically type-check XPath queries. To this end, we prove the decidability of a logic with converse for finite ordered trees whose time comple ...

2007