[pt] Este trabalho é uma elaboração, com exemplos, e evolução do Algoritmo de Compressão Horizontal (HC) apresentado e seu Conjunto de Regras de Compressão. Este trabalho apresenta uma prova, feita no Provador Interativo de Teoremas Lean, de que o algoritmo HC pode obter uma Derivação Comprimida, representada por um Grafo Acíclico Dirigido, a partir de qualquer Derivação Tipo-Árvore em Dedução Natural para a Lógica Minimal Puramente Implicacional. Finalmente, a partir da Cobertura e Corretude do algoritmo HC, pode-se argumentar que NP = PSPACE. / [en] This work is an elaboration, with examples, and evolution of the presented Horizontal Compression Algorithm (HC) and its set of Compression Rules. This work argues a proof, done in the Lean Interactive Theorem Prover, that the HC algorithm can obtain a Compressed Derivation, represented by a Directed Acyclic Graph, from any Tree-Like Natural Deduction Derivation in Minimal Purely Implicational Logic. Finally, from the Coverage and Soundness of the HC algorithm, one can argue that NP = PSPACE.

[pt] Esta tese apresenta um novo cálculo de sequente, correto e completo para a Lógica Proposicional Minimal Implicacional (M →). LMT → destina-se a ser usado para a busca de provas em M →, em uma abordagem bottom-up. A Terminação do cálculo é garantida por uma estratégia de aplicação de regras que força uma maneira ordenada no procedimento de busca de provas de tal forma que todas as combinações possíveis são exploradas. Para uma fórmula inicial α, as provas em LMT→ têm um limite superior de |α|.2 |α|+1+2·log2|α|, que juntamente com a estratégia do sistema, garantem a decidibilidade do mesmo. As regras do sistema são concebidas para lidar com a necessidade de repetição de hipóteses e a natureza de perda de contexto da regra → esquerda , evitando a ocorrência de loops e o uso de backtracking. Portanto, a busca de prova em LMT → é determinística, sempre executando buscas no sentido forward. LMT → tem a propriedade de permitir a extração de contramodelos a partir de buscas de prova que falharam (bicompletude), isto é, a árvore de tentativa de prova de um ramo totalmente expandido produz um modelo de Kripke que falsifica a fórmula inicial. A geração de contra-modelo (usando a semântica Kripke) é obtida como consequência da completude do sistema. LMT→ é implementado como um provador de teoremas interativo baseado no cálculo proposto aqui. Comparamos nosso cálculo com outros sistemas dedutivos conhecidos para M →, especialmente com Tableaux no estilo Fitting, um método que também tem a propriedade de ser bicompleto. Também propomos aqui uma tradução de LMT → para o verificador de prova Dedukti como uma forma de avaliar a correção da implementação que desenvolvemos, no que diz respeito à especificação do sistema, além de torná-lo mais fácil de comparar com outros sistemas existentes. / [en] This thesis presents a new sequent calculus called LMT→ that has the properties to be terminating, sound and complete for Propositional Implicational Minimal Logic (M →). LMT→ is aimed to be used for proof search in M →, in a bottom-up approach. Termination of the calculus is guaranteed by a strategy of rule application that forces an ordered way to search for proofs such that all possible combinations are stressed. For an initial formula α, proofs in LMT→ has an upper bound of |α|.2 |α|+1+2·log2|α|, which together with the system strategy ensure decidability. System rules are conceived to deal with the necessity of hypothesis repetition and the contextsplitting nature of → left, avoiding the occurrence of loops and the usage of backtracking. Therefore, LMT→ steers the proof search always in a forward, deterministic manner. LMT→ has the property to allow extractability of counter-models from failed proof searches (bicompleteness), i.e., the attempt proof tree of an expanded branch produces a Kripke model that falsifies the initial formula. Counter-model generation (using Kripke semantics) is achieved as a consequence of the completeness of the system. LMT→ is implemented as an interactive theorem prover based on the calculus proposed here. We compare our calculus with other known deductive systems for M →, especially with Fitting s Tableaux, a method that also has the bicompleteness property. We also proposed here a translation of LMT→ to the Dedukti proof checker as a way to evaluate the correctness of the implementation regarding the system specification and to make our system easier to compare to others.

La thèse est consacrée à des problématiques d’algorithmique et de complexité sur deux sujets. Le premier sujet s’intéresse à la composition comportementale des services web. Ce problème a été réduit à la simulation d’un automate par le produit fermé d’un ensemble d’automates. La thèse étudie dans sa première partie la complexité de ce problème en considérant deux paramètres : le nombre des instances considéré de chaque service et la présence des états hybrides : état à la fois intermédiaire et final dans un automate. Le second sujet porte sur les systèmes de fermeture et s’intéresse au calcul de l’extension maximale d’un système de fermeture ainsi qu’à l’énumération des clefs candidates d’une base implicative. On donne un algorithme incrémental polynomial qui génère l’extension maximale d’un treillis codé par une relation binaire. Puis, la notion de key-ideal est définie, en prouvant que leur énumération est équivalente à l’énumération des clefs candidates. Ensuite, on donne un algorithme qui permet de générer les key-ideal minimaux en temps incrémental polynomial et les key-ideal non minimaux en délai polynomial. / This thesis investigates complexity and computational issues in two parts. The first concerns an issue related to web services composition problem: Deciding whether the behaviour of a web service can be composed out of an existing repository of web services. This question has been reduced to simulating a finite automata to the product closure of an automata set. We study the complexity of this problem considering two parameters; the number of considered instances in the composition and the presence of the so-called hybrid states (states that are both intermediate and final). The second part concerns closure systems and two related issues; Maximal extension of a closure system : we give an incremental polynomial algorithm that computes a lattice's maximal extension when the input is a binary relation. Candidate keys enumeration : we introduce the notion of key-ideal sets and prove that their enumeration is equivalent to candidate keys enumeration. We then give an efficient algorithm that generates all non-minimal key-ideal sets in a polynomial delay and all minimal ones in incremental polynomial time.