Abstract

It is possible to compute in which logics a given formula is deducible? The aim of this paper is to provide a formal basis to answer positively this question in the context of substructural logics. Such a basis is founded on structurally-free logic, a logic in which the usual structural rules are replaced by complex combinator rules, and thus constitute a generalization of traditional sequent systems.A family of substructural logics is identified by the set of structural rules admissible to all its members. Combinators encode the sequence of structural rules needed to prove a formula, thus representing the family of logics in which that formula is provable. In this setting, structurally-free theorem proving is a decision procedure that inputs a formula and outputs the corresponding combinator when the formula is deducible.We then present an algorithm to compute a combinator corresponding to a given formula in the fragment containing only the connective → and [otimes]. The algorithm is based on equestructural transformations, i.e. it transforms one sequent in a set of simpler sequents from which we can compute the combinator of the original sequent. We show that this algorithm is sound and complete and always terminates