From cut-free calculi to automated deduction: the case of bounded contraction

Ciabattoni, Agata; Lellmann, Bjorn; Vega, Carlos Alberto Olarte; Pimentel, Elaine Gouvea

From cut-free calculi to automated deduction: the case of bounded contraction

Página do item simplificado Estatísticas

dc.contributor.author	Ciabattoni, Agata
dc.contributor.author	Lellmann, Bjorn
dc.contributor.author	Vega, Carlos Alberto Olarte
dc.contributor.author	Pimentel, Elaine Gouvea
dc.date.accessioned	2020-07-30T18:37:21Z
dc.date.available	2020-07-30T18:37:21Z
dc.date.issued	2017
dc.description.resumo	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	pt_BR
dc.identifier.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: https://www.researchgate.net/publication/317825238_From_Cut-free_Calculi_to_Automated_Deduction_The_Case_of_Bounded_Contraction. Acesso em: 29 jul. 2020. http://dx.doi.org/10.1016/j.entcs.2017.04.006.	pt_BR
dc.identifier.doi	10.1016/j.entcs.2017.04.006.
dc.identifier.issn	1571-0661
dc.identifier.uri	https://repositorio.ufrn.br/jspui/handle/123456789/29757
dc.language	en	pt_BR
dc.publisher	Elsevier	pt_BR
dc.subject	Proof theory	pt_BR
dc.subject	Substructural logics	pt_BR
dc.subject	Proof search	pt_BR
dc.subject	Bounded contraction	pt_BR
dc.title	From cut-free calculi to automated deduction: the case of bounded contraction	pt_BR
dc.type	article	pt_BR