# Benchmarking Theorems of Implicational Linear Logic

### by Dr. Valeria de Paiva

- When: Friday, 10/02/2020, between 1pm and 2pm, EDT
- Where: Zoom; Outside guests please RSVP by emailing Harley Eades
- YouTube Recording: https://youtu.be/rgJES5O6THY

#### Abstract

Benchmarking automated theorem proving (ATP) systems using
standardized problem sets is a well-established method for measuring
their performance. The availability of such libraries of problems for
non-classical logics is very limited. So in our first work (with
Olarte, Pimentel, and Reis FLoC2018) we proposed a library for
benchmarking Girard’s (propositional) intuitionistic linear logic,
starting from Kleene’s initial collection. However, we want to use
these theorems not for checking the efficiency of different theorem
provers, but instead to investigate the structure of the space of
proofs of linear theorems, in different variants of linear
logic. Having learned of Tarau’s work on ‘generating’ intuitionistic
implication theorems, I suggested to him that we calculate the
*linear* implicational theorems. His program turned out to be very
adept and in a few hours produces almost 8 billion “small”
theorems. Given this economy of scale, we’re hoping to do some machine
learning of intuitionistic and linear logic, in the near future. (This
work was presented by Paul Tarau in ICLP2020, Sept 2020.)

#### Bio

Valeria de Paiva is a mathematician and computer scientist based in Cupertino, CA. She’s working on a ‘stealth’ start-up in Berkeley, the Topos Institute, while ‘visiting’ the Department of Informatica, PUC-Rio de Janeiro. She worked as a Principal Scientist at Samsung Research America, and as a senior applied scientist at Nuance Communications, Sunnyvale, CA. Earlier she was at Rearden Commerce and she was a search analyst at Cuil, Inc. in Menlo Park, CA. Before that, she was a research scientist at the Intelligent Systems Laboratory of PARC (Palo Alto Research Center), California (2000-2008). She received her Ph.D. in Mathematics from Cambridge University in 1988 for work on “Dialectica Categories”, under Martin Hyland’s supervision, and has ever since worked on logical approaches to computation, especially using Category Theory.