Projects

Valeria's photo
  • Network Mathematics. Working on 3 subprojects: Parmesan (DEMO http://www.jacobcollard.com/parmesan2/, PREPRINTS https://arxiv.org/abs/2307.06699, https://arxiv.org/abs/2208.13830, VIDEO https://www.youtube.com/watch?v=-ZhZjMn1Zpk), MathGloss (DEMO https://mathgloss.github.io/MathGloss/database, https://arxiv.org/abs/2311.12649, see also https://europroofnet.github.io/cambridge-2023/#horowitz) and MathChat https://arxiv.org/abs/2309.00642 (MathAnnotator https://gaoq111.github.io/math_concept_annotation/). 2020.
  • Entailment and Contradiction Detection (ECD) and Natural Language Inference (NLI). I worked for many years at Xerox's PARC on the Bridge project. Together with Katerina Kalouli and Dick Crouch we produced a new Bridge-like system, with free and open tools. This work can be seen at http://h2942521.stratoserver.net:8080/katerina.kalouli/resources.html. Some of this work has to do with lexical resources and connects to the work below. Some of it has to do with work with Gerard de Melo on an implicative lexicon. Some of it is more theorem proving and connects to work with Vivek Nigam. Some of it is really logic and it may connect to Linear Logic. 2012.
  • Lexical Portuguese Resources and OpenWordNet-PT. OpenWordNet-PT is a Portuguese wordnet we are building. The team includes Alexandre Rademaker, Gerard de Melo, Livy Real, Claudia Freitas and Fabricio Chalub, amongst others. The code is in GitHub and there is a browsable interface, http://openwordnet-pt.org. 2011.
  • Constructive Modal Logics and IMLA. Constructive Modal Logics are very underdeveloped in comparison to classical modal logics. Through the loose organization of several IMLA (Intuitionistic Modal Logics and Applications) workshops we are putting forward our approach, which is mostly based on the Curry-Howard interpretation. This includes work with Gavin Bierman, Nick Benton, Natasha Alechina, Eike Ritter, Michael Mendler, Neil Ghani, amongst others . 1999.
  • Categorical Structures for (Linear) Logic. For my thesis I worked on categorical models of Linear Logic, then a promising new logic touted for its applications to computing. My thesis uncovered a connection between linear logic and Goedel's Dialectica interpretation boosting linear logic's reputation and, at the same time, reminding logicians of Godel's ingenious way of proving relative consistency of arithmetic. Since then I have described many variants of Linear Logic: FILL(Hyland, Eades), DILL(Barber and Plotkin), ILT(Maietti and Ritter), etc. I have also applied new calculi (linear or not), e.g. FIL(Pereira), CS4(Alechina, Mendler), CK(Bellin, Ritter), IHL(Brauner), to modelling phenomena in Computing and Mathematics. 1990.