[pt] COMPACTAÇÃO DE PROVAS LÓGICAS

[en] LOGIC PROOFS COMPACTATION

[pt] VASTON GONCALVES DA COSTA

[pt] TEORIA DA PROVA

[pt] LOGICA PROPOSICIONAL

[pt] CALCULO DE SEQUENCIAS

[pt] COMPLEXIDADE DE PROVAS

[pt] DEDUCAO NATURAL

[en] PROOF THEORY

[en] PROPOSITIONAL LOGIC

[en] SEQUENT CALCULUS

[en] PROOF COMPLEXITY

[en] NATURAL DEDUCTION

[pt] É 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).

[en] It is well-known that the size of propositional classical proofs can be huge. Proof theoretical studies discovered exponential gaps between normal or cut-free proofs and their respective non-normal proofs. The task of automatic theorem proving is, on the other hand, usually based on the construction of normal, cut-free or only-atomic-cuts proofs, since this procedure produces less alternative choices. There are familiar tautologies such that the cut-free proof is huge while the non-cut-free is small. The aim of this work is to reduce the weight of proposicional deductions. In this sense we present two methods. The fi first, namely vertical method, uses the extension axioms. We present a method that generates a such extension axiom. The second, namely horizontal method, adds suitable (propositional) unifi fications modulo variable substitutions.We also present a method that generates a such unifi fication during the proving process. The proofs produced correspond in a certain way to non normal proofs (non cut-free proofs).

EDWARD HERMANN HAEUSLER

EDWARD HERMANN HAEUSLER

LUIZ CARLOS PINHEIRO DIAS PEREIRA

MAURICIO AYALA RINCON

MARCELO DA SILVA CORREA

GEIZA MARIA HAMAZAKI DA SILVA

2007-06-01

2007-04-09

[pt] TEXTO

application/pdf

application/pdf

application/pdf

application/pdf

application/pdf

application/pdf

application/pdf

PORTUGUÊS

https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=10018@1

https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=10018@2

https://doi.org/10.17771/PUCRio.acad.10018