XINFORMAÇÕES SOBRE DIREITOS AUTORAIS
As obras disponibilizadas nesta Biblioteca Digital foram publicadas sob expressa autorização dos respectivos autores, em conformidade com a Lei 9610/98.
A consulta aos textos, permitida por seus respectivos autores, é livre, bem como a impressão de trechos ou de um exemplar completo exclusivamente para uso próprio. Não são permitidas a impressão e a reprodução de obras completas com qualquer outra finalidade que não o uso próprio de quem imprime.
A reprodução de pequenos trechos, na forma de citações em trabalhos de terceiros que não o próprio autor do texto consultado,é permitida, na medida justificada para a compreeensão da citação e mediante a informação, junto à citação, do nome do autor do texto original, bem como da fonte da pesquisa.
A violação de direitos autorais é passível de sanções civis e penais.
As obras disponibilizadas nesta Biblioteca Digital foram publicadas sob expressa autorização dos respectivos autores, em conformidade com a Lei 9610/98.
A consulta aos textos, permitida por seus respectivos autores, é livre, bem como a impressão de trechos ou de um exemplar completo exclusivamente para uso próprio. Não são permitidas a impressão e a reprodução de obras completas com qualquer outra finalidade que não o uso próprio de quem imprime.
A reprodução de pequenos trechos, na forma de citações em trabalhos de terceiros que não o próprio autor do texto consultado,é permitida, na medida justificada para a compreeensão da citação e mediante a informação, junto à citação, do nome do autor do texto original, bem como da fonte da pesquisa.
A violação de direitos autorais é passível de sanções civis e penais.
Coleção Digital
Título: COMPACTAÇÃO DE PROVAS LÓGICAS Autor: VASTON GONCALVES DA COSTA
Instituição: PONTIFÍCIA UNIVERSIDADE CATÓLICA DO RIO DE JANEIRO - PUC-RIO
Colaborador(es):
EDWARD HERMANN HAEUSLER - ORIENTADOR
Nº do Conteudo: 10018
Catalogação: 01/06/2007 Idioma(s): PORTUGUÊS - BRASIL
Tipo: TEXTO Subtipo: TESE
Natureza: PUBLICAÇÃO ACADÊMICA
Nota: Todos os dados constantes dos documentos são de inteira responsabilidade de seus autores. Os dados utilizados nas descrições dos documentos estão em conformidade com os sistemas da administração da PUC-Rio.
Referência [pt]: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=10018@1
Referência [en]: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=10018@2
Referência DOI: https://doi.org/10.17771/PUCRio.acad.10018
Resumo:
Título: COMPACTAÇÃO DE PROVAS LÓGICAS Autor: VASTON GONCALVES DA COSTA
Nº do Conteudo: 10018
Catalogação: 01/06/2007 Idioma(s): PORTUGUÊS - BRASIL
Tipo: TEXTO Subtipo: TESE
Natureza: PUBLICAÇÃO ACADÊMICA
Nota: Todos os dados constantes dos documentos são de inteira responsabilidade de seus autores. Os dados utilizados nas descrições dos documentos estão em conformidade com os sistemas da administração da PUC-Rio.
Referência [pt]: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=10018@1
Referência [en]: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=10018@2
Referência DOI: https://doi.org/10.17771/PUCRio.acad.10018
Resumo:
É um fato conhecido que provas clássicas podem ser
demasiadamente grandes. Estudos em teoria da prova
descobriram diferenças exponenciais entre
provas normais (ou provas livres do corte) e suas
respectivas provas não normais. Por outro lado, provadores
automáticos de teorema usualmente se baseiam na
construção de provas normais, livres de corte ou provas de
corte atômico, pois tais procedimento envolvem menos
escolhas. Provas de algumas tautologias são
conhecidamente grandes quanto realizadas sem a regra do
corte e curtas quando a utilizam. Queremos com este
trabalho apresentar procedimentos para reduzir o
tamanho de provas proposicionais. Neste sentido,
apresentamos dois métodos. O primeiro, denominado método
vertical, faz uso de axiomas de extensão e alguns
casos é possível uma redução considerável no tamanho da
prova. Apresentamos um procedimento que gera tais axiomas
de extensão. O segundo, denominado método horizontal,
adiciona fórmulas máximas por meio de unificação via
substituição de variáveis proposicionais. Também
apresentamos um método que gera tal unificação durante o
processo de construção da prova. O primeiro método
é aplicado a dedução natural enquanto o segundo à Dedução
Natural e Cálculo de Seqüentes. As provas produzidas
correspondem de certo modo a provas não normais (com a
regra do corte).
Descrição | Arquivo |
CAPA, AGRADECIMENTOS, RESUMO, ABSTRACT, SUMÁRIO E LISTAS | |
CAPÍTULO 1 | |
CAPÍTULO 2 | |
CAPÍTULO 3 | |
CAPÍTULO 4 | |
CAPÍTULO 5 | |
REFERÊNCIAS BIBLIOGRÁFICAS E APÊNDICES |