The categorical modeling of Petri nets has received much attention recently. The Dialectica construction has also had its fair share of attention. We revisit the use of the Dialectica construction as a categorical model for Petri nets generalising the original application to suggest that Petri nets with different kinds of transitions can be modelled in the same categorical framework. Transitions representing truth-values, probabilities, rates or multiplicities, evaluated in different algebraic structures called lineales are useful and are modelled here in the same category. We investigate (categorical instances of) this generalised model and its connections to more recent models of categorical nets. Final version for Fundamenta Informaticae

This paper presents categorical formulations of Turing, Medvedev, Muchnik, and Weihrauch reducibilities in Computability Theory, utilizing Lawvere doctrines. While the first notions lend themselves to a smooth categorical presentation, essentially dualizing the traditional idea of realizability doctrines, Weihrauch reducibility and its extensions to represented and multi-represented spaces require a separate investigation. Our abstract analysis of these concepts highlights a shared characteristic among all these reducibilities. Specifically, we demonstrate that all these doctrines stemming from computability concepts can be proven to be instances of completions of quantifiers for doctrines, analogous to what occurs for doctrines for realizability. As a corollary of these results, we will be able to formally compare Weihrauch reducibility with the dialectica doctrine constructed from a doctrine representing Turing degrees.

Mathematics is a highly specialized domain with its own unique set of challenges. Despite this, there has been relatively little research on natural language processing for mathematical texts, and there are few mathematical language resources aimed at NLP. In this paper, we aim to provide annotated corpora that can be used to study the language of mathematics in different contexts, ranging from fundamental concepts found in textbooks to advanced research mathematics. We preprocess the corpora with a neural parsing model and some manual intervention to provide part-of-speech tags, lemmas, and dependency trees. In total, we provide 182397 sentences across three corpora. We then aim to test and evaluate several noteworthy natural language processing models using these corpora, to show how well they can adapt to the domain of mathematics and provide useful tools for exploring mathematical language. We evaluate several neural and symbolic models against benchmarks that we extract from the corpus metadata to show that terminology extraction and definition extraction do not easily generalize to mathematics, and that additional work is needed to achieve good performance on these metrics. Finally, we provide a learning assistant that grants access to the content of these corpora in a context-sensitive manner, utilizing text search and entity linking. Though our corpora and benchmarks provide useful metrics for evaluating mathematical language processing, further work is necessary to adapt models to mathematics in order to provide more effective learning assistants and apply NLP methods to different mathematical domains.

Abstract Against the backdrop of the ever-improving Natural Language Inference (NLI) models, recent efforts have focused on the suitability of the current NLI datasets and on the feasibility of the NLI task as it is currently approached. Many of the recent studies have exposed the inherent human disagreements of the inference task and have proposed a shift from categorical labels to human subjective probability assessments, capturing human uncertainty. In this work, we show how neither the current task formulation nor the proposed uncertainty gradient are entirely suitable for solving the NLI challenges. Instead, we propose an ordered sense space annotation, which distinguishes between logical and common-sense inference. One end of the space captures non-sensical inferences, while the other end represents strictly logical scenarios. In the middle of the space, we find a continuum of common-sense, namely, the subjective and graded opinion of a “person on the street.” To arrive at the proposed annotation scheme, we perform a careful investigation of the SICK corpus and we create a taxonomy of annotation issues and guidelines. We re-annotate the corpus with the proposed annotation scheme, utilizing four symbolic inference systems, and then perform a thorough evaluation of the scheme by fine-tuning and testing commonly used pre-trained language models on the re-annotated SICK within various settings. We also pioneer a crowd annotation of a small portion of the MultiNLI corpus, showcasing that it is possible to adapt our scheme for annotation by non-experts on another NLI corpus. Our work shows the efficiency and benefits of the proposed mechanism and opens the way for a careful NLI task refinement.

Abstract Gödel’s Dialectica interpretation was designed to obtain the consistency of Peano arithmetic via a proof of consistency of Heyting arithmetic and double negation. In recent years, proof theoretic transformations (the so-called proof interpretations) based on Gödel’s Dialectica interpretation have been used systematically to extract new content from proofs and so the interpretation has found relevant applications in several areas of mathematics and computer science. Following our previous work on ‘Gödel fibrations’, we present a (hyper)doctrine characterization of the Dialectica, which corresponds exactly to the logical description of the interpretation. To show that, we derive the soundness of the interpretation of the implication connective, as expounded on by Spector and Troelstra, in the categorical model. This requires extra logical principles, going beyond intuitionistic logic, namely Markov Principle and the Independence of Premise principle, as well as some choice. We show how these principles are satisfied in the categorical setting, establishing a tight (internal language) correspondence between the logical system and the categorical framework. We make sure that this tight correspondence extends to the use of the principles above, instead of the weaker rules we had proved earlier on. This tight correspondence should come handy not only when discussing the traditional applications of the Dialectica but also when dealing with newer uses in modelling games or concurrency theory.

Dialectica categories are interesting categorical models of Linear Logic which preserve the differences between linear connectives that the logic is supposed to make, unlike some of the most traditional models like coherence spaces. They arise from the categorical modelling of Gödel’s Dialectica interpretation and seem to be having a revival: connections between Dialectica constructions and containers, lenses and polynomials have been described recently in the literature. In this note I will recap the basic Dialectica constructions and then go on to describe the less well-known interplay of comonads, coalgebras and comonoids that characterizes the composite functor standing for the "of course!" operator in dialectica categories. This composition of comonads evokes some work on stateful games by Laird and others, also discussed in the setting of Reddy’s system LLMS (Linear Logic Model of State).

We introduce the notion of a Gödel fibration, which is a fibration categorically embodying both the logical principle of traditional Skolemization (we can exchange the order of quantifiers paying the price of a functional) and the existence of a prenex normal form presentation for every logical formula. Building up from Hofstra's earlier fibrational characterization of the de Paiva's categorical Dialectica construction, we show that a fibration is an instance of the Dialectica construction if and only if it is a Gödel fibration. This result establishes an internal presentation of the dialectica construction. Then we provide a deep structural analysis of the Dialectica construction producing a full description of which categorical structure behaves well with respect to this construction, focusing on (weak) finite products and coproducts. We conclude describing the applications we envisage for this generalized fibrational version of the Dialectica construction.

Despite the advances in Natural Language Inference through the training of massive deep models, recent work has revealed the generalization difficulties of such models, which fail to perform on adversarial datasets with challenging linguistic phenomena.Such phenomena, however, can be handled well by symbolic systems.Thus, we propose Hy-NLI, a hybrid system that learns to identify an NLI pair as linguistically challenging or not.Based on that, it uses its symbolic or deep learning component, respectively, to make the final inference decision.We show how linguistically less complex cases are best solved by robust state-of-the-art models, like BERT and XLNet, while hard linguistic phenomena are best handled by our implemented symbolic engine.Our thorough evaluation shows that our hybrid system achieves state-of-the-art performance across mainstream and adversarial datasets and opens the way for further research into the hybrid direction.

Abstract Full intuitionistic linear logic (FILL) was first introduced by Hyland and de Paiva, and went against current beliefs that it was not possible to incorporate all of the linear connectives, e.g. tensor, par and implication, into an intuitionistic linear logic. Bierman showed that their formalization of FILL did not enjoy cut elimination as such, but Bellin proposed a small change to the definition of FILL regaining cut elimination and using proof nets. In this note we adopt Bellin’s proposed change and give a direct proof of cut elimination for the sequent calculus. Then we show that a categorical model of FILL in the basic dialectica category is also a linear/non-linear model of Benton and a full tensor model of Melliès’ and Tabareau’s tensorial logic. We give a double-negation translation of linear logic into FILL that explicitly uses par in addition to tensor. Lastly, we introduce a new library to be used in the proof assistant Agda for proving properties of dialectica categories.

Lexical resources need to be as complete as possible.Very little work seems to have been done on adverbs, the smallest part of speech class in Princeton WordNet counting the number of synsets.Amongst adverbs, manner adverbs ending in '-ly' seem the easiest to work with, as their meaning is almost the same as the one of the associated adjective.This phenomenon seems to be parallel in English and Portuguese, where these manner adverbs finish in the suffix '-mente'.We use this correspondence to improve the coverage of adverbs in the lexical resource OpenWordNet-PT, a wordnet for Portuguese.

This work investigates legal concepts and their expression in Portuguese, concentrating on the “Order of Attorneys of Brazil” Bar exam. Using a corpus formed by a collection of multiple-choice questions, three norms related to the Ethics part of the OAB exam, language resources (Princeton WordNet and OpenWordNet-PT) and tools (AntConc and Freeling), we began to investigate the concepts and words missing from our repertory of concepts and words in Portuguese, the knowledge base OpenWordNet-PT. We add these concepts and words to OpenWordNet-PT and hence obtain a representation of these texts that is mostly “contained” in the lexical knowledge base.

This paper describes work extending Princeton WordNet to the domain of geological texts, associated with the time periods of the geological eras of the Earth History.We intend this extension to be considered as an example for any other domain extension that we might want to pursue.To provide this extension, we first produce a textual version of Princeton WordNet.Then we map a fragment of the International Commission on Stratigraphy (ICS) ontologies to WordNet and create the appropriate new synsets.We check the extended ontology on a small corpus of sentences from Gas and Oil technical reports and realize that more work needs to be done, as we need new words, new senses and new compounds in our extended WordNet.

The series of workshops on Intuitionistic Modal Logic and Applications (IMLA) owes its existence to the hope that philosophers, mathematical logicians and computer scientists would share information and tools when investigating intuitionistic modal logics and modal type theories, if they knew of each other's work. More than 10 years have passed since the retrospective view of de Paiva et al. [ 10 ], and progress in the area of constructive modal logic has been slow and getting slower. It is our view that differences in the outlook of the various groups of scholars interested in the topic, differences that were once fruitful, now are responsible for a tendency for the new work to be driven by technical issues that have not had wide interest, leading to compartmentalization and waning interest in the IMLA big tent. Work on modal type theories seems to have been pursued in narrow tracts. For instance, much work in the symposium on Principles of Programming Languages (POPL), in specific type systems could be considered work in applied constructive modal logic, but it is not considered so, as this perspective is not considered useful or productive. Generally speaking, topic specialists have stopped expecting outsiders to say anything of interest to them, so they do not make the effort to say anything of interest to outsiders.

Semantic relations between words are key to building systems that aim to understand and manipulate language.For English, the "de facto" standard for representing this kind of knowledge is Princeton's WordNet.Here, we describe the wordnet-like resources currently available for Portuguese: their origins, methods of creation, sizes, and usage restrictions.We start tackling the problem of comparing them, but only in quantitative terms.Finally, we sketch ideas for potential collaboration between some of the projects that produce Portuguese wordnets.

Our paper is actually two contributions in one. First, we argue that IBM's Jeopardy! playing machine needs a formal semantics. We present several arguments as we discuss the system. We also situate the work in the broader context of contemporary AI. Our second point is that the work in this area might well be done as a broad collaborative project. Hence our "Blue Sky'' contribution is a proposal to organize a polymath-style effort aimed at developing formal tools for the study of state of the art question-answer systems, and other large scale NLP efforts whose architectures and algorithms lack a theoretical foundation.

This paper presents NomLex-BR, a lexical resource describing Brazilian Portuguese nominalizations, and its integration with OpenWordnet-PT.We first describe the original English NOMLEX lexical resource and how we used it to bootstrap a Portuguese version.Subsequently, we describe how this lexicon can be embedded into OpenWordnet-PT, which facilitates its use and helps spot-checking both the bigger integrated resource and the original lexicon.Lastly, we outline some of the other, more substantial work that we plan to engage for the project of using linguistic insights for knowledge representation in Portuguese.

This paper presents OpenWordNet-PT, a freely available open-source wordnet for Portuguese, with its latest developments and practical uses.We provide a detailed description of the RDF representation developed for OpenWordnet-PT.We highlight our efforts to extend the coverage of our resource and add nominalization relations connecting nouns and verbs.Finally, we present several real-world applications where OpenWordnet-PT was put to use, including a large-scale high-throughput sentiment analysis system.

This paper briefly shows how Intuitionistic Description Logic can be considered a good alternative to classical ALC as far as formalizing legal knowledge is concerned.

Deverbal nouns pose serious challenges for knowledge-representation systems. We present a method of canonicalizing deverbal noun representations, relying on a rich lexicon of verb subcategorization frames, the WordNet database, a large finite-state network for derivational morphology and a series of heuristics for mapping deverbal arguments onto the arguments of corresponding verbs.1

1PARC, CA, USA 2ANU, Australia 3University of Bamberg, Germany

Valeria de Paiva, Rajeev Goré, Michael Mendler; Forthcoming Papers, Journal of Logic and Computation, Volume 14, Issue 4, 1 August 2004, Pages 621–622, https://

We discuss the treatment of prevention statements in both natural language semantics and knowledge representation, with particular regard to existence entailments. First order representations with an explicit existence predicate are shown to not adequately capture the entailments of prevention statements. A linguistic analysis is framed in a higher order intensional logic, employing a Fregean notion of existence as instantiation of a concept. We discuss how this can be mapped to a Cyc style knowledge representation.

Moggi's computational lambda calculus is a metalanguage for denotational semantics which arose from the observation that many different notions of computation have the categorical structure of a strong monad on a cartesian closed category. In this paper we show that the computational lambda calculus also arises naturally as the term calculus corresponding (by the Curry–Howard correspondence) to a novel intuitionistic modal propositional logic. We give natural deduction, sequent calculus and Hilbert-style presentations of this logic and prove strong normalisation and confluence results.