Sciweavers

FROCOS
2007
Springer
13 years 10 months ago
Idempotent Transductions for Modal Logics
Abstract. We investigate the extension of modal logics by bisimulation quantifiers and present a class of modal logics which is decidable when augmented with bisimulation quanti...
Tim French
ATVA
2007
Springer
101views Hardware» more  ATVA 2007»
13 years 10 months ago
A Generic Constructive Solution for Concurrent Games with Expressive Constraints on Strategies
Abstract. The emerging technology of interacting systems calls for new forto ensure their reliability. Concurrent games are paradigmatic abstract models for which several logics ha...
Sophie Pinchinat
TABLEAUX
2009
Springer
13 years 11 months ago
Tableaux and Model Checking for Memory Logics
Memory logics are modal logics whose semantics is specified in terms of relational models enriched with additional data structure to represent memory. The logical language is then...
Carlos Areces, Diego Figueira, Daniel Gorín...
LFCS
2009
Springer
13 years 11 months ago
Hypersequent Systems for the Admissible Rules of Modal and Intermediate Logics
The admissible rules of a logic are those rules under which the set of theorems of the logic is closed. In a previous paper by the authors, formal systems for deriving the admissib...
Rosalie Iemhoff, George Metcalfe
FSEN
2009
Springer
13 years 11 months ago
Program Logics for Sequential Higher-Order Control
We introduce a Hoare logic for higher-order functional languages with control operators such as callcc. The key idea is to build the assertion language and proof rules around an e...
Martin Berger
WOLLIC
2009
Springer
13 years 11 months ago
Classic-Like Analytic Tableaux for Finite-Valued Logics
The paper provides a recipe for adequately representing a very inclusive class of finite-valued logics by way of tableaux. The only requisite for applying the method is that the o...
Carlos Caleiro, João Marcos
LICS
2009
IEEE
13 years 11 months ago
Logics with Rank Operators
—We introduce extensions of first-order logic (FO) and fixed-point logic (FP) with operators that compute the rank of a definable matrix. These operators are generalizations o...
Anuj Dawar, Martin Grohe, Bjarki Holm, Bastian Lau...
TIME
2009
IEEE
13 years 11 months ago
Axiomatizations for Temporal Epistemic Logic with Perfect Recall over Linear Time
—This paper presents various semantic interpretations for logics of knowledge and time with prefect recall. We allow both past and future operators and examine the interpretation...
Szabolcs Mikulás, Mark Reynolds, Tim French
TACAS
2010
Springer
160views Algorithms» more  TACAS 2010»
13 years 11 months ago
Optimal Tableau Algorithms for Coalgebraic Logics
Deciding whether a modal formula is satisfiable with respect to a given set of (global) assumptions is a question of fundamental importance in applications of logic in computer sc...
Rajeev Goré, Clemens Kupke, Dirk Pattinson