Search

Given that today 60% of Internet traffic is generated by bots, 'CAPTCHA' (Completely Automated Public Turing Test to tell Computers and Humans Apart) tests that are supposedly impossible to be done by robots have been introduced. What are the cognitive and emotional effects of these tests on Internet users? Does this request to demonstrate they are not a robot affect users' identity as human beings? To answer these questions, we selected two groups (117 and 116 respondents, respectively). An online questionnaire that differed only in the task was proposed: we asked the first group to complete some CAPTCHA tests, and the second group to complete some logic tests. In addition to other questions in both versions, we introduced the TLX scale (NASA). Preliminary results show that CAPTCHA execution is associated with feelings of alienation and that the user's self-perception of humanity is influenced by the execution of the two different types of test. [ABSTRACT FROM AUTHOR]

We present two extensions of the LF constructive type theory featuring monadic locks. A lock is a monadic type construct that captures the effect of an external call to an oracle. Such calls are the basic tool for plugging-in and gluing together, different metalanguages and proof development environments. Oracles can be invoked either to check that a constraint holds or to provide a witness. The systems are presented in the canonical style developed by the 'CMU School.' The first system, CLLF𝒫, is the canonical version of the system LLF𝒫, presented earlier by the authors. The second system, CLLF𝒫?, features the possibility of invoking the oracle to obtain also a witness satisfying a given constraint. In order to illustrate the advantages of our new frameworks, we show how to encode logical systems featuring rules that deeply constrain the shape of proofs. The locks mechanisms of CLLF𝒫 and CLLF𝒫? permit to factor out naturally the complexities arising from enforcing these 'side conditions,' which severely obscure standard LF encodings. We discuss Girard's Elementary Affine Logic, Fitch–Prawitz set theory, call-by-value λ-calculi and functions, both total and even partial. [ABSTRACT FROM AUTHOR]

We investigate youths' conceptualization of social robots. Informed by Schudson's theory of the potency of the cultural object, we conducted two studies. The first study centered on essays on social robots written by bachelor's and master's students. The second study centered on prototypes of social robots built by small groups comprised of same students. The essays and prototypes were content analyzed. The results confirm that social robots embody all five dimensions that characterize cultural objects. However, to fully understand this peculiar cultural object, another dimension needs to be introduced: dynamicity. [ABSTRACT FROM AUTHOR]

The LFP Framework is an extension of the Harper-Honsell-Plotkin's Edinburgh Logical Framework LF with external predicates, hence the name Open Logical Framework. This is accomplished by defining lock type constructors, which are a sort of ◁ -modality constructors, releasing their argument under the condition that a possibly external predicate is satisfied on an appropriate typed judgement. Lock types are defined using the standard pattern of constructive type theory, i.e. via introduction, elimination and equality rules. Using LFP, one can factor out the complexity of encoding specific features of logical systems, which would otherwise be awkwardly encoded in LF, e.g. side-conditions in the application of rules in Modal Logics, and sub-structural rules, as in non-commutative Linear Logic. The idea of LFP is that these conditions need only to be specified, while their verification can be delegated to an external proof engine, in the style of the Poincaré Principle or Deduction Modulo. Indeed such paradigms can be adequately formalized in LFP. We investigate and characterize the meta-theoretical properties of the calculus underpinning LFP: strong normalization, confluence and subject reduction. This latter property holds under the assumption that the predicates are well-behaved, i.e. closed under weakening, permutation, substitution and reduction in the arguments. Moreover, we provide a canonical presentation of LFP, based on a suitable extension of the notion of βη-long normal form, allowing for smooth formulations of adequacy statements. [ABSTRACT FROM AUTHOR]

Joyal's categorical construction on (well-founded) Conway games and winning strategies provides a compact closed category, where tensor and linear implication are defined via Conway disjunctive sum (in combination with negation for linear implication). The equivalence induced on games by the morphisms coincides with the contextual closure of the equideterminacy relation w.r.t. the disjunctive sum. Recently, the above categorical construction has been generalized to non-wellfounded games. Here we investigate Joyal's construction for a different notion of sum, i.e. selective sum. While disjunctive sum reflects the interleaving semantics, selective sum accommodates a form of parallelism, by allowing the current player to move in different parts of the board simultaneously. We show that Joyal's categorical construction can be successfully extended to selective sum, when we consider alternating games, i.e. games where each position is marked as Left player (L) or Right player (R), that is only L or R can move from that position, R starts, and L/R positions strictly alternate. Alternating games typically arise in the context of Game Semantics. This category of well-founded games with selective sum is symmetric monoidal closed, and it induces exactly the equideterminacy relation. Generalizations to non-wellfounded games give linear categories, i.e. models of Linear Logic. Our game models, providing a certain level of parallelism, may be situated halfway between traditional sequential alternating game models and the concurrent game models by Abramsky and Mellies. We work in a context of coalgebraic games, whereby games are viewed as elements of a final coalgebra, and game operations are defined as final morphisms. [ABSTRACT FROM AUTHOR]

Taking the view that infinite plays are draws, we study Conway non-terminating games and non-losing strategies. These admit a sharp coalgebraic presentation, where non-terminating games are seen as a final coalgebra and game contructors, such as disjunctive sum, as final morphisms. We have shown, in a previous paper, that Conway’s theory of terminating games can be rephrased naturally in terms of game (pre)congruences. Namely, various conceptually independent notions of equivalence can be defined and shown to coincide on Conway’s terminating games. These are the equivalence induced by the ordering on surreal numbers, the contextual equivalence determined by observing what player has a winning strategy, Joyal’s categorical equivalence, and, for impartial games, the denotational equivalence induced by Grundy semantics. In this paper, we discuss generalizations of such equivalences to non-terminating games and non-losing strategies. The scenario is even more rich and intriguing in this case. In particular, we investigate efficient characterizations of the contextual equivalence, and we introduce a category of fair strategies and a category of fair pairs of strategies, both generalizing Joyal’s category of Conway games and winning strategies. Interestingly, the category of fair pairs captures the equivalence defined by Berlekamp, Conway, Guy on loopy games. [ABSTRACT FROM PUBLISHER]

The article discusses the model for the universality of cardinal ordering. Mathematicians offered proof that any partial ordering can be represented by an appropriate model of ZF injective of the ordering set of cardinals. A hypothesis that has been formed by speculating or conjecturing has been supposed that (CU) is consistent with ZF and working on an ideal symmetric submodel for an Easton generic extension of a model.

The article offers information on the comparison of axioms related to local and global universality. It offers information on the classification of set theoretical formulas and the models of calculus. It offers information on the use of standard notations and elementary set-theoretical related to the axioms.

Proves that many intersection type theories of interest satisfy an Approximation theorem with respect to a suitable notion of approximant. Implication of a type for terms only through an existing approximant; Use of a Kripke version of suitable sets where bases correspond to words.