Concept

Method of analytic tableaux

Related publications (32)

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.

Exploiting Satisfiability Solvers for Efficient Logic Synthesis

Ana Petkovska

Logic synthesis is an important part of electronic design automation (EDA) flows, which enable the implementation of digital systems. As the design size and complexity increase, the data structures and algorithms for logic synthesis must adapt and improve ...

EPFL2017

Procedures for first-order logic with equality are used in many modern theorem provers and solvers, yet procedure termination in case of interesting sub-classes of satisfiable formulas remains a challenging problem. We present an instantiation-based semi-d ...

2016

Long-Term Time-Sensitive Costs for CRF-Based Tracking by Detection

Jean-Marc Odobez, Alexandre Heili

We present a Conditional Random Field (CRF) approach to tracking-by-detection in which we model pairwise factors linking pairs of detections and their hidden labels, as well as higher order potentials defined in terms of label costs. Our method considers l ...

Springer Int Publishing Ag2016

Counterexample-Guided Quantifier Instantiation for Synthesis in SMT, Computer Aided Verification

Viktor Kuncak, Andrew Joseph Reynolds

We introduce the first program synthesis engine implemented inside an SMT solver. We present an approach that extracts solution functions from unsatisfiability proofs of the negated form of synthesis conjectures. We also discuss novel counterexample-guided ...

2015

We prove that the quantifier-free fragment of the theory of character strings with regular language membership constraints and linear integer constraints over string lengths is decidable. We do that by describing a sound, complete and terminating tableaux ...

Springer-Verlag Berlin2015

, , ,

In this paper, we establish a non-trivial duality between tautology and contradiction check to speed up circuit SAT. Tautology check determines if a logic circuit is true in every possible interpretation. Analogously, contradiction check dete ...

IEEE2015

Exploiting Long-Term Connectivity and Visual Motion in CRF-based Multi-Person Tracking

Jean-Marc Odobez, Alexandre Heili

We present a conditional random field approach to tracking-by-detection in which we model pairwise factors linking pairs of detections and their hidden labels, as well as higher order potentials defined in terms of label costs. To the contrary of previous ...

2014

, ,

A scalable programming language is one in which the same concepts can describe small as well as large parts. Towards this goal, Scala unifies concepts from object and module systems. An essential ingredient of this unification is the concept of objects wit ...

Assoc Computing Machinery2014

Detection of Local Wall Stiffness Drop in Steel-Lined Pressure Tunnels and Shafts of Hydroelectric Power Plants Using Steep Pressure Wave Excitation and Wavelet Decomposition

Anton Schleiss, Fadi Hachem

A new monitoring approach for detecting, locating, and quantifying structurally weak reaches of steel-lined pressure tunnels and shafts is presented. These reaches arise from local deterioration of the backfill concrete and the rock mass surrounding the li ...

2012

To support verification of expressive properties of functional programs, we consider algebraic style specifications that may relate multiple user-defined functions, and compare multiple invocations of a function for different arguments. We present decision ...

Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa2011