enter search term and/or author name
The article investigates the power of the dynamic complexity classes D
Permissive-nominal logic: First-order logic over nominal terms and sets
Gilles Dowek, Murdoch J. Gabbay
Article No.: 20
Permissive-Nominal Logic (PNL) is an extension of first-order predicate logic in which term-formers can bind names in their arguments.
This allows for direct axiomatizations with binders, such as of the λ-binder of the...
Most of the research on temporalized Description Logics (DLs) has concentrated on the case where temporal operators can be applied to concepts, and sometimes additionally to TBox axioms and ABox assertions. The aim of this article is to study...
Calculus of cooperation and game-based reasoning about protocol privacy
Sara Miner More, Pavel Naumov
Article No.: 22
The article introduces a new formal system, the calculus of cooperation, for reasoning about coalitions of players in a certain class of games. The calculus is an extension of the propositional intuitionistic logic that adds a coalition parameter...
Deductive inference for the interiors and exteriors of horn theories
Kazuhisa Makino, Hirotaka Ono
Article No.: 23
In this article, we investigate deductive inference for interiors and exteriors of Horn knowledge bases, where interiors and exteriors were introduced by Makino and Ibaraki  to study stability properties of knowledge bases. We present a...
Arithmetic complexity via effective names for random sequences
Bjørn Kjos-Hanssen, Frank Stephan, Jason Teutsch
Article No.: 24
We investigate enumerability properties for classes of sets which permit recursive, lexicographically increasing approximations, or left-r.e. sets. In addition to pinpointing the complexity of left-r.e. Martin-Löf, computably, Schnorr,...
In modal logics, graded (world) modalities have been deeply investigated as a useful framework for generalizing standard existential and universal modalities in such a way that they can express statements about a given number of immediately...
Well-structured program equivalence is highly undecidable
Robert Goldblatt, Marcel Jackson
Article No.: 26
We show that strict deterministic propositional dynamic logic with intersection is highly undecidable, solving a problem in the Stanford Encyclopedia of Philosophy. In fact we show something quite a bit stronger. We introduce the construction of...
For programs whose data variables range over Boolean or finite domains, program verification is decidable, and this forms the basis of recent tools for software model checking. In this article, we consider algorithmic verification of programs that...