From Cut-free Calculi to Automated Deduction: The Case of Bounded Contraction
Electr. Notes Theor. Comput. Sci., Volume 332, 2017, Pages 75-93.
Abstract The addition of the bounded contraction rules to Full Lambek Calculus with exchange and weakening ( FL ew ) gives rise to serious complications for proof search. For example, adding to FL ew a naive version of these rules brakes cut-admissibility. Although this can be avoided by refining these rules, in this work we sho...More
Full Text (Upload PDF)
PPT (Upload PPT)