LPAR
2010
Springer
13 years 10 months ago
2010
Springer
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...
LPAR
2010
Springer
13 years 10 months ago
2010
Springer
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 ...
LPAR
2010
Springer
13 years 10 months ago
2010
Springer
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...
LPAR
2010
Springer
13 years 10 months ago
2010
Springer
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...
LPAR
2010
Springer
13 years 10 months ago
2010
Springer
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...
LPAR
2010
Springer
13 years 10 months ago
2010
Springer
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...
LPAR
2010
Springer
13 years 10 months ago
2010
Springer
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...
LPAR
2010
Springer
13 years 10 months ago
2010
Springer
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...
LPAR
2010
Springer
13 years 10 months ago
2010
Springer
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 ...
LPAR
2010
Springer
13 years 10 months ago
2010
Springer
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...