[pt] A quantização eficiente dos coeficientes do filtro de síntese utilizado em codificadores de voz CELP (Code Excited Linear Prediction) é fundamental para o bom desempenho desta classe de codificadores, especialmente quando se considera a operação em taxas inferiores a 8 Kbps. Neste trabalho são examinados três quantizadores vetoriais distintos que apresentam bom potencial para utilização em codificadores que operem a baixas taxas de bits. Cada um desses quantizadores foi implementado dentro da estrutura do codificador VSELP (Vector Sum Excited Linear Prediction) uma variação importante do codificador CELP padronizada para uso na telefonia celular digital americana. Estas três técnicas de quantização vetorial dos coeficientes do filtro baseiam-se na representação LSP e são comparadas em termos da robustez aos erros no canal de transmissão, da complexidade computacional de implementação e, principalmente, da qualidade da voz sintetizada (avaliada em função de medidas objetivas de razão sinal ruído ponderada e de testes de escuta informais). Também é examinada a aplicação da técnica de Simulated Annealing para associação de índices aos níveis de saída dos quantizadores, visando diminuir a sua sensibilidade aos erros no canal de transmissão. / [en] Efficent quantization of synthesis filter coefficients on CELP (Code Excited Linear Prediction) coders is very important for a good performance of this class of coders, specially when operating below 8 Kbps. Three vector quantizers with good potential for utilization on low rate coders are studied. Each of them was implemented inside the structure of VSELP( Vector Sum Linear Prediction) coder, an important menber in the class of CELP coders: VSELP is the north American cellular Communication standard. These three vector quantizers work with LSP parameters and are compared considering the robustness to channel errors, complexity and quality of sythesized speech. The quality of synthesized speech is evaluated considering objective measures of frequency weighted signal to noise ratio and subjective results obtained from informal listening tests. In order to improve the robustness to channel errors, the problem of binary indices assignment to the output levels of the quantizer is also investigated. The technique used to determine good indices assignments is Simulated Annealing

[pt] Existem diferentes estilos de cálculos dedutivos, usados para derivar os teoremas de uma lógica. Os mais habituais são os sistemas axiomáticos; mas, do ponto de vista da teoria da prova, os sistemas em dedução natural parecem ser mais interessantes. Essa é a motivação que leva ao desenvolvimento de técnicas que visam a facilitar a transformação de um cálculo dedutivo para o estilo em dedução natural. Esse trabalho se concentra no aspecto de modelar regras para os quantificadores da linguagem considerada e, para isso, faz uso de rótulos. Após uma apresentação intuitiva da técnica desenvolvida, passa-se à exposição de sistemas lógicos tratados pelo método: lógica de ultrafiltros, lógica de filtros, CTL, lógica de Keisler e CTL*. Em cada caso, analisam-se aspectos de teoria da prova. / [en] There are many kinds of deductive calculus. The axiomatic ones are the more usual. However, from the point of view of proof theory, Natural Deduction systems seem to be more interesting. This is the motivation for developping a technique that aims to ease the transformation from deductive calculus to Natural Deduction style. This work concentrates on the aspect of modeling the rules for the quantifiers of the logic considered, and for this purpose labels are used. After an intuitive presentation of the technique developped, some logical systems are treated by the method: ultrafilter logic, filter logic, CTL, Keisler`s logic and CTL*. For each one of them proof-theoretical aspects are analysed.