Concept

Hilbert system

Related publications (14)

Graph Chatbot

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

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

2024

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

2023

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

Never Say Never Probabilistic & Temporal Failure Detectors (Extended)

Rachid Guerraoui, David Kozhaya, Yvonne Anne Pignolet-Oswald

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

IPDPS2016

Never Say Never Probabilistic & Temporal Failure Detectors

Rachid Guerraoui, David Kozhaya

Ieee2016

L-2-cohomology and complete Hamiltonian manifolds

Tudor Ratiu

A classical theorem of Frankel for compact Kahler manifolds states that a Kahler S-1-action is Hamiltonian if and only if it has fixed points. We prove a metatheorem which says that when the Hodge theory holds on non-compact manifolds, Frankel's theorem st ...

Elsevier2015

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

Methods for Designing Reliable Probe Arrays

Giovanni De Micheli, Luca Benini, Abhishek Garg

Recent advances in biosensing technologies have led to applications of biosensor probe arrays for rapid identification of biological agents such as drugs, gene expressions, proteins, cholesterol and fats in an input sample. However, monitoring the simultan ...

IEEE2010

Lukasiewicz fuzzy logic networks and their ultra low power hardware implementation

Rafal Tomasz Dlugosz

In this paper, we propose a new category of current-mode Łukasiewicz OR and AND logic neurons and ensuing logic networks along with their ultra-low power realization. The introduced circuits can operate in a wide range of the input signals varying in-betwe ...

Elsevier2010

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