Please use this identifier to cite or link to this item:
Title: From cut-free calculi to automated deduction: the case of bounded contraction
Authors: Ciabattoni, Agata
Lellmann, Bjorn
Vega, Carlos Alberto Olarte
Pimentel, Elaine Gouvea
Keywords: Proof theory;Substructural logics;Proof search;Bounded contraction
Issue Date: 2017
Publisher: Elsevier
Citation: CIABATTONI, Agata; LELLMANN, Björn; OLARTE, Carlos; PIMENTEL, Elaine. From Cut-free Calculi to Automated Deduction: the case of bounded contraction. Electronic Notes in Theoretical Computer Science, [S.L.], v. 332, p. 75-93, jun. 2017. Disponível em: Acesso em: 29 jul. 2020.
Portuguese Abstract: The addition of the bounded contraction rules to Full Lambek Calculus with exchange and weakening (FLew) gives rise to serious complications for proof search. For example, adding to FLew a naive version of these rules brakes cut-admissibility. Although this can be avoided by refining these rules, in this work we show that even “good” proof systems for FLew plus bounded contraction do not necessarily lead to good implementations. In order to solve this problem, we propose an extension of the lazy splitting methodology to bounded contractions, showing how to transform our focused, cut-free sequent calculus into a terminating theorem prover. Our system is used to show that the decision problem for FLew with bounded contraction is in EXPTIME
ISSN: 1571-0661
Appears in Collections:CCET - DM - Artigos publicados em periódicos
ECT - Artigos publicados em periódicos

Files in This Item:
File Description SizeFormat 
FromCut-freeCalculi_VEGA_2017.pdf324,19 kBAdobe PDFThumbnail

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.