Sciweavers

LICS
2012
IEEE
12 years 2 months ago
Graph Logics with Rational Relations and the Generalized Intersection Problem
Abstract—We investigate some basic questions about the interaction of regular and rational relations on words. The primary motivation comes from the study of logics for querying ...
Pablo Barceló, Diego Figueira, Leonid Libki...
LICS
2012
IEEE
12 years 2 months ago
The Complete Proof Theory of Hybrid Systems
—Hybrid systems are a fusion of continuous dynamical systems and discrete dynamical systems. They freely combine dynamical features from both worlds. For that reason, it has ofte...
André Platzer
LICS
2012
IEEE
12 years 2 months ago
The Winning Ways of Concurrent Games
Abstract—A bicategory of concurrent games, where nondeterministic strategies are formalized as certain maps of event structures, was introduced recently. This paper studies an ex...
Pierre Clairambault, Julian Gutierrez, Glynn Winsk...
LICS
2012
IEEE
12 years 2 months ago
Near Unanimity Constraints Have Bounded Pathwidth Duality
—We show that if a finite relational structure has a near unanimity polymorphism, then the constraint satisfaction problem with that structure as its fixed template has bounded...
Libor Barto, Marcin Kozik, Ross Willard
LICS
2012
IEEE
12 years 2 months ago
Logics of Dynamical Systems
—We study the logic of dynamical systems, that is, logics and proof principles for properties of dynamical systems. Dynamical systems are mathematical models describing how the s...
André Platzer
LICS
2012
IEEE
12 years 2 months ago
Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
—Interactive theorem provers based on higher-order logic (HOL) traditionally follow the definitional approach, reducing high-level specifications to logical primitives. This al...
Dmitriy Traytel, Andrei Popescu, Jasmin Christian ...
LICS
2012
IEEE
12 years 2 months ago
The Ordinal-Recursive Complexity of Timed-arc Petri Nets, Data Nets, and Other Enriched Nets
—We show how to reliably compute fast-growing functions with timed-arc Petri nets and data nets. This construction provides ordinal-recursive lower bounds on the complexity of th...
Serge Haddad, Sylvain Schmitz, Philippe Schnoebele...
LICS
2012
IEEE
12 years 2 months ago
An Automata Model for Trees with Ordered Data Values
—Data trees are trees in which each node, besides carrying a label from a finite alphabet, also carries a data value infinite domain. They have been used as an abstraction mode...
Tony Tan
LICS
2012
IEEE
12 years 2 months ago
Countermodels from Sequent Calculi in Multi-Modal Logics
—A novel countermodel-producing decision procedure that applies to several multi-modal logics, both intuitionistic and classical, is presented. Based on backwards search in label...
Deepak Garg, Valerio Genovese, Sara Negri
LICS
2012
IEEE
12 years 2 months ago
Step Indexed Realizability Semantics for a Call-by-Value Language Based on Basic Combinatorial Objects
—We propose a mathematical framework for step indexed realizability semantics of a call-by-value polymorphic lambda calculus with recursion, existential types and recursive types...
Naohiko Hoshino