[en] ARGUING NP = PSPACE: ON THE COVERAGE AND SOUNDNESS OF THE HORIZONTAL COMPRESSION ALGORITHM

Detalhes bibliográficos
Ano de defesa:	2024
Autor(a) principal:	ROBINSON CALLOU DE M BRASIL FILHO
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:	eng
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] GRAFO ACICLICO DIRECIONADO [pt] COMPLEXIDADE DE ALGORITMOS [pt] LOGICA MINIMAL PURAMENTE IMPLICACIONAL [pt] COMPRESSAO DE PROVA [en] DIRECTED ACYCLIC GRAPH [en] ALGORITHM COMPLEXITY [en] PURELY IMPLICATIONAL MINIMAL LOGIC [en] PROOF COMPRESSION
Link de acesso:	https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=67979&idi=1 https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=67979&idi=2 http://doi.org/10.17771/PUCRio.acad.67979
Resumo:	[pt] Este trabalho é uma elaboração, com exemplos, e evolução do Algoritmo de Compressão Horizontal (HC) apresentado e seu Conjunto de Regras de Compressão. Este trabalho apresenta uma prova, feita no Provador Interativo de Teoremas Lean, de que o algoritmo HC pode obter uma Derivação Comprimida, representada por um Grafo Acíclico Dirigido, a partir de qualquer Derivação Tipo-Árvore em Dedução Natural para a Lógica Minimal Puramente Implicacional. Finalmente, a partir da Cobertura e Corretude do algoritmo HC, pode-se argumentar que NP = PSPACE.

Registros relacionados