Concept

True quantified Boolean formula

Related publications (39)

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.

Satisfiability Modulo Recursive Programs

Viktor Kuncak, Philippe Paul Henri Suter, Ali Sinan Köksal

We present a semi-decision procedure for checking satisfiability of expressive correctness properties of recursive first-order functional programs. In our approach, both properties and programs are expressed in the same language, a subset of Scala. We impl ...

Springer-Verlag Berlin2011

Fast Randomized Test-and-Set and Renaming

Rachid Guerraoui, Seth Gilbert, Dan Alistarh, Hagit Albo Attiya, Andrei Giurgiu

Most people believe that renaming is easy: simply choose a name \emph{at random}; if more than one process selects the same name, then try again. We highlight the issues that occur when trying to implement such a scheme and shed new light on the read-write ...

2010

Fast Randomized Test-and-Set and Renaming

Rachid Guerraoui, Seth Gilbert, Dan Alistarh, Hagit Albo Attiya, Andrei Giurgiu

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

On Combining Theories with Shared Set Operations

Viktor Kuncak, Ruzica Piskac

We explore the problem of automated reasoning about the non-disjoint combination of theories that share set variables and operations. We prove a combination theorem and apply it to show the decidability of the satisfiability problem for a class of formulas ...

2009

Modeling stochasticity and robustness in gene regulatory networks

Giovanni De Micheli, Abhishek Garg, Ioannis Xenarios

Motivation: Understanding gene regulation in biological processes and modeling the robustness of underlying regulatory networks is an important problem that is currently being addressed by computational systems biologists. Lately, there has been a renewed ...

2009

Non-Clausal Satisfiability Modulo Theories

Philippe Paul Henri Suter

This thesis presents NC(T), an extension of the DPLL(T) scheme [16, 29] for decision procedures for quantifier-free first-order logics. In DPLL(T), a general Boolean DPLL engine is instantiated with a theory solver for the theory T. The DPLL engine is resp ...

2008

Information Visualization of Multi-dimensional Cellular Automata using GPU Programming

Stéphane Gobron

We propose a method for generating all possible rules of multidimension Boolean cellular automata (CA). Based on an original encoding method and the programming of graphical processor units (GPU), this method allows us to visualize the CA information flow ...

IEEE Computer Society2007

EP theorems and linear complementary problems

Let A be a rational n × n square matrix and b be a rational n-vector for some positive integer n. The linear complementarity problem (abbreviated by LCP) is to find a vector (x, y) in R^(2n) satisfying y = Ax + b (x, y) >= 0 and the complementarity conditi ...

1998

A Boolean Approach to Construct Neural Networks for Non-Boolean Problems

A neural network construction method for problems specified for data sets with in- and/or output values in the continuous or discrete domain is described and evaluated. This approach is based on a Boolean approximation of the data set and is generic for va ...

1996