A Sound and Complete Axiomatization of Majority-n Logic

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

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

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

Electronic devices play an irreplaceable role in our lives. With the tightening time to market, exploding demand for computing power, and continuous desire for smaller, faster, less energy-consuming, and lower-cost chips, computer-aided design for electron ...

Logic rewriting is a powerful optimization technique that replaces small sections of a Boolean network with better implementations. Typically, exact synthesis is used to compute optimum replacement on-the-fly, with possible support for Boolean don't cares. ...

Rapid single-flux quantum (RSFQ) is one of the most advanced and promising superconducting logic families, offering exceptional energy efficiency and speed. RSFQ technology requires delay registers (DFFs) and splitter cells to satisfy the path-balancing an ...

Factored form is a powerful multi-level representation of a Boolean function that readily translates into an implementation of the function in CMOS technology. In particular, the number of literals in a factored form correlates strongly with the number of ...

This article explores how the logic underlying modal practices tends to modulate the population’s responsiveness to improvements in global transport supply. Based on a quantitative survey conducted in 2018–2019 among the working population of the cantons o ...

State-of-the-art sensors for measuring FPGA voltage fluctuations are time-to-digital converters (TDCs). They allow detecting voltage fluctuations in the order of a few nanoseconds. The key building component of a TDC is a delay line, typically implemented ...

With Moore's law coming to an end, increasingly more hope is being put in specialized hardware implemented on reconfigurable architectures such as Field-Programmable Gate Arrays (FPGAs). Yet, it is often neglected that these architectures themselves experi ...

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

In this paper, we consider the first eigenvalue.1(O) of the Grushin operator.G :=.x1 + |x1|2s.x2 with Dirichlet boundary conditions on a bounded domain O of Rd = R d1+ d2. We prove that.1(O) admits a unique minimizer in the class of domains with prescribed ...

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

We give a new characterization of the Sherali-Adams proof system, showing that there is a degree-d Sherali-Adams refutation of an unsatisfiable CNF formula C if and only if there is an ε > 0 and a degree-d conical junta J such that viol_C(x) - ε = J, where ...

Individual transistors based on emerging reconfigurable nanotechnologies exhibit electrical conduction for both types of charge carriers. These transistors (referred to as Reconfigurable Field-Effect Transistors (RFETs)) enable dynamic reconfiguration to d ...

Approximate logic synthesis is an emerging field that tolerates errors in the synthesized logic circuits for better optimization quality. Indeed, in many computing problems, the requirement of preserving the exact functionality either results in unnecessar ...

Submodular functions are a widely studied topic in theoretical computer science. They have found several applications both theoretical and practical in the fields of economics, combinatorial optimization and machine learning. More recently, there have also ...

We address for the first time the problem of correcting group discriminations within a score function, while minimizing the individual error. Each group is described by a probability density function on the set of profiles. We first solve the problem analy ...

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

Unstructured neural network pruning algorithms have achieved impressive compression ratios. However, the resulting-typically irregular-sparse matrices hamper efficient hardware implementations, leading to additional memory usage and complex control logic t ...

Most logic synthesis algorithms work on graph representations of logic functions with nodes associated with arbitrary logic expressions or simple logic functions and iteratively optimize such graphs. While recent multilevel logic synthesis efforts focused ...

A Sound and Complete Axiomatization of Majority-n Logic

Chattez avec Graph Search

Orthologic with Axioms

Interpolation and Quantifiers in Ortholattices

Contemporary Logic Synthesis: with an Application to AQFP Circuit Optimization

Scalable Logic Rewriting Using Don’t Cares

Algebraic and Boolean Methods for SFQ Superconducting Circuits

Improving Standard-Cell Design Flow using Factored Form Optimization

Analysing the potential for modal shiftbased on the logic of modal choice

RDS: FPGA Routing Delay Sensors for Effective Remote Power Analysis Attacks

Automating the Design of Programmable Interconnect for Reconfigurable Architectures

LISA – A Modern Proof System

The first Grushin eigenvalue on cartesian product domains

NP Satisfiability for Arrays as Powers

On Semi-Algebraic Proofs and Algorithms

Utilizing XMG-based Synthesis to Preserve Self-Duality for RFET-Based Circuits

Logic Synthesis From Incomplete Specifications Using Disjoint Support Decomposition

Streaming and Matching Problems with Submodular Functions

Removing Algorithmic Discrimination (With Minimal Individual Error)

Formula Normalizations in Verification

Dynamic Probabilistic Pruning: A General Framework for Hardware-Constrained Pruning at Different Granularities

Three-Input Gates for Logic Synthesis