Journal of Logic Language and Information

  Tarski avoids the liar paradox by relativizing truth and falsehood to particular languages and forbidding the predication
 to sentences in a language of truth or falsehood by any sentences belonging to the same language. The Tarski truth-schemata
 stratify an object-language and indefinitely ascending hierarchy of meta-languages in which the truth or falsehood of sentences
 in a language can only be asserted or denied in a higher-order meta-language. However, Tarski's statement of the truth-schemata
 themselves involve general truth functions, and in particular the biconditional, defined in terms of truth conditions involving
 truth values standardly displayed in a truth table. Consistently with his semantic program, all such truth values should also
 be relativized to particular languages for Tarski. The objection thus points toward the more interesting problem of Tarski's
 concept of the exact status of truth predications in a general logic of sentential connectives. Tarski's three-part solution
 to the circularity objection which he anticipates is discussed and refuted in detail.
 
	

  We continue the work initiated in Herzig and Lorini (J Logic Lang Inform, in press) whose aim is to provide a minimalistic logical framework combining the expressiveness of dynamic logic in which actions are first-class citizens in the object language,
 with the expressiveness of logics of agency such as STIT and logics of group capabilities such as CL and ATL. We present a
 logic called 

DDLA
 (Deterministic Dynamic logic of Agency) which supports reasoning about actions and joint actions of agents and coalitions, and agentive and coalitional capabilities.
 In 

DDLA
 it is supposed that, once all agents have selected a joint action, the effect of this joint action is deterministic. In order
 to assess 

DDLA
 we prove that it embeds Coalition Logic. We then extend 

DDLA
 with modal operators for agents' preferences, and show that the resulting logic is sufficiently expressive to capture the
 game-theoretic concepts of best response and Nash equilibrium.
 
	

  The aim of this paper, is to provide a logical framework for reasoning about actions, agency, and powers of agents and coalitions
 in game-like multi-agent systems. First we define our basic Dynamic Logic of Agency (

DLA
). Differently from other logics of individual and coalitional capability such as Alternating-time Temporal Logic (ATL) and
 Coalition Logic, in 

DLA
 cooperation modalities for expressing powers of agents and coalitions are not primitive, but are defined from more basic
 dynamic logic operators of action and (historic) necessity. We show that STIT logic can be reconstructed in 

DLA
. We then extend 

DLA
 with epistemic operators, which allows us to distinguish capability and power. We finally characterize the conditions under
 which agents are aware of their capabilities and powers.
 
	

  We conducted a computer-based psychological experiment in which a random mix of 40 tautologies and 40 non-tautologies were
 presented to the participants, who were asked to determine which ones of the formulas were tautologies. The participants were
 eight university students in computer science who had received tuition in propositional logic. The formulas appeared one by
 one, a time-limit of 45 s applied to each formula and no aids were allowed. For each formula we recorded the proportion of
 the participants who classified the formula correctly before timeout (accuracy) and the mean response time among those participants
 (latency). We propose a new proof formalism for modeling propositional reasoning with bounded cognitive resources. It models
 declarative memory, visual memory, working memory, and procedural memory according to the memory model of Atkinson and Shiffrin
 and reasoning processes according to the model of Newell and Simon. We also define two particular proof systems, T and NT, for showing propositional formulas to be tautologies and non-tautologies, respectively. The accuracy was found to be higher
 for non-tautologies than for tautologies (p < .0001). For tautologies the correlation between latency and minimum proof length in T was .89 and for non-tautologies the correlation between latency and minimum proof length in NT was .87.
 
	

  Probability logics have been an active topic of investigation of beliefs in type spaces in game theoretical economics. Beliefs
 are expressed as subjective probability measures. Savage's postulates in decision theory imply that subjective probability
 measures are not necessarily countably additive but finitely additive. In this paper, we formulate a probability logic Σ+ that is strongly complete with respect to this class of type spaces with finitely additive probability measures, i.e. a set
 of formulas is consistent in Σ+ iff it is satisfied in a finitely additive type space. Although we can characterize Σ+-theories satisfiable in the class as maximally consistent sets of formulas, we prove that any canonical model of maximally
 consistent sets is not universal in the class of type spaces with finitely additive measures, and, moreover, it is not a type
 space. At the end of this paper, we show that even a minimal use of probability indices causes the failure of compactness
 in probability logics.
 
	

  A first-order dynamic non-commutative logic (DN), which has no structural rules and has some program operators, is introduced
 as a Gentzen-type sequent calculus. Decidability, cut-elimination and completeness theorems are shown for DN or its fragments.
 DN is intended to represent not only program-based, resource-sensitive, ordered, sequence-based, but also hierarchical (tree-based)
 reasoning.
 
	

  We provide necessary and sufficient conditions determining how monotonicity of some classes of reducible quantifiers depends
 on the monotonicity of simpler quantifiers of iterations to which they are equivalent.
 
	

  One way of coping with agreement of features in French is to perform two parallel computations, one in the free pregroup of
 syntactic types, the other in that of feature types. Technically speaking, this amounts to working in the direct product of two free pregroups.
 
	

Volker Weber
	

  We introduce 

A
 -ranked preferential structures and combine them with an accessibility relation. 

A
 -ranked preferential structures are intermediate between simple preferential structures and ranked structures. The additional
 accessibility relation allows us to consider only parts of the overall 

A
 -ranked structure. This framework allows us to formalize contrary to duty obligations, and other pictures where we have a
 hierarchy of situations, and maybe not all are accessible to all possible worlds. Representation results are proved.
 
	

  While classical temporal logics lose track of a state as soon as a temporal operator is applied, several branching-time logics
 able to repeatedly refer to a state have been introduced in the literature. We study such logics by introducing a new formalism,
 hybrid branching-time logics, subsuming the other approaches and making the ability to refer to a state more explicit by assigning
 a name to it. We analyze the expressive power of hybrid branching-time logics and the complexity of their satisfiability problem.
 As main result, the satisfiability problem for the hybrid versions of several branching-time logics is proved to be 2EXPTIME-complete. To prove the upper bound, the automata-theoretic approach to branching-time logics is extended to hybrid logics.
 As a result of independent interest, the nonemptiness problem for alternating one-pebble Büchi tree automata is shown to be
 2EXPTIME-complete. A common property of the logics studied is that they refer to only one state. This restriction is crucial: The
 ability to refer to more than one state causes a nonelementary blow-up in complexity. In particular, we prove that satisfiability
 for NCTL* has nonelementary complexity.
 
	

  Large databases of linguistic annotations are used for testing linguistic hypotheses and for training language processing
 models. These linguistic annotations are often syntactic or prosodic in nature, and have a hierarchical structure. Query languages
 are used to select particular structures of interest, or to project out large slices of a corpus for external analysis. Existing
 languages suffer from a variety of problems in the areas of expressiveness, efficiency, and naturalness for linguistic query.
 We describe the domain of linguistic trees and discuss the expressive requirements for a query language. Then we present a
 language that can express a wide range of queries over these trees, and show that the language is first-order complete over
 trees.
 
	

  The purpose of this paper is to argue that the hybrid formalism fits naturally in the context of David Lewis's counterfactual
 logic and that its introduction into this framework is desirable. This hybridization enables us to regard the inference The
 pig is Mary; Mary is pregnant; therefore the pig is pregnant' as a process of updating local information (which depends on
 the given situation) by using global information (independent of the situation). Our hybridization also has the following
 technical advantages: (i) it preserves the completeness and decidability of Lewis's logic; (ii) it allows us to characterize
 the Limit Assumption as a proof-rule with some side-conditions; and (iii) it enables us to establish a general Kripke completeness
 result by using the proof-rule corresponding to the Limit Assumption.
 
	

  This paper sets forth a new theory of quantifiers and term connectives, called shadow theory, which should help simplify various semantic theories of natural language by greatly reducing the need of Montagovian proper
 names, type-shifting, and λ-conversion. According to shadow theory, conjunctive, disjunctive, and negative noun phrases such
 as John and Mary, John or Mary, and not both John and Mary, as well as determiner phrases such as every man, some woman, and the boys, are all of semantic type e and denote individual-like objects, called shadows' conjunctive, disjunctive, or negative shadows, such as John-and-Mary, John-or-Mary, and not-(John-and-Mary). There is no essential difference between quantification
 and denotation: quantification is nothing but denotation of shadows. Individuals and shadows constitute a Boolean structure.
 Formal language LSD (Language for Shadows with Distributivity), which takes compound terms to denote shadows, is investigated. Expansions and
 enrichments of LSD are also considered toward the end of the paper.
 
	

  The hybrid logic 

H(@,¯)
 and the independence friendly modal logic IFML are compared for their expressive powers. We introduce a logic IFML
 
 c
  having a non-standard syntax and a compositional semantics; in terms of this logic a syntactic fragment of IFML is singled out, denoted IFML
 
 c
 . (In the Appendix it is shown that the game-theoretic semantics of IFML
 
 c
  coincides with the compositional semantics of IFML
 
 c
 .) The hybrid logic 

H(@,¯)
 is proven to be strictly more expressive than IFML
 
 c
 . By contrast, 

H(@,¯)
 and the full IFML are shown to be incomparable for their expressive powers. Building on earlier research (Tulenheimo and Sevenster 2006), a
 PSPACE-decidable fragment of the undecidable logic 

H(@,¯)
 is disclosed. This fragment is not translatable into the hybrid logic 

H(@)
 and has not been studied previously in connection with hybrid logics. In the Appendix IFML
 
 c
  is shown to lack the property of ˜quasi-positionality' but proven to enjoy the weaker property of ˜bounded quasi-positionality'. The latter fact provides from the IFML internal perspective an account of what makes the compositional semantics of IFML
 
 c
  possible.
 
	

  We study hybrid logics in topological semantics. We prove that hybrid logics of separation axioms are complete with respect
 to certain classes of finite topological models. This characterisation allows us to obtain several further results. We prove
 that aforementioned logics are decidable and PSPACE-complete, the logics of T
 1 and T
 2 coincide, the logic of T
 1 is complete with respect to two concrete structures: the Cantor space and the rational numbers.
 
	

  This paper examines and classifies the computational complexity of model checking and satisfiability for hybrid logics over
 frames with equivalence relations. The considered languages contain all possible combinations of the downarrow binder, the
 existential binder, the satisfaction operator, and the global modality, ranging from the minimal hybrid language to very expressive
 languages. For model checking, we separate polynomial-time solvable from PSPACE-complete cases, and for satisfiability, we
 exhibit cases complete for NP, PSpace, NExpTime, and even N2ExpTime. Our analysis includes the versions of all these languages without atomic propositions, and also complete frames.
 
	

  We consider the model checking problem for Hybrid Logic. Known algorithms so far are global in the sense that they compute,
 inductively, in every step the set of all worlds of a Kripke structure that satisfy a subformula of the input. Hence, they
 always exploit the entire structure. Local model checking tries to avoid this by only traversing necessary parts of the input
 in order to establish or refute the satisfaction relation between a given world and a formula. We present a framework for
 local model checking of Hybrid Logic based on games. We show that these games are simple reachability games for ordinary Hybrid
 Logic and weak Büchi games for Hybrid Logic with operators interpreted over the transitive closure of the accessibility relation
 of the underlying Kripke frame, and show how to solve these games thus solving the local model checking problem. Since the
 first-order part of Hybrid Logic is inherently hard to localise in model checking, we give examples, in the end, of how global
 model checkers can be optimised in certain special cases using well-established techniques like fixpoint approximations and
 divide-and-conquer algorithms.
 
	

  This paper contributes to the principled construction of tableau-based decision procedures for hybrid logic with global, difference,
 and converse modalities. We also consider reflexive and transitive relations. For converse-free formulas we present a terminating
 control that does not rely on the usual chain-based blocking scheme. Our tableau systems are based on a new model existence
 theorem.
 
	

Preface