Towards Structurally-Free Theorem Proving

Is it 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, structurallyfree 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 (if it exists) in the fragment containing only the connectives → and ⊗. T...

• Type: Journal
• Year: 1998
• Where: IGPL
• Authors: Marcelo Finger
• Keywords: IGPL 1998, Logics, Structural Rules, Substructural Logics