In this paper we consider an intuitionistic variant of the modal logic S4 (which we call IS4). The novelty of this paper is that we place particular importance on the natural deduction formulation of IS4— our formulation has several important metatheoretic properties. In addition, we study models of IS4— not in the framework of Kirpke semantics, but in the more general framework of category theory. This allows not only a more abstract definition of a whole class of models but also (...) a means of modelling proofs as well as provability. (shrink)

A common misconception among logicians is to think that intuitionism is necessarily tied-up with single conclusion calculi. Single conclusion calculi can be used to model intuitionism and they are convenient, but by no means are they necessary. This has been shown by such influential textbook authors as Kleene, Takeuti and Dummett, to cite only three. If single conclusions are not necessary, how do we guarantee that only intuitionistic derivations are allowed? Traditionally one insists on restrictions on particular rules: implication right, (...) negation right and universal quantification right are required to be single conclusion rules. In this note we show that instead of a cardinality restriction such as one-conclusion-only, we can use a notion of dependency between formulae to enforce the constructive character of derivations. The system we obtain, called FIL for full intuitionistic logic, satisfies basic properties such as soundness, completeness and cut elimination. We present two motivating applications of FIL and discuss some future work. (shrink)

In this paper we give a brief treatment of a theory of proofs for a system of Full Intuitionistic Linear Logic. This system is distinct from Classical Linear Logic, but unlike the standard Intuitionistic Linear Logic of Girard and Lafont includes the multiplicative disjunction par. This connective does have an entirely natural interpretation in a variety of categorical models of Intuitionistic Linear Logic. The main proof-theoretic problem arises from the observation of Schellinx that cut elimination fails outright for an intuitive (...) formulation of Full Intuitionistic Linear Logic; the nub of the problem is the interaction between par and linear implication. We present here a term assignment system which gives an interpretation of proofs as some kind of non-deterministic function. In this way we find a system which does enjoy cut elimination. The system is a direct result of an analysis of the categorical semantics, though we make an effort to present the system as if it were purely a proof-theoretic construction. (shrink)

This thesis describes two classes of Dialectica categories. Chapter one introduces dialectica categories based on Goedel's Dialectica interpretation and shows that they constitute a model of Girard's Intuitionistic Linear Logic. Chapter two shows that, with extra assumptions, we can provide a comonad that interprets Girard's !-course modality. Chapter three presents the second class of Dialectica categories, a simplification suggested by Girard, that models (classical) Linear Logic and chapter four shows how to provide modalities ! and ? for this second class (...) of construction. (shrink)

Edited in collaboration with FoLLI, the Association of Logic, Language and Information this book constitutes the refereed proceedings of the 22nd Workshop on Logic, Language, Information and Computation, WoLLIC 2015, held in the campus of Indiana University, Bloomington, IN, USA in July 2015. The 14 contributed papers, presented together with 8 invited lectures and 4 tutorials, were carefully reviewed and selected from 44 submissions. The focus of the workshop was on interdisciplinary research involving formal logic, computing and programming theory, and (...) natural language and reasoning. (shrink)

Hybrid logics are a principled generalization of both modal logics and description logics, a standard formalism for knowledge representation. In this paper we give the first constructive version of hybrid logic, thereby showing that it is possible to hybridize constructive modal logics. Alternative systems are discussed, but we fix on a reasonable and well-motivated version of intuitionistic hybrid logic and prove essential proof-theoretical results for a natural deduction formulation of it. Our natural deduction system is also extended with additional inference (...) rules corresponding to conditions on the accessibility relations expressed by so-called geometric theories. Thus, we give natural deduction systems in a uniform way for a wide class of constructive hybrid logics. This shows that constructive hybrid logics are a viable enterprise and opens up the way for future applications. (shrink)

The first aim of this note is to describe an algebraic structure, more primitive than lattices and quantales, which corresponds to the intuitionistic flavour of Linear Logic we prefer. This part of the note is a total trivialisation of ideas from category theory and we play with a toy-structure a not distant cousin of a toy-language. The second goal of the note is to show a generic categorical construction, which builds models for Linear Logic, similar to categorical models GC of (...) [deP1990], but more general. The ultimate aim is to relate different categorical models of linear logic. (shrink)

Linguistic Issues in Language Technology (LiLT) is an open-access journal that focuses on the relationships between linguistic insights and language technology. In conjunction with machine learning and statistical techniques, deeper and more sophisticated models of language and speech are needed to make significant progress in both existing and newly emerging areas of computational language analysis. The vast quantity of electronically accessible natural language data (text and speech, annotated and unannotated, formal and informal) provides unprecedented opportunities for data-intensive analysis of linguistic (...) phenomena, which can in turn enrich computational methods. Taking an eclectic view on methodology, LiLT provides a forum for this work. In this volume, contributors offer new perspectives on semantic representations for textual inference. (shrink)

We consider two systems of constructive modal logic which are computationally motivated. Their modalities admit several computational interpretations and are used to capture intensional features such as notions of computation, constraints, concurrency, etc. Both systems have so far been studied mainly from type-theoretic and category-theoretic perspectives, but Kripke models for similar systems were studied independently. Here we bring these threads together and prove duality results which show how to relate Kripke models to algebraic models and these in turn to the (...) appropriate categorical models for these logics. (shrink)

In an unpublished note Reddy introduced an extended intuitionistic linear calculus, called LLMS (for Linear Logic Model of State), to model state manipulation via the notions of sequential composition and ‘regenerative values’. His calculus introduces the connective ‘before’ ▹ and an associated modality †, for the storage of objects sequentially reusable. Earlier and independently de Paiva introduced a (collection of) dialectica categorical models for (classical and intuitionistic) Linear Logic, the categories Dial2Set. These categories contain, apart from the structure needed (...) to model linear logic, an extra tensor product functor and an extra comonad structure corresponding to a modality related to the extra tensor product. It is surprising that these works arising from completely different motivations can be related in a meaningful way. In this article, following joint work with Corrêa and Haeusler, we first adapt Reddy's system LLMS providing a commutative version of the connective ‘before’ and its associated modality and then construct a dialectica category on Sets , which we show is a sound model for the modified version of Reddy's the system LLMSc. Moreover, following the work of Tucker, we provide another variant of the Dialectica categories with a non-commutative tensor and its associated modality, which models soundlyLLMS itself. We conclude with some speculation on future applications. (shrink)

Benchmarking automated theorem proving (ATP) systems using standardized problem sets is a well-established method for measuring their performance. However, the availability of such libraries for non-classical logics is very limited. In this work we propose a library for benchmarking Girard's (propositional) intuitionistic linear logic. For a quick bootstrapping of the collection of problems, and for discussing the selection of relevant problems and understanding their meaning as linear logic theorems, we use translations of the collection of Kleene's intuitionistic theorems in the (...) traditional monograph "Introduction to Metamathematics". We analyze four different translations of intuitionistic logic into linear logic and compare their proofs using a linear logic based prover with focusing. In order to enhance the set of problems in our library, we apply the three provability-preserving translations to the propositional benchmarks in the ILTP Library. Finally, we generate a comprehensive set of reachability problems for Petri nets and encode such problems as linear logic sequents, thus enlarging our collection of problems. (shrink)

The λσ-calculus adds explicit substitutions to the λ-calculus so as to provide a theoretical framework within which the implementation of functional programming languages can be studied. This paper generalises the λσ-calculus to provide a linear calculus of explicit substitutions, called xDILL, which analogously describes the implementation of linear functional programming languages.Our main observation is that there are non-trivial interactions between linearity and explicit substitutions and that xDILL is therefore best understood as a synthesis of its underlying logical structure and the (...) technology of explicit substitutions. This is in contrast to the λσ-calculus where the explicit substitutions are independent of the underlying logical structure. (shrink)

Much has been said about intuitionistic and classical logical systems since Gentzen’s seminal work. Recently, Prawitz and others have been discussing how to put together Gentzen’s systems for classical and intuitionistic logic in a single unified system. We call Prawitz’ proposal the Ecumenical System, following the terminology introduced by Pereira and Rodriguez. In this work we present an Ecumenical sequent calculus, as opposed to the original natural deduction version, and state some proof theoretical properties of the system. We reason that (...) sequent calculi are more amenable to extensive investigation using the tools of proof theory, such as cut-elimination and rule invertibility, hence allowing a full analysis of the notion of Ecumenical entailment. We then present some extensions of the Ecumenical sequent system and show that interesting systems arise when restricting such calculi to specific fragments. This approach of a unified system enabling both classical and intuitionistic features sheds some light not only on the logics themselves, but also on their semantical interpretations as well as on the proof theoretical properties that can arise from combining logical systems. (shrink)

This collection of papers, celebrating the contributions of Swedish logician Dag Prawitz to Proof Theory, has been assembled from those presented at the Natural Deduction conference organized in Rio de Janeiro to honour his seminal research. Dag Prawitz’s work forms the basis of intuitionistic type theory and his inversion principle constitutes the foundation of most modern accounts of proof-theoretic semantics in Logic, Linguistics and Theoretical Computer Science.

The geometric system of deduction called N-Graphs was introduced by de Oliveira in 2001. The proofs in this system are represented by means of digraphs and, while its derivations are mostly based on Gentzen's sequent calculus, the system gets its inspiration from geometrically based systems, such as the Kneales' tables of development, Statman's proofs-as-graphs, Buss' logical flow graphs, and Girard's proof-nets. Given that all these geometric systems appeal to the classical symmetry between premises and conclusions, providing an intuitionistic version of (...) any of these is an interesting exercise in extending the range of applicability of the geometric system in question. In this article we produce an intuitionistic version of N-Graphs, based on Maehara's LJ' system, as described by Takeuti. Recall that LJ' has multiple conclusions in all but the essential intuitionistic rules, e.g., implication right and negation right. We show soundness and completeness of our intuitionistic N-Graphs with respect to LJ'. We also discuss how we expect to extend this work to a version of N-Graphs corresponding to the intuitionistic logic system FIL (Full Intuitionistic Logic) of de Paiva and Pereira and sketch future developments. (shrink)

Cuprins CONTUR Re-Introducere sau: Dincolo de „teoria şi practica” informării şi documentării – Spre o hermeneutică posibilă şi necesară Proiectul şi Programul PHILOBIBLON( în noua formulare) FOCUS Dana Stana, Omonimia şi paronimia în bibliologie Victoria Frâncu, Profesia de bibliotecar la graniţa dintre spaţiul bibliotecii şi ciberspaţiu Olimpia Curta, Laboratorul de informatică şi profesioniştii săi Ionel Enache, Fundamentele teoretice ale marketingului de bibliotecă Maria Petrescu, Bibliotecile digitale şi impactul lor asupra tinerilor Adriana Szekely, Liana Grigore, Bibliorev – în continuă schimbare István (...) Király V., Proiect în vederea Acreditării ISI al revistei PHILOBIBLON Valeria Salánki, Cultura organizaţională. Propunere de studiu asupra culturii organizaţionale – octombrie 2008 Marian Petcu, Originile faptului divers în presa română Tudor-George Pereverza Expresia bibliografică a Iconografiei eminesciene (Fotografie şi artă plastică, 1939-1989) Vlad A. Codrea, Gabriela-Rodica Morărescu, Forray Erzsébet, Catalogus Raritatum et Benefactorum, un manuscris reprezentativ din perioada de început a Muzeului de Ştiinţele Naturii din Aiud 4 Alin Mihai Gherman, Pornind de la o Bucoavnă necunoscută Roxana Bălăucă, Tipărituri franceze în colecţiile BCU „Lucian Blaga”: secolul al XVIII-lea Maria-Stela Constantinescu-Matiţa, Szabó Károly – bibliotecar, bibliograf şi istoric Roxana Bălăucă, Theodor Aman în Donaţia Sion Margareta Berchez, Îmbogăţirea colecţiilor Bibliotecii Universităţii de Ştiinţe Agricole şi Medicină Veterinară Cluj-Napoca prin schimbul de publicaţii de-a lungul timpului Ioana Rotund, O oază francofonă la Cluj Ilona Okos-Rigó, Biblioteca şi Grădina Botanică Clujeană Gabriela Pop, Institutul de Iudaistică şi Istorie Evreiască „Dr. Moshe Carmilly” şi Biblioteca de Studii Iudaice Mariana Falup, Împrumutul interbibliotecar intern şi internaţional şi livrarea de documente la B.C.U. Cluj-Napoca ORIZONTURI Doru Radosav, Viaţa ca alterego. Petrea Icoanei: travesti şi clandestinitate în mişcarea de rezistenţă anticomunistă Ionuţ Costea, Mitbiografia între propagandă şi memorie Gabriela Morărescu ;Vlad Codrea, Preocupări pentru cunoaşterea şi protecţia naturii în scrierile unui entuziast naturalist al secolului XIX: Basiliu Basiota Alin Mihai Gherman, Vechi lexic bibliotecăresc Raluca Betea, Influenţa artei Renaşterii asupra decoraţiei icoanelor din secolele XVI-XVIII din Transilvania şi Maramureş 5 Monica Mureşan, Căsătoria civilă ca aspect al modernizării societăţii transilvănene la sfârşitul secolului al XIX –lea. – Discurs oficial şi receptare socială reflectate în presa vremii Ancuţa-Lăcrimioara Chiş, Diferenţa şi discriminarea socio-politică a femeii Irina Petraş, Casa, locul vieţii (fragmente) Monica Mureşan Pentru o istorie a morţii în peisajul istoriografic românesc - prezentarea unor contribuţii colective recente: Religiozitate şi atitudini în faţa morţii în spaţiul transilvan din premodernitate până în secolul XX, coord. Mihaela Grancea, 2005 şi Discursuri despre moarte în Transilvania secolelor XVI-XX, coord Mihaela Grancea şi Ana Dumitran, 2006. REFLEXII Olimpia Curta, Reviste electronice. Baze şi perspective de Alice Keller – Recenzie Adrian Grănescu, Arhitectura Clinicilor Universitare din Cluj 1886-1903 Dorina Buia, Itinerar de suflet la Tăul Muced Raluca Soare, De la teoriile ataşamentului la tehnicile de intervenţie în psihoterapie. (Školka Enikő – Teorii explicative, Modele şi Tehnici de intervenţie în psihologie clinică şi psihoterapie) Sidonia Nedeianu Grama, Mitbiografia politică în istoria orală Raluca Soare, Opera bibliothecariorum 1990-2007 – Recenzie Ionuţ Costea, Kovács Mária, A kolozsvári „Lucian Blaga” Központi Egyetemi Könyvtár 19. századi magyar nyelvű kéziratainak katalógusa. Első kötet: történelmi és földrajzi kéziratok/ Catalogul manuscriselor maghiare din secolul al 19-lea din colecţiile Bibliotecii Centrale Universitare „Lucian Blaga” Volumul I: Manuscrise de istorie şi geografie, Editura Argonaut, Cluj-Napoca, 2007, 218 p. – Recenzie 6 Ana Maria Căpâlneanu, Lola Maria Petrescu – Biblioteca şi provocările secolului XXI, Cluj-Napoca: Risoprint, 2007 István Király V, Bibliografia ca instrument al clarificării de sine Kinga Tamás, Viorica Sâncrăian - un coleg şi un bibliotecar de excepţie În colecţia BIBLIOTHECA BIBLIOLOGICA au apărut Revista PHILOBIBLON – Volumele apărute. (shrink)

The extent to which game play is experienced as engaging is an important criterion for the playability of video games. This study investigates how video games can be designed towards increased levels of experienced engagement over time. For this purpose, two experiments were conducted in which a total of 35 participants repeatedly played a video game. Results indicate that experienced engagement is based on the extent to which the game provides rich experiences as well as by the extent to which (...) the game provides a sense of control. In view of the influence of both game features and players’ expertise on the levels of experienced richness and control, it is concluded that game features should be modified over time to maintain optimal levels of engagement. (shrink)

This article provides ethical guidance on using race in health research as a variable or in defining the study population. To this end, a plain, non-exhaustive checklist is provided for researchers and research ethics committees, preceded by a brief introduction on the need for justification when using race as a variable or in defining a study population, the problem of exoticism, that distinctions pertain between race, ethnicity and ancestry, the problematic naming of races, and that race does not serve well (...) as a presumed biological construct in genetic research. (shrink)

The US neutrino community gathered at the Workshop on the Intermediate Neutrino Program at Brookhaven National Laboratory February 4-6, 2015 to explore opportunities in neutrino physics over the next five to ten years. Scientists from particle, astroparticle and nuclear physics participated in the workshop. The workshop examined promising opportunities for neutrino physics in the intermediate term, including possible new small to mid-scale experiments, US contributions to large experiments, upgrades to existing experiments, R&D plans and theory. The workshop was organized into (...) two sets of parallel working group sessions, divided by physics topics and technology. Physics working groups covered topics on Sterile Neutrinos, Neutrino Mixing, Neutrino Interactions, Neutrino Properties and Astrophysical Neutrinos. Technology sessions were organized into Theory, Short-Baseline Accelerator Neutrinos, Reactor Neutrinos, Detector R&D and Source, Cyclotron and Meson Decay at Rest sessions.This report summarizes discussion and conclusions from the workshop. (shrink)

This paper, which gives continuity to another article, analyzes the content of I Dialogus V, 14-22 and, in an appendix, presents our Portuguese translation of this excerpt. In these chapters, the Inceptor Venerabilis discusses whether St. Peter and the Roman Church possess primacy over all other apostles and churches; andwhether this primacy is granted by God himself. Ockham first presents, not ad litteram, the opinion of those who refute the thesis that Christ did not give primacy to Peter and the (...) Roman Church. Then, because this thesis fully deflates papal power, he proposes a contrary thesis based on five proofs. We conclude that Ockham’s unnamed opponent is Marsilius of Padua, whose opinions are in his Defensor Pacis. (shrink)

© 2016 Regents of the University of California.The Review summarizes much of particle physics and cosmology. Using data from previous editions, plus 3,062 new measurements from 721 papers, we list, evaluate, and average measured properties of gauge bosons and the recently discovered Higgs boson, leptons, quarks, mesons, and baryons. We summarize searches for hypothetical particles such as supersymmetric particles, heavy bosons, axions, dark photons, etc. All the particle properties and search limits are listed in Summary Tables. We also give numerous (...) tables, figures, formulae, and reviews of topics such as Higgs Boson Physics, Supersymmetry, Grand Unified Theories, Neutrino Mixing, Dark Energy, Dark Matter, Cosmology, Particle Detectors, Colliders, Probability and Statistics. Among the 117 reviews are many that are new or heavily revised, including those on Pentaquarks and Inflation. The complete Review is published online in a journal and on the website of the Particle Data Group. The printed PDG Book contains the Summary Tables and all review articles but no longer includes the detailed tables from the Particle Listings. A Booklet with the Summary Tables and abbreviated versions of some of the review articles is also available. (shrink)