Benchmarking Theorems of Implicational Linear Logic

by Dr. Valeria de Paiva

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.

School of Computer and Cyber Sciences Augusta University