[en] BUILDING TABLEAUX FOR INTUITIONISTIC LINEAR LOGIC

Detalhes bibliográficos
Ano de defesa:	2022
Autor(a) principal:	HUGO HOFFMANN BORGES
Orientador(a):	Não Informado pela instituição
Banca de defesa:	Não Informado pela instituição
Tipo de documento:	Tese
Tipo de acesso:	Acesso aberto
Idioma:	por
Instituição de defesa:	MAXWELL
Programa de Pós-Graduação:	Não Informado pela instituição
Departamento:	Não Informado pela instituição
País:	Não Informado pela instituição
Palavras-chave em Português:	[pt] TEORIA DA PROVA [pt] TABLEAUX [pt] LOGICA RELEVANTE [pt] LOGICA LINEAR [en] PROOF THEORY [en] TABLEAU [en] RELEVANT LOGIC [en] LINEAR LOGIC
Link de acesso:	https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=58715&idi=1 https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=58715&idi=2 http://doi.org/10.17771/PUCRio.acad.58715
Resumo:	[pt] O objetivo desta dissertação é construir um tableaux linear intuicionista a partir de um cálculo de sequentes relevante clássico. Os passos principais dessa construção são: i) tradução das regras do cálculo dos sequentes relevante clássico para regras de tableaux (capítulo 3), usando a estratégia apresentada por D Agostino et al. em Tableau Methods for Substructural Logic. ii) construção de um tableaux linear clássico através da linearização do tableaux clássico relevante (capítulo 4). iii) apresentar um tableau intuicionista ao estilo Fitting, em que são adicionados rótulos T s e F s às fórmulas (capítulo 5).

Registros relacionados