LPAR
2010
Springer
13 years 8 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 8 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 8 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 8 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 8 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 8 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 8 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 8 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 8 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 8 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...