Sciweavers

LICS
2008
IEEE
13 years 11 months ago
A Logical Characterization of Individual-Based Models
Individual-based models are a relatively new approach to modelling dynamical systems of interacting entities, for example molecules in a biological cell. Although they are computa...
James F. Lynch
LICS
2008
IEEE
13 years 11 months ago
The Quest for a Logic Capturing PTIME
The question of whether there is a logic that captures polynomial time is the central open problem in descriptive complexity theory. In my talk, I will review the question and the...
Martin Grohe
LICS
2008
IEEE
13 years 11 months ago
Piecewise Testable Tree Languages
— This paper presents a decidable characterization of tree languages that can be defined by a boolean combination of Σ1 formulas. This is a tree extension of the Simon theorem,...
Mikolaj Bojanczyk, Luc Segoufin, Howard Straubing
LICS
2008
IEEE
13 years 11 months ago
Focusing on Binding and Computation
Variable binding is a prevalent feature of the syntax and proof theory of many logical systems. In this paper, we define a programming language that provides intrinsic support fo...
Daniel R. Licata, Noam Zeilberger, Robert Harper
LICS
2008
IEEE
13 years 11 months ago
On the Computational Complexity of Cut-Reduction
Using appropriate notation systems for proofs, cutreduction can often be rendered feasible on these notations. Explicit bounds can be given. Developing a suitable notation system ...
Klaus Aehlig, Arnold Beckmann
LICS
2008
IEEE
13 years 11 months ago
On the Asymptotic Nullstellensatz and Polynomial Calculus Proof Complexity
We show that the asymptotic complexity of uniformly generated (expressible in First-Order (FO) logic) propositional tautologies for the Nullstellensatz proof system (NS) as well a...
Søren Riis
LICS
2008
IEEE
13 years 11 months ago
Nonlocal Flow of Control and Kleene Algebra with Tests
Kleene algebra with tests (KAT) is an equational system for program verification that combines Kleene algebra (KA), or the algebra of regular expressions, with Boolean algebra. I...
Dexter Kozen
LICS
2008
IEEE
13 years 11 months ago
A Neutral Approach to Proof and Refutation in MALL
We propose a setting in which the search for a proof of B or a refutation of B (a proof of ¬B) can be carried out simultaneously: this is in contrast to the usual approach in aut...
Olivier Delande, Dale Miller
LICS
2008
IEEE
13 years 11 months ago
From Automatic Structures to Borel Structures
We study the classes of B¨uchi and Rabin automatic structures. For B¨uchi (Rabin) automatic structures their domains consist of infinite strings (trees), and the basic relation...
Greg Hjorth, Bakhadyr Khoussainov, Antonio Montalb...