-
Skolem, Gödel, and Hilbert fibrations
Authors:
Davide Trotta,
Jonathan Weinberger,
Valeria de Paiva
Abstract:
Grothendieck fibrations are fundamental in capturing the concept of dependency, notably in categorical semantics of type theory and programming languages. A relevant instance are Dialectica fibrations which generalise Gödel's Dialectica proof interpretation and have been widely studied in recent years.
We characterise when a given fibration is a generalised, dependent Dialectica fibration, namel…
▽ More
Grothendieck fibrations are fundamental in capturing the concept of dependency, notably in categorical semantics of type theory and programming languages. A relevant instance are Dialectica fibrations which generalise Gödel's Dialectica proof interpretation and have been widely studied in recent years.
We characterise when a given fibration is a generalised, dependent Dialectica fibration, namely an iterated completion of a fibration by dependent products and sums (along a given class of display maps). From a technical perspective, we complement the work of Hofstra on Dialectica fibrations by an internal viewpoint, categorifying the classical notion of quantifier-freeness. We also generalise both Hofstra's and Trotta et al.'s work on Gödel fibrations to the dependent case, replacing the class of cartesian projections in the base category by arbitrary display maps. We discuss how this recovers a range of relevant examples in categorical logic and proof theory. Moreover, as another instance, we introduce Hilbert fibrations, providing a categorical understanding of Hilbert's $ε$- and $τ$-operators well-known from proof theory.
△ Less
Submitted 12 August, 2024; v1 submitted 22 July, 2024;
originally announced July 2024.
-
Mathematical Entities: Corpora and Benchmarks
Authors:
Jacob Collard,
Valeria de Paiva,
Eswaran Subrahmanian
Abstract:
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 fu…
▽ More
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.
△ Less
Submitted 17 June, 2024;
originally announced June 2024.
-
Towards a Brazilian History Knowledge Graph
Authors:
Valeria de Paiva,
Alexandre Rademaker
Abstract:
This short paper describes the first steps in a project to construct a knowledge graph for Brazilian history based on the Brazilian Dictionary of Historical Biographies (DHBB) and Wikipedia/Wikidata. We contend that large repositories of Brazilian-named entities (people, places, organizations, and political events and movements) would be beneficial for extracting information from Portuguese texts.…
▽ More
This short paper describes the first steps in a project to construct a knowledge graph for Brazilian history based on the Brazilian Dictionary of Historical Biographies (DHBB) and Wikipedia/Wikidata. We contend that large repositories of Brazilian-named entities (people, places, organizations, and political events and movements) would be beneficial for extracting information from Portuguese texts. We show that many of the terms/entities described in the DHBB do not have corresponding concepts (or Q items) in Wikidata, the largest structured database of entities associated with Wikipedia. We describe previous work on extracting information from the DHBB and outline the steps to construct a Wikidata-based historical knowledge graph.
△ Less
Submitted 28 March, 2024;
originally announced March 2024.
-
MathGloss: Building mathematical glossaries from text
Authors:
Lucy Horowitz,
Valeria de Paiva
Abstract:
MathGloss is a project to create a knowledge graph (KG) for undergraduate mathematics from text, automatically, using modern natural language processing (NLP) tools and resources already available on the web. MathGloss is a linked database of undergraduate concepts in mathematics. So far, it combines five resources: (i) Wikidata, a collaboratively edited, multilingual knowledge graph hosted by the…
▽ More
MathGloss is a project to create a knowledge graph (KG) for undergraduate mathematics from text, automatically, using modern natural language processing (NLP) tools and resources already available on the web. MathGloss is a linked database of undergraduate concepts in mathematics. So far, it combines five resources: (i) Wikidata, a collaboratively edited, multilingual knowledge graph hosted by the Wikimedia Foundation, (ii) terms covered in mathematics courses at the University of Chicago, (iii) the syllabus of the French undergraduate mathematics curriculum which includes hyperlinks to the automated theorem prover Lean 4, (iv) MuLiMa, a multilingual dictionary of mathematics curated by mathematicians, and (v) the nLab, a wiki for category theory also curated by mathematicians. MathGloss's goal is to bring together resources for learning mathematics and to allow every mathematician to tailor their learning to their own preferences. Moreover, by organizing different resources for learning undergraduate mathematics alongside those for learning formal mathematics, we hope to make it easier for mathematicians and formal tools (theorem provers, computer algebra systems, etc) experts to "understand" each other and break down some of the barriers to formal math.
△ Less
Submitted 21 November, 2023;
originally announced November 2023.
-
Extracting Mathematical Concepts with Large Language Models
Authors:
Valeria de Paiva,
Qiyue Gao,
Pavel Kovalev,
Lawrence S. Moss
Abstract:
We extract mathematical concepts from mathematical text using generative large language models (LLMs) like ChatGPT, contributing to the field of automatic term extraction (ATE) and mathematical text processing, and also to the study of LLMs themselves. Our work builds on that of others in that we aim for automatic extraction of terms (keywords) in one mathematical field, category theory, using as…
▽ More
We extract mathematical concepts from mathematical text using generative large language models (LLMs) like ChatGPT, contributing to the field of automatic term extraction (ATE) and mathematical text processing, and also to the study of LLMs themselves. Our work builds on that of others in that we aim for automatic extraction of terms (keywords) in one mathematical field, category theory, using as a corpus the 755 abstracts from a snapshot of the online journal "Theory and Applications of Categories", circa 2020. Where our study diverges from previous work is in (1) providing a more thorough analysis of what makes mathematical term extraction a difficult problem to begin with; (2) paying close attention to inter-annotator disagreements; (3) providing a set of guidelines which both human and machine annotators could use to standardize the extraction process; (4) introducing a new annotation tool to help humans with ATE, applicable to any mathematical field and even beyond mathematics; (5) using prompts to ChatGPT as part of the extraction process, and proposing best practices for such prompts; and (6) raising the question of whether ChatGPT could be used as an annotator on the same level as human experts. Our overall findings are that the matter of mathematical ATE is an interesting field which can benefit from participation by LLMs, but LLMs themselves cannot at this time surpass human performance on it.
△ Less
Submitted 29 August, 2023;
originally announced September 2023.
-
Parmesan: mathematical concept extraction for education
Authors:
Jacob Collard,
Valeria de Paiva,
Eswaran Subrahmanian
Abstract:
Mathematics is a highly specialized domain with its own unique set of challenges that has seen limited study in natural language processing. However, mathematics is used in a wide variety of fields and multidisciplinary research in many different domains often relies on an understanding of mathematical concepts. To aid researchers coming from other fields, we develop a prototype system for searchi…
▽ More
Mathematics is a highly specialized domain with its own unique set of challenges that has seen limited study in natural language processing. However, mathematics is used in a wide variety of fields and multidisciplinary research in many different domains often relies on an understanding of mathematical concepts. To aid researchers coming from other fields, we develop a prototype system for searching for and defining mathematical concepts in context, focusing on the field of category theory. This system, Parmesan, depends on natural language processing components including concept extraction, relation extraction, definition extraction, and entity linking. In developing this system, we show that existing techniques cannot be applied directly to the category theory domain, and suggest hybrid techniques that do perform well, though we expect the system to evolve over time. We also provide two cleaned mathematical corpora that power the prototype system, which are based on journal articles and wiki pages, respectively. The corpora have been annotated with dependency trees, lemmas, and part-of-speech tags.
△ Less
Submitted 17 July, 2023; v1 submitted 13 July, 2023;
originally announced July 2023.
-
Extracting Blockchain Concepts from Text
Authors:
Rodrigo Veiga,
Markus Endler,
Valeria de Paiva
Abstract:
Blockchains provide a mechanism through which mutually distrustful remote parties can reach consensus on the state of a ledger of information. With the great acceleration with which this space is developed, the demand for those seeking to learn about blockchain also grows. Being a technical subject, it can be quite intimidating to start learning. For this reason, the main objective of this project…
▽ More
Blockchains provide a mechanism through which mutually distrustful remote parties can reach consensus on the state of a ledger of information. With the great acceleration with which this space is developed, the demand for those seeking to learn about blockchain also grows. Being a technical subject, it can be quite intimidating to start learning. For this reason, the main objective of this project was to apply machine learning models to extract information from whitepapers and academic articles focused on the blockchain area to organize this information and aid users to navigate the space.
△ Less
Submitted 6 May, 2023;
originally announced May 2023.
-
Extracting Mathematical Concepts from Text
Authors:
Jacob Collard,
Valeria de Paiva,
Brendan Fong,
Eswaran Subrahmanian
Abstract:
We investigate different systems for extracting mathematical entities from English texts in the mathematical field of category theory as a first step for constructing a mathematical knowledge graph. We consider four different term extractors and compare their results. This small experiment showcases some of the issues with the construction and evaluation of terms extracted from noisy domain text.…
▽ More
We investigate different systems for extracting mathematical entities from English texts in the mathematical field of category theory as a first step for constructing a mathematical knowledge graph. We consider four different term extractors and compare their results. This small experiment showcases some of the issues with the construction and evaluation of terms extracted from noisy domain text. We also make available two open corpora in research mathematics, in particular in category theory: a small corpus of 755 abstracts from the journal TAC (3188 sentences), and a larger corpus from the nLab community wiki (15,000 sentences).
△ Less
Submitted 29 August, 2022;
originally announced August 2022.
-
Categorifying computable reducibilities
Authors:
Davide Trotta,
Manlio Valenti,
Valeria de Paiva
Abstract:
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…
▽ More
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.
△ Less
Submitted 21 September, 2024; v1 submitted 18 August, 2022;
originally announced August 2022.
-
Dialectica Principles via Gödel Doctrines
Authors:
Davide Trotta,
Matteo Spadetto,
Valeria de Paiva
Abstract:
Gödel's Dialectica interpretation was conceived as a tool to obtain the consistency of Peano arithmetic via a proof of consistency of Heyting arithmetic in the 40s. In recent years, several proof-theoretic transformations, based on Gödel's Dialectica interpretation, have been used systematically to extract new content from classical proofs, following a suggestion of Kreisel. Thus, the interpretati…
▽ More
Gödel's Dialectica interpretation was conceived as a tool to obtain the consistency of Peano arithmetic via a proof of consistency of Heyting arithmetic in the 40s. In recent years, several proof-theoretic transformations, based on Gödel's Dialectica interpretation, have been used systematically to extract new content from classical proofs, following a suggestion of Kreisel. Thus, the interpretation has found new relevant applications in several areas of mathematics and computer science. Several authors have explained the Dialectica interpretation in categorical terms. In our previous work, we introduced an intrinsic categorical presentation of the Dialectica construction via a generalisation of Hofstra's work, using the notion of Gödel fibration and its proof-irrelevant version, a Gödel doctrine. The key idea is that Gödel fibrations can be thought of as fibrations generated by some basic elements playing the role of quantifier-free elements. This categorification of quantifier-free elements is crucial not only to show that our notion of Gödel fibration is equivalent to Hofstra's Dialectica fibration in the appropriate way, but also to show how Gödel doctrines embody the main logical features of the Dialectica Interpretation. To show that, we derive the soundness of the interpretation of the implication connective, as expounded by 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 correspondence between the logical system and the categorical framework. Finally, to complete our analysis, we characterise categories obtained as results of the tripos-to-topos of Hyland, Johnstone and Pitts applied to Gödel doctrines.
△ Less
Submitted 14 May, 2022;
originally announced May 2022.
-
Proceedings Second Joint International Workshop on Linearity & Trends in Linear Logic and Applications
Authors:
Ugo Dal Lago,
Valeria de Paiva
Abstract:
This volume contains a selection of papers presented at Linearity&TLLA 2020, namely the Second Joint International Workshop on Linearity & Trends in Linear Logic and Applications, held on June 29-30, 2020 online. (The workshop was supposed to take place in Paris as part of FSCD 2020, but due to the COVID pandemic it was decided not to hold the event live.) Linearity is a central concept in many th…
▽ More
This volume contains a selection of papers presented at Linearity&TLLA 2020, namely the Second Joint International Workshop on Linearity & Trends in Linear Logic and Applications, held on June 29-30, 2020 online. (The workshop was supposed to take place in Paris as part of FSCD 2020, but due to the COVID pandemic it was decided not to hold the event live.) Linearity is a central concept in many theoretical and practical approaches to computer science. On the theoretical side, there is much work stemming from linear logic and dealing with resource control, complexity classes, and more recently quantum computation. On the practical side there is certainly work on program analysis, operational semantics, logic programming languages, program transformations, and efficient implementation techniques. Linear logic is not only a theoretical tool for the analysis of resource usage in logic and computation. It is also a corpus of distinct approaches and methodologies (e.g., proof nets, geometry of interaction, coherent spaces, relational models) that were originally developed for the study of linear logic's syntax and semantics have nowadays found applications in several other fields.
△ Less
Submitted 28 December, 2021;
originally announced December 2021.
-
Dialectica Logical Principles
Authors:
Davide Trotta,
Matteo Spadetto,
Valeria de Paiva
Abstract:
Gödel's Dialectica interpretation was designed to obtain a relative consistency proof for Heyting arithmetic, to be used in conjunction with the double negation interpretation to obtain the consistency of Peano arithmetic. In recent years, proof theoretic transformations (so-called proof interpretations) that are based on Gödel's Dialectica interpretation have been used systematically to extract n…
▽ More
Gödel's Dialectica interpretation was designed to obtain a relative consistency proof for Heyting arithmetic, to be used in conjunction with the double negation interpretation to obtain the consistency of Peano arithmetic. In recent years, proof theoretic transformations (so-called proof interpretations) that are 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 characterisation of the Dialectica which corresponds exactly to the logical description of the interpretation. To show that we derive in the category theory the soundness of the interpretation of the implication connective, as expounded on by Spector and Troelstra. This requires extra logical principles, going beyond intuitionistic logic, Markov's Principle (MP) and the Independence of Premise (IP) 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. This tight correspondence should come handy not only when discussing the applications of the Dialectica already known, like its use to extract computational content from (some) classical theorems (proof mining), its use to help to model specific abstract machines, etc. but also to help devise new applications.
△ Less
Submitted 16 September, 2021;
originally announced September 2021.
-
Kolmogorov-Veloso Problems and Dialectica Categories
Authors:
Valeria de Paiva,
Samuel G. da Silva
Abstract:
We investigate the categorical connection between Dialectica constructions, Kolmogorov problems, Veloso problems and Blass problems. We show that the work of Kolmogorov can be regarded as a bridge between Veloso's abstract notion of a problem and the conceptual problems Blass discussed in his questions-and-answers framework. This bridge can be seen by means of the categorical Dialectica constructi…
▽ More
We investigate the categorical connection between Dialectica constructions, Kolmogorov problems, Veloso problems and Blass problems. We show that the work of Kolmogorov can be regarded as a bridge between Veloso's abstract notion of a problem and the conceptual problems Blass discussed in his questions-and-answers framework. This bridge can be seen by means of the categorical Dialectica constructions introduced in de Paiva's dissertation and reformulated by da Silva to account for set-theoretical foundational assumptions. The use of categorical concepts allows us to provide several examples, connecting extremely different areas of mathematics, and using simple methods. This paper also shows that while Blass and Kolmogorov notions of problem can be investigated using the Zermelo-Fraenkel (ZF) set-theoretical framework, Veloso problems require the Axiom of Choice (AC). Moreover, weaker notions of choice (dependent choice and countable choice) can also be accounted for in the problems' framework.
△ Less
Submitted 16 February, 2022; v1 submitted 16 July, 2021;
originally announced July 2021.
-
Dialectica Petri Nets
Authors:
Elena Di Lavore,
Wilmer Leal,
Valeria de Paiva
Abstract:
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 r…
▽ More
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.
△ Less
Submitted 14 February, 2024; v1 submitted 26 May, 2021;
originally announced May 2021.
-
The Gödel Fibration
Authors:
Davide Trotta,
Matteo Spadetto,
Valeria de Paiva
Abstract:
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 D…
▽ More
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.
△ Less
Submitted 28 April, 2021;
originally announced April 2021.
-
Deriving Theorems in Implicational Linear Logic, Declaratively
Authors:
Paul Tarau,
Valeria de Paiva
Abstract:
The problem we want to solve is how to generate all theorems of a given size in the implicational fragment of propositional intuitionistic linear logic. We start by filtering for linearity the proof terms associated by our Prolog-based theorem prover for Implicational Intuitionistic Logic. This works, but using for each formula a PSPACE-complete algorithm limits it to very small formulas. We take…
▽ More
The problem we want to solve is how to generate all theorems of a given size in the implicational fragment of propositional intuitionistic linear logic. We start by filtering for linearity the proof terms associated by our Prolog-based theorem prover for Implicational Intuitionistic Logic. This works, but using for each formula a PSPACE-complete algorithm limits it to very small formulas. We take a few walks back and forth over the bridge between proof terms and theorems, provided by the Curry-Howard isomorphism, and derive step-by-step an efficient algorithm requiring a low polynomial effort per generated theorem. The resulting Prolog program runs in O(N) space for terms of size N and generates in a few hours 7,566,084,686 theorems in the implicational fragment of Linear Intuitionistic Logic together with their proof terms in normal form. As applications, we generate datasets for correctness and scalability testing of linear logic theorem provers and training data for neural networks working on theorem proving challenges. The results in the paper, organized as a literate Prolog program, are fully replicable.
Keywords: combinatorial generation of provable formulas of a given size, intuitionistic and linear logic theorem provers, theorems of the implicational fragment of propositional linear intuitionistic logic, Curry-Howard isomorphism, efficient generation of linear lambda terms in normal form, Prolog programs for lambda term generation and theorem proving.
△ Less
Submitted 21 September, 2020;
originally announced September 2020.
-
Dialectica Fuzzy Petri Nets
Authors:
Valeria de Paiva,
Apostolos Syropoulos
Abstract:
Brown and Gurr have introduced a model of Petri Nets that is based on de~Paiva's Dialectica categories. This model was refined in an unpublished technical report, where Petri nets with multiplicities, instead of {\em elementary} nets (i.e., nets with multiplicities zero and one only) were considered. In this note we expand this modelling to deal with {\em fuzzy} petri nets. The basic idea is to us…
▽ More
Brown and Gurr have introduced a model of Petri Nets that is based on de~Paiva's Dialectica categories. This model was refined in an unpublished technical report, where Petri nets with multiplicities, instead of {\em elementary} nets (i.e., nets with multiplicities zero and one only) were considered. In this note we expand this modelling to deal with {\em fuzzy} petri nets. The basic idea is to use as the dualizing object in the Dialectica categories construction, the unit interval that has all the properties of a {\em lineale} structure.
△ Less
Submitted 8 March, 2020;
originally announced March 2020.
-
Existence, multiplicity and regularity for a Schrödinger equation with magnetic potential involving sign-changing weight function
Authors:
Francisco Odair Vieira de Paiva,
Sandra Machado de Souza Lima,
Olimpio Hiroshi Miyagaki
Abstract:
In this paper we consider the following class of elliptic problems $$- Δ_A u + u = a_λ(x) |u|^{q-2}u+b_μ(x) |u|^{p-2}u ,\,\, x\in \mathbb{R}^N$$ where $1<q<2<p<2^*-1= \frac{N+2}{N-2}$, $a_λ(x)$ is a sign-changing weight function, $b_μ(x)$ have some aditional conditions, $u \in H^1_A(\mathbb{R}^N)$ and $A:\mathbb{R}^N \rightarrow\mathbb{R}^N$ is a magnetic potential. Exploring the relationship betw…
▽ More
In this paper we consider the following class of elliptic problems $$- Δ_A u + u = a_λ(x) |u|^{q-2}u+b_μ(x) |u|^{p-2}u ,\,\, x\in \mathbb{R}^N$$ where $1<q<2<p<2^*-1= \frac{N+2}{N-2}$, $a_λ(x)$ is a sign-changing weight function, $b_μ(x)$ have some aditional conditions, $u \in H^1_A(\mathbb{R}^N)$ and $A:\mathbb{R}^N \rightarrow\mathbb{R}^N$ is a magnetic potential. Exploring the relationship between the Nehari manifold and fibering maps, we will discuss the existence, multiplicity and regularity of solutions.
△ Less
Submitted 15 April, 2019;
originally announced April 2019.
-
The ILLTP Library for Intuitionistic Linear Logic
Authors:
Carlos Olarte,
Valeria de Paiva,
Elaine Pimentel,
Giselle Reis
Abstract:
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, an…
▽ More
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.
△ Less
Submitted 15 April, 2019;
originally announced April 2019.
-
On the Lambek Calculus with an Exchange Modality
Authors:
Jiaming Jiang,
Harley Eades III,
Valeria de Paiva
Abstract:
In this paper we introduce Commutative/Non-Commutative Logic (CNC logic) and two categorical models for CNC logic. This work abstracts Benton's Linear/Non-Linear Logic by removing the existence of the exchange structural rule. One should view this logic as composed of two logics; one sitting to the left of the other. On the left, there is intuitionistic linear logic, and on the right is a mixed co…
▽ More
In this paper we introduce Commutative/Non-Commutative Logic (CNC logic) and two categorical models for CNC logic. This work abstracts Benton's Linear/Non-Linear Logic by removing the existence of the exchange structural rule. One should view this logic as composed of two logics; one sitting to the left of the other. On the left, there is intuitionistic linear logic, and on the right is a mixed commutative/non-commutative formalization of the Lambek calculus. Then both of these logics are connected via a pair of monoidal adjoint functors. An exchange modality is then derivable within the logic using the adjunction between both sides. Thus, the adjoint functors allow one to pull the exchange structural rule from the left side to the right side. We then give a categorical model in terms of a monoidal adjunction, and then a concrete model in terms of dialectica Lambek spaces.
△ Less
Submitted 15 April, 2019;
originally announced April 2019.
-
Existence and multiplicity results for a class of non-linear Schrödinger equations with magnetic potential involving sign-changing non linearity
Authors:
Francisco Odair Vieira de Paiva,
Sandra Machado de Souza Lima,
Olimpio Hiroshi Miyagaki
Abstract:
In this work we consider the following class of elliptic problems $$- Δ_A u + u = a(x) |u|^{q-2}u+b(x) |u|^{p-2}u , \mbox{ in } \mathbb{R}^N, $$ $u\in H^1_A (\mathbb{R}^N)$, with $2<q<p<2^*= \frac{2N}{N-2}$, $a(x)$ and $b(x)$ are functions that can change signal and satisfy some additional conditions; $u \in H^1_A(\mathbb{R}^N)$ and $A:\mathbb{R}^N \rightarrow \mathbb{R}^N$ is a magnetic potential…
▽ More
In this work we consider the following class of elliptic problems $$- Δ_A u + u = a(x) |u|^{q-2}u+b(x) |u|^{p-2}u , \mbox{ in } \mathbb{R}^N, $$ $u\in H^1_A (\mathbb{R}^N)$, with $2<q<p<2^*= \frac{2N}{N-2}$, $a(x)$ and $b(x)$ are functions that can change signal and satisfy some additional conditions; $u \in H^1_A(\mathbb{R}^N)$ and $A:\mathbb{R}^N \rightarrow \mathbb{R}^N$ is a magnetic potential. Also using the Nehari method in combination with other complementary arguments, we discuss the existence of infinite solutions to the problem in question, varying the assumptions about the weight functions.
△ Less
Submitted 12 April, 2019;
originally announced April 2019.
-
Existence at least four solutions for a Schrödinger equation with magnetic potential involving sign-changing weight function
Authors:
Francisco Odair Vieira de Paiva,
Sandra Machado de Souza Lima,
Olimpio Hiroshi Miyagaki
Abstract:
In this paper we consider the following class of elliptic problems $$- Δ_A u + u = a_λ(x) |u|^{q-2}u+b_μ(x) |u|^{p-2}u ,$$ for $x \in \mathbb{R}^N$, $1<q<2<p<2^*-1= \frac{N+2}{N-2}$, $a_λ(x)$ is a sign-changing weight function, $b_μ(x)$ has some aditional conditions, $u \in H^1_A(\mathbb{R}^N)$ and $A:\mathbb{R}^N \rightarrow\mathbb{R}^N$ is a magnetic potential. Exploring the Bahri Li argument an…
▽ More
In this paper we consider the following class of elliptic problems $$- Δ_A u + u = a_λ(x) |u|^{q-2}u+b_μ(x) |u|^{p-2}u ,$$ for $x \in \mathbb{R}^N$, $1<q<2<p<2^*-1= \frac{N+2}{N-2}$, $a_λ(x)$ is a sign-changing weight function, $b_μ(x)$ has some aditional conditions, $u \in H^1_A(\mathbb{R}^N)$ and $A:\mathbb{R}^N \rightarrow\mathbb{R}^N$ is a magnetic potential. Exploring the Bahri Li argument and some preliminar results we will discuss the existence of four solution to the problem in question.
△ Less
Submitted 12 April, 2019;
originally announced April 2019.
-
Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications
Authors:
Thomas Ehrhard,
Maribel Fernández,
Valeria de Paiva,
Lorenzo Tortora de Falco
Abstract:
This volume contains a selection of papers presented at Linearity/TLLA 2018: Joint Linearity and TLLA workshops (part of FLOC 2018) held on July 7-8, 2018 in Oxford. Linearity has been a key feature in several lines of research in both theoretical and practical approaches to computer science. On the theoretical side there is much work stemming from linear logic dealing with proof technology, compl…
▽ More
This volume contains a selection of papers presented at Linearity/TLLA 2018: Joint Linearity and TLLA workshops (part of FLOC 2018) held on July 7-8, 2018 in Oxford. Linearity has been a key feature in several lines of research in both theoretical and practical approaches to computer science. On the theoretical side there is much work stemming from linear logic dealing with proof technology, complexity classes and more recently quantum computation. On the practical side there is work on program analysis, expressive operational semantics for programming languages, linear programming languages, program transformation, update analysis and efficient implementation techniques. Linear logic is not only a theoretical tool to analyse the use of resources in logic and computation. It is also a corpus of tools, approaches, and methodologies (proof nets, exponential decomposition, geometry of interaction, coherent spaces, relational models, etc.) that were originally developed for the study of linear logic's syntax and semantics and are nowadays applied in several other fields.
△ Less
Submitted 12 April, 2019;
originally announced April 2019.
-
Linguistic Legal Concept Extraction in Portuguese
Authors:
Alessandra Cid,
Alexandre Rademaker,
Bruno Cuconato,
Valeria de Paiva
Abstract:
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 m…
▽ More
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 "contained" in the lexical knowledge base.
△ Less
Submitted 22 October, 2018;
originally announced October 2018.
-
Dialectica Categories for the Lambek Calculus
Authors:
Valeria de Paiva,
Harley Eades III
Abstract:
We revisit the old work of de Paiva on the models of the Lambek Calculus in dialectica models making sure that the syntactic details that were sketchy on the first version got completed and verified. We extend the Lambek Calculus with a κmodality, inspired by Yetter's work, which makes the calculus commutative. Then we add the of-course modality !, as Girard did, to re-introduce weakening and cont…
▽ More
We revisit the old work of de Paiva on the models of the Lambek Calculus in dialectica models making sure that the syntactic details that were sketchy on the first version got completed and verified. We extend the Lambek Calculus with a κmodality, inspired by Yetter's work, which makes the calculus commutative. Then we add the of-course modality !, as Girard did, to re-introduce weakening and contraction for all formulas and get back the full power of intuitionistic and classical logic. We also present the categorical semantics, proved sound and complete. Finally we show the traditional properties of type systems, like subject reduction, the Church-Rosser theorem and normalization for the calculi of extended modalities, which we did not have before.
△ Less
Submitted 21 January, 2018;
originally announced January 2018.
-
Proceedings of the LexSem+Logics Workshop 2016
Authors:
Steven Neale,
Valeria de Paiva,
Arantxa Otegi,
Alexandre Rademaker
Abstract:
Lexical semantics continues to play an important role in driving research directions in NLP, with the recognition and understanding of context becoming increasingly important in delivering successful outcomes in NLP tasks. Besides traditional processing areas such as word sense and named entity disambiguation, the creation and maintenance of dictionaries, annotated corpora and resources have becom…
▽ More
Lexical semantics continues to play an important role in driving research directions in NLP, with the recognition and understanding of context becoming increasingly important in delivering successful outcomes in NLP tasks. Besides traditional processing areas such as word sense and named entity disambiguation, the creation and maintenance of dictionaries, annotated corpora and resources have become cornerstones of lexical semantics research and produced a wealth of contextual information that NLP processes can exploit. New efforts both to link and construct from scratch such information - as Linked Open Data or by way of formal tools coming from logic, ontologies and automated reasoning - have increased the interoperability and accessibility of resources for lexical and computational semantics, even in those languages for which they have previously been limited.
LexSem+Logics 2016 combines the 1st Workshop on Lexical Semantics for Lesser-Resources Languages and the 3rd Workshop on Logics and Ontologies. The accepted papers in our program covered topics across these two areas, including: the encoding of plurals in Wordnets, the creation of a thesaurus from multiple sources based on semantic similarity metrics, and the use of cross-lingual treebanks and annotations for universal part-of-speech tagging. We also welcomed talks from two distinguished speakers: on Portuguese lexical knowledge bases (different approaches, results and their application in NLP tasks) and on new strategies for open information extraction (the capture of verb-based propositions from massive text corpora).
△ Less
Submitted 14 August, 2016;
originally announced August 2016.
-
ALPRS - A New Approach for License Plate Recognition using the Sift Algorithm
Authors:
Francisco Assis da Silva,
Almir Olivette Artero,
Maria Stela Veludo de Paiva,
Ricardo Luis Barbosa
Abstract:
This paper presents a new approach for the automatic license plate recognition, which includes the SIFT algorithm in step to locate the plate in the input image. In this new approach, besides the comparison of the features obtained with the SIFT algorithm, the correspondence between the spatial orientations and the positioning associated with the keypoints is also observed. Afterwards, an algorith…
▽ More
This paper presents a new approach for the automatic license plate recognition, which includes the SIFT algorithm in step to locate the plate in the input image. In this new approach, besides the comparison of the features obtained with the SIFT algorithm, the correspondence between the spatial orientations and the positioning associated with the keypoints is also observed. Afterwards, an algorithm is used for the character recognition of the plates, very fast, which makes it possible its application in real time. The results obtained with the proposed approach presented very good success rates, so much for locating the characters in the input image, as for their recognition.
△ Less
Submitted 7 March, 2013;
originally announced March 2013.
-
Fuzzy Topological Systems
Authors:
Apostolos Syropoulos,
Valeria de Paiva
Abstract:
Dialectica categories are a very versatile categorical model of linear logic. These have been used to model many seemingly different things (e.g., Petri nets and Lambek's calculus). In this note, we expand our previous work on fuzzy petri nets to deal with fuzzy topological systems. One basic idea is to use as the dualizing object in the Dialectica categories construction, the unit real interval […
▽ More
Dialectica categories are a very versatile categorical model of linear logic. These have been used to model many seemingly different things (e.g., Petri nets and Lambek's calculus). In this note, we expand our previous work on fuzzy petri nets to deal with fuzzy topological systems. One basic idea is to use as the dualizing object in the Dialectica categories construction, the unit real interval [0,1], which has all the properties of a {\em lineale}. The second basic idea is to generalize Vickers's notion of a topological system.
△ Less
Submitted 13 July, 2011;
originally announced July 2011.
