Representation and Reasoning about Evolutions of the World in the Context of Reasoning about Actions

The first step in reasoning about actions and change involves reasoning about how the world would evolve if a certain action is executed in a certain state. Most research on this assumes the evolution to be only a single step and focus on formulating the transition function that defines changes between states due to actions. In this paper we consider cases where the evolution is more than just a single change between one state and another. This is manifested when the execution of an action may trigger execution of other actions, or when multiple agents act on the environment following certain strategies.     

Curry-Howard Terms for Linear Logic

In this paper we 1. provide a natural deduction system for full first-order linear logic, 2. introduce Curry-Howard-style terms for this version of linear logic, 3. extend the notion of substitution of Curry-Howard terms for term variables, 4. define the reduction rules for the Curry-Howard terms and 5. outline a proof of the strong normalization for the full system of linear logic using a development of Girard's candidates for reducibility, thereby providing an alternative to Girard's proof using proof-nets.     

A cirquent calculus system with clustering and ranking

Cirquent calculus is a new proof-theoretic and semantic approach introduced by G. Japaridze for the needs of his theory of computability logic (CoL). The earlier article “From formulas to cirquents in computability logic” by Japaridze generalized formulas in CoL to circuit-style structures termed cirquents. It showed that, through cirquents with what are termed clustering and ranking, one can capture, refine and generalize independence-friendly (IF) logic. Specifically, the approach allows us to account for independence from propositional connectives in the same spirit as IF logic accounts for independence from quantifiers. Japaridze's treatment of IF logic, however, was purely semantical, and no deductive system was proposed. The present paper syntactically constructs a cirquent calculus system with clustering and ranking, sound and complete w.r.t. the propositional fragment of cirquent-based semantics. Such a system captures the propositional version of what is called extended IF logic, thus being an axiomatization of a nontrivial fragment of that logic.     

A Logic for Information Systems

A conception of an information system has been introduced by Pawlak. The study has been continued in works of Pawlak and Orlowska and in works of Vakarelov. They had proposed some basic relations and had constructed a formal system of a modal logic that describes the relations and some of their Boolean combinations. Our work is devoted to a generalization of this approach. A class of relation systems and a complete calculus construction method for these systems are proposed. As a corollary of our main result, our paper contains a solution of a Vakarelov's problem: how to construct a formal system that describes all the Boolean combinations of the basic relations.     

Complete Axiomatizations for Reasoning about Knowledge and Branching Time

Sound and complete axiomatizations are provided for a number of different logics involving modalities for the knowledge of multiple agents and operators for branching time, extending previous work of Halpern, van der Meyden and Vardi [to appear, SIAM Journal on Computing] for logics of knowledge and linear time. The paper considers the system constraints of synchrony, perfect recall and unique initial states, which give rise to interaction axioms. The language is based on the temporal logic CTL*, interpreted with respect to a version of the bundle semantics.     

Parsing Pregroup Grammars and Lambek Calculus Using Partial Composition

The paper presents a way to transform pregroup grammars into contextfree grammars using functional composition. The same technique can also be used for the proof-nets of multiplicative cyclic linear logic and for Lambek calculus allowing empty premises.     

Quantized Linear Logic,Involutive Quantales and Strong Negation

A new logic, quantized intuitionistic linear logic (QILL), is introduced, and is closely related to the logic which corresponds to Mulvey and Pelletier's (commutative) involutive quantales. Some cut-free sequent calculi with a new property quantization principle and some complete semantics such as an involutive quantale model and a quantale model are obtained for QILL. The relationship between QILL and Wansing's extended intuitionistic linear logic with strong negation is also observed using such syntactical and semantical frameworks.     

Using Lexicographic Parametric Programming for Searching a Non-dominated Set in Multiple-Objective Linear Programming

In this paper we propose an approach which makes it possible to search non-dominated and only non-dominated solutions in multiple-objective linear programming. The approach is based on the use of a reference direction and lexicographic parametric programming. The requisite theory is developed in the paper. The use of the approach is illustrated with a numerical example.     

An Axiomatisation for the Multi-modal Logic of Knowledge and Linear Time LTK

The paper aims at providing the multi-modal propositional logicLTK with a sound and complete axiomatisation. This logic combinestemporal and epistemic operators and focuses on m odeling thebehaviour of a set of agents operating in a system on the backgroundof a temporal framework. Time is represented as linear and discrete,whereas knowledge is modeled as an S₅-like modality. A furthermodal operator intended to represent environment knowledge isadded to the system in order to achieve the expressive powersufficient to describe the piece of information available tothe agents at each moment in the flow of time.     

Memory for Actions of an Event: Older and Younger Adults Compared

Previous studies have shown increased false memory effects in older compared to younger adults. To investigate this phenomenon in event memory, in the present study, the authors presented younger and older adults with a robbery. A distinction was made between verbal and visual actions of the event, and recognition and subjective experience of retrieval (remember/know/guess judgments) were analyzed. Although there were no differences in hits, older adults accepted more false information as true and, consequently, showed less accurate recognition than younger adults. Moreover, older adults were more likely than younger adults to accompany these errors with remember judgments. Young adults accepted fewer false verbal actions than visual ones and awarded fewer remember judgments to their false alarms for verbal than for visual actions. Older adults, however, did not show this effect of type of information. These results suggest that aging is a relevant factor in memory for real-life eyewitness situations.     

A Deep Inference System for the Modal Logic S5

We present a cut-admissible system for the modal logic S5 in a formalism that makes explicit and intensive use of deep inference. Deep inference is induced by the methods applied so far in conceptually pure systems for this logic. The system enjoys systematicity and modularity, two important properties that should be satisfied by modal systems. Furthermore, it enjoys a simple and direct design: the rules are few and the modal rules are in exact correspondence to the modal axioms. Presented by Heinrich Wansing     

A maximin model for IRT-based test design with practical constraints

A maximin model for IRT-based test design is proposed. In the model only the relative shape of the target test information function is specified. It serves as a constraint subject to which a linear programming algorithm maximizes the information in the test. In the practice of test construction, several demands as linear constraints in the model. A worked example of a text construction problem with practical constraints is presented. The paper concludes with a discussion of some alternative models of test construction.The authors are indebted to Jos J. Adea for suggesting Equation 17 as a Simplification of an earlier version of this constraint. This research was suuorted in part by a grant from the Dutch Organization for Research (NWO) through the Foundation for Psychological and Psychonomic Research in the Netherlands (Psychon).     

A verification framework for agent programming with declarative goals

A long and lasting problem in agent research has been to close the gap between agent logics and agent programming frameworks. The main reason for this problem of establishing a link between agent logics and agent programming frameworks is identified and explained by the fact that agent programming frameworks have hardly incorporated the concept of a declarative goal. Instead, such frameworks have focused mainly on plans or goals-to-do instead of the end goals to be realised which are also called goals-to-be. In this paper, the programming language GOAL is introduced which incorporates such declarative goals. The notion of a commitment strategy—one of the main theoretical insights due to agent logics, which explains the relation between beliefs and goals—is used to construct a computational semantics for GOAL. Finally, a proof theory for proving properties of GOAL agents is introduced. Thus, the main contribution of this paper, rather than the language GOAL itself, is that we offer a complete theory of agent programming in the sense that our theory provides both for a programming framework and a programming logic for such agents. An example program is proven correct by using this programming logic.     

班级环境与学生适应性的多层线性模型

此研究探索中国中小学体制下的班级社会心理环境对于学生的适应性的关系。以江光荣和林盂平所编制的《我的班级》问卷测量班级环境．选择学生的学校适应（由Teacher-Child Rating Scale（T-CRS）测量）、主观幸福感（以Student’s Life Satisfaction Scale（SLSS）测量）和焦虑（用State-Trait Anxiety Inventory for Children（STAlC）测量）作为适应指标．以多层线性模型（HLM）方法进行分析,结果显示：学生个体所知觉到的班级环境,对其适应水平有相当肯定的鳃释力,而一个班级学生整体适应水平的高低,与这个班的班级环境有极大关联。此结果表明．中国学校体制下的班级社会心理环境对于学生的发展和适应状况,具有举足轻重的作用。     

A multi-attribute extension of the secretary problem: Theory and experiments

We present a generalization of a class of sequential search problems with ordinal ranks, referred to as “secretary” problems, in which applicants are characterized by multiple attributes. We then present a procedure for numerically computing the optimal search policy and test it in two experiments with incentive-compatible payoffs. With payoffs dependent on the absolute ranks of the attributes, we test the optimal search model with both symmetric (Experiment 1) and asymmetric (Experiment 2) search problems. In both experiments we find that, relative to the optimal search policy, subjects stop the search too early. Our results show that this bias is largely driven by a propensity to stop prematurely on applicants of intermediate (relative) quality.