Sciweavers

LPAR
2010
Springer
13 years 9 months ago
Counting and Enumeration Problems with Bounded Treewidth
By Courcelle's Theorem we know that any property of finite structures definable in monadic second-order logic (MSO) becomes tractable over structures with bounded treewidth. T...
Reinhard Pichler, Stefan Rümmele, Stefan Wolt...
LPAR
2010
Springer
13 years 9 months ago
Semiring-Induced Propositional Logic: Definition and Basic Algorithms
In this paper we introduce an extension of propositional logic that allows clauses to be weighted with values from a generic semiring. The main interest of this extension is that ...
Javier Larrosa, Albert Oliveras, Enric Rodrí...
LPAR
2010
Springer
13 years 9 months ago
Hardness of Preorder Checking for Basic Formalisms
We investigate the complexity of preorder checking when the specification is a flat finite-state system whereas the implementation is either a non-flat finite-state system or a st...
Laura Bozzelli, Axel Legay, Sophie Pinchinat
LPAR
2010
Springer
13 years 9 months ago
Speed-Up Techniques for Negation in Grounding
Abstract. Grounding is the task of reducing a first order formula to ground formula that is equivalent on a given universe, and is important in many kinds of problem solving and re...
Amir Aavani, Shahab Tasharrofi, Gulay Ünel, E...
LPAR
2010
Springer
13 years 9 months ago
Synthesis of Trigger Properties
In automated synthesis, we transform a specification into a system that is guaranteed to satisfy the specification. In spite of the rich theory developed for temporal synthesis, l...
Orna Kupferman, Moshe Y. Vardi
LPAR
2010
Springer
13 years 9 months ago
Disunification for Ultimately Periodic Interpretations
Abstract. Disunification is an extension of unification to first-order formulae over syntactic equality atoms. Instead of considering only syntactic equality, I extend a disunifica...
Matthias Horbach
LPAR
2010
Springer
13 years 9 months ago
Qex: Symbolic SQL Query Explorer
We describe a technique and a tool called Qex for generating input tables and parameter values for a given parameterized SQL query. The evaluation semantics of an SQL query is tra...
Margus Veanes, Nikolai Tillmann, Jonathan de Halle...
LPAR
2010
Springer
13 years 9 months ago
Satisfiability of Non-linear (Ir)rational Arithmetic
Abstract. We present a novel way for reasoning about (possibly ir)rational quantifier-free non-linear arithmetic by a reduction to SAT/SMT. The approach is incomplete and dedicated...
Harald Zankl, Aart Middeldorp
LPAR
2010
Springer
13 years 9 months ago
On the Satisfiability of Two-Variable Logic over Data Words
Data trees and data words have been studied extensively in connection with XML reasoning. These are trees or words that, in addition to labels from a finite alphabet, carry labels ...
Claire David, Leonid Libkin, Tony Tan
LPAR
2010
Springer
13 years 9 months ago
Infinite Families of Finite String Rewriting Systems and Their Confluence
We introduce parameterized rewrite systems for describing infinite families of finite string rewrite systems depending upon non-negative integer parameters, as well as ways to reas...
Jean-Pierre Jouannaud, Benjamin Monate