[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).
| Identifer | oai:union.ndltd.org:puc-rio.br/oai:MAXWELL.puc-rio.br:10018 |
| Date | 01 June 2007 |
| Creators | VASTON GONCALVES DA COSTA |
| Contributors | EDWARD HERMANN HAEUSLER |
| Publisher | MAXWELL |
| Source Sets | PUC Rio |
| Language | Portuguese |
| Detected Language | Portuguese |
| Type | TEXTO |
Page generated in 0.0023 seconds