-
20University of Sao Paulo (Sao Paulo), Brazil, July 28–31, 1998Bulletin of Symbolic Logic 5 (3). 1999.
-
101A short note on intuitionistic propositional logic with multiple conclusionsManuscrito 28 (2): 317-329. 2005.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 restri…Read more
-
Inheritance Defaults (Studies in Natural Language Processing)Cambridge University Press. 1993.reissued in soft cover 2006
-
From Quirky Case to Representing Space: Papers in Honor of Annie ZaenenCSLI Press. 2013.Annie Zaenen’s research has broadly influenced the field of linguistics from the underlying architecture of formal theories to the minute details of lexical representation. This volume assembles a wide range of essays from linguists who have been profoundly influenced by Zaenen’s work. Taking Zaenen as a model, the contributors explore a variety of topics, including the mapping of syntax onto argument and the relationship between syntax and semantics. From Quirky Case to Representing Space prese…Read more
-
8Linguistic 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…Read more
-
4Edited 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 i…Read more
-
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.
-
279Benchmarking 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 the…Read more
-
Relating Categorical and Kripke Semantics for Intuitionistic Modal LogicsIn Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic, Csli Publications. pp. 35-52. 1998.
-
61An ecumenical notion of entailmentSynthese 198 (S22): 5391-5413. 2019.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 th…Read more
-
21Dialectica categories, cardinalities of the continuum and combinatorics of idealsLogic Journal of the IGPL 25 (4): 585-603. 2017.
-
15Relating Categorical and Kripke Semantics for Intuitionistic Modal LogicsIn Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic, Csli Publications. pp. 35-52. 1998.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 …Read more
-
283LinealesO Que Nos Faz Pensar 107-123. 1991.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 …Read more
-
87Elements of Categorical Logic: Fifty Years Later (review)Logica Universalis 7 (3): 265-273. 2013.
-
29Intuitionistic N-GraphsLogic Journal of the IGPL 22 (2): 274-285. 2014.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 pre…Read more
-
28Linear logic model of state revisitedLogic Journal of the IGPL 22 (5): 791-804. 2014.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,…Read more
-
112On an intuitionistic modal logicStudia Logica 65 (3): 383-416. 2000.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 mod…Read more
-
44Intuitionistic hybrid logicJournal of Applied Logic 4 (3): 231-255. 2006.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…Read more
-
11Linear explicit substitutionsLogic Journal of the IGPL 8 (1): 7-31. 2000.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 t…Read more
-
13On an Intuitionistic Modal LogicStudia Logica 65 (3). 2000.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 Kripke 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…Read more
-
210The Dialectica CategoriesDissertation, University of Cambridge, UK. 1990.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 f…Read more
-
51Full intuitionistic linear logicAnnals of Pure and Applied Logic 64 (3): 273-291. 1993.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 elimin…Read more
-
University of BirminghamResearcher
Cupertino, CA, United States of America
Areas of Specialization
Logic and Philosophy of Logic |
Science, Logic, and Mathematics |