Concept

Système axiomatique

Publications associées (16)

Orthologic with Axioms

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

LISA – A Modern Proof System

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

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

Dagstuhl, Germany, Schloss Dagstuhl - Leibniz-Zentrum fur Informatik2023

A Toolbox for Barriers on Interactive Oracle Proofs

Alessandro Chiesa

Interactive oracle proofs (IOPs) are a proof system model that combines features of interactive proofs (IPs) and probabilistically checkable proofs (PCPs). IOPs have prominent applications in complexity theory and cryptography, most notably to constructing ...

SPRINGER INTERNATIONAL PUBLISHING AG2022

Minimum Cost Intervention Design for Causal Effect Identification

Negar Kiyavash, Sina Akbari, Seyed Jalal Etesami

Pearl's do calculus is a complete axiomatic approach to learn the identifiable causal effects from observational data. When such an effect is not identifiable, it is necessary to perform a collection of often costly interventions in the system to learn the ...

PMLR2022

Wigner Measures and Coherent Quantum Control

Tudor Ratiu

We introduce Wigner measures for infinite-dimensional open quantum systems; important examples of such systems are encountered in quantum control theory. In addition, we propose an axiomatic definition of coherent quantum feedback. ...

2021

Axiomatic scale theory

Martin Alois Rohrmeier, Daniel Harasim

Scales are a fundamental concept of musical practice around the world. They commonly exhibit symmetry properties that are formally studied using cyclic groups in the field of mathematical scale theory. This paper proposes an axiomatic framework for mathema ...

TAYLOR & FRANCIS LTD2020

An Operational Approach to Information Leakage

Ibrahim Issa

Given two random variables X and Y , an operational approach is undertaken to quantify the "leakage" of information from X to Y . The resulting measure L (X -> Y) is called maximal leakage, and is defined as the multiplicative increase, upon observing Y , ...

IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC2020

Structural Rewriting in XOR-Majority Graphs

Giovanni De Micheli, Mathias Soeken, Zhufei Chu

In this paper, we present a structural rewriting method for a recently proposed XOR-Majority graph (XMG), which has exclusive-OR (XOR), majority-of-three (MAJ), and inverters as primitives. XMGs are an extension of Majority-Inverter Graphs (MIGs). Previous ...

ASSOC COMPUTING MACHINERY2019

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

A Formally Verified NAT

George Candea, Solal Vincenzo Pirelli, Aikaterini Argyraki, Arseniy Zaostrovnykh, Luis David Figueiredo Mascarenhas Moreira Pedrosa

We present a Network Address Translator (NAT) written in C and proven to be semantically correct according to RFC 3022, as well as crash-free and memory-safe. There exists a lot of recent work on network verification, but it mostly assumes models of networ ...

Assoc Computing Machinery2017

Analytic twists of modular forms and applications

Alexandre François Peyrot

We are interested in the study of non-correlation of Fourier coefficients of Maass forms against a wide class of real analytic functions. In particular, the class of functions we are interested in should be thought of as some archimedean analogs of Frobeni ...

EPFL2017

Never Say Never Probabilistic & Temporal Failure Detectors

Rachid Guerraoui, David Kozhaya

The failure detector approach for solving distributed computing problems has been celebrated for its modularity. This approach allows the construction of algorithms using abstract failure detection mechanisms, defined by axiomatic properties, as building b ...

Ieee2016

Majority-Inverter Graph: A New Paradigm for Logic Optimization

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

In this paper, we propose a paradigm shift in representing and optimizing logic by using only majority (MAJ) and inversion (INV) functions as basic operations. We represent logic functions by Majority-Inverter Graph (MIG): a directed acyclic graph c ...

Ieee-Inst Electrical Electronics Engineers Inc2016

A Sound and Complete Axiomatization of Majority-n Logic

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

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

Majority-Inverter Graph: A Novel Data-Structure and Algorithms for Efficient Logic Optimization

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

In this paper, we present Majority-Inverter Graph (MIG), a novel logic representation structure for efficient optimization of Boolean functions. An MIG is a directed acyclic graph consisting of three-input majority nodes and regular/complemented e ...

2014

Regularity in metric spaces

Serguei Timochine

Using arguments developed by De Giorgi in the 1950's, it is possible to prove the regularity of the solutions to a vast class of variational problems in the Euclidean space. The main goal of the present thesis is to extend these results to the more abstrac ...

EPFL2006