[pt] O tamanho das provas formais possui algumas importantes implicações
teóricas na área da complexidade computacional. O problema de determinar
se uma fórmula é uma tautologia da Lógica Proposicional Intuicionista e do
fragmento puramente implicacional da Lógica Minimal (M(contém)) é PSPACE-
Completo. Qualquer lógica proposicional com um sistema de dedução
natural que satisfaça o princípio da subfórmula possui o problema de
determinar tautologias em PSPACE. Saber se qualquer tautologia em M(contém)
admite provas de tamanho polinomialmente limitado está relacionado com
saber se NP = PSPACE. Técnicas de compressão de provas reportadas
na literatura utilizam duas abordagens principais para comprimir provas:
gerar provas já compactadas; comprimir uma prova já gerada. Proposta
por Gordeev e Haeusler (6), a Compressão Horizontal é uma técnica
de compressão de provas em dedução natural da M(contém) que utiliza grafos
direcionados para representar as provas. Dada a prova de uma tautologia
qualquer da M(contém), que pode possuir tamanho exponencial em relação ao
tamanho da conclusão, o objetivo da Compressão Horizontal é que a prova
resultante da compressão possua tamanho polinomialmente limitado em
relação ao tamanho da conclusão. Nosso trabalho apresenta a primeira
implementação da Compressão Horizontal, juntamente com os primeiros
resultados da aplicação da técnica sobre provas de tautologias da M(contém), além
disso, compara as taxas de compressão obtidas com técnicas tradicionais de
compressão de dados. / [en] The size of formal proofs has some important theoretical implications
in computational complexity theory. The problem of determining if some
formula of Intuitionistic Propositional Logic and the purely implicational
fragment of Minimal Logic (M(contains)) is a tautology is PSPACE-Complete. Any
propositional logic with a natural deduction system that satisfies the sub-
formula principle is PSPACE. To know if any tautology in M(contains) admits
polynomially sized proof is related to whether NP = PSPACE. Proof
compression techniques reported in literature use two main approaches
to proof compressing: generating already compressed proofs; compressing
an already generated proof. Proposed by Gordeev and Haeusler (6), the
Horizontal Compression is a natural deduction proof compression technique
that uses directed graphs to represent proofs. Given a tautology proof in
M(contains), which may have an exponential size in relation to conclusion length,
the goal of Horizontal Compression is that the compressed proof has a
polynomially limited size in relation to conclusion length. Our work presents
the first implementation of Horizontal Compression, together with the first
results of the execution of the technique on proofs of M(contains) tautologies.
| Identifer | oai:union.ndltd.org:puc-rio.br/oai:MAXWELL.puc-rio.br:47267 |
| Date | 26 March 2020 |
| Creators | JOSE FLAVIO CAVALCANTE BARROS JUNIOR |
| Contributors | EDWARD HERMANN HAEUSLER |
| Publisher | MAXWELL |
| Source Sets | PUC Rio |
| Language | Portuguese |
| Detected Language | Portuguese |
| Type | TEXTO |
Page generated in 0.0027 seconds