Sciweavers

CSL
2010
Springer
13 years 5 months ago
New Algorithm for Weak Monadic Second-Order Logic on Inductive Structures
We present a new algorithm for model-checking weak monadic second-order logic on inductive structures, a class of structures of bounded clique width. Our algorithm directly manipul...
Tobias Ganzow, Lukasz Kaiser
CSL
2010
Springer
13 years 5 months ago
Quantified Differential Dynamic Logic for Distributed Hybrid Systems
Abstract. We address a fundamental mismatch between the combinations of dynamics that occur in complex physical systems and the limited kinds of dynamics supported in analysis. Mod...
André Platzer
CSL
2010
Springer
13 years 5 months ago
A Sequent Calculus with Implicit Term Representation
We investigate a modification of the sequent calculus which s a first-order proof into its abstract deductive structure and a unifier which renders this structure a valid proof. We...
Stefan Hetzl
CSL
2010
Springer
13 years 5 months ago
On the Computability of Region-Based Euclidean Logics
By a Euclidean logic, we understand a formal language whose variables range over subsets of Euclidean space, of some fixed dimension, and whose non-logical primitives have fixed me...
Yavor Nenov, Ian Pratt-Hartmann
CSL
2010
Springer
13 years 5 months ago
Energy and Mean-Payoff Games with Imperfect Information
We consider two-player games with imperfect information and quantitative objective. The game is played on a weighted graph with a state space partitioned into classes of indistingu...
Aldric Degorre, Laurent Doyen, Raffaella Gentilini...
CSL
2010
Springer
13 years 5 months ago
On Slicewise Monotone Parameterized Problems and Optimal Proof Systems for TAUT
Abstract. For a reasonable sound and complete proof calculus for firstorder logic consider the problem to decide, given a sentence of firstorder logic and a natural number n, whet...
Yijia Chen, Jörg Flum
CSL
2010
Springer
13 years 5 months ago
Efficient Enumeration for Conjunctive Queries over X-underbar Structures
Guillaume Bagan, Arnaud Durand, Emmanuel Filiot, O...
CSL
2010
Springer
13 years 5 months ago
Coq Modulo Theory
Pierre-Yves Strub
CSL
2010
Springer
13 years 5 months ago
Fibrational Induction Rules for Initial Algebras
This paper provides an induction rule that can be used to prove properties of data structures whose types are inductive, i.e., are carriers of initial algebras of functors. Our res...
Neil Ghani, Patricia Johann, Clément Fumex
CSL
2010
Springer
13 years 5 months ago
Ordered Sets in the Calculus of Data Structures
Our goal is to identify families of relations that are useful for reasoning about software. We describe such families using decidable quantifier-free classes of logical constraints...
Viktor Kuncak, Ruzica Piskac, Philippe Suter