We explore the relationships between the computational problem of recognizing expander graphs, and the problem of efficiently approximating proof length in the well-known system of \emph{resolution}. This program builds upon known connections between graph expansion and resolution lower bounds. A proof system $P$ is \emph{(quasi-)automatizable} if there is a search algorithm which finds a $P$-proof of a given formula $f$ in time (quasi)polynomial in the length of a shortest $P$-proof of $f$. It is open whether resolution is (quasi-)automatizable. We prove several conditional non-automatizability results for resolution modulo new conjectures concerning the complexity of identifying bipartite expander graphs. Our reductions use a natural family of formulas and exploit the well-known relationships between expansion and length of resolution proofs. Our hardness assumptions are unsupported; we survey known results as progress towards establishing their plausibility. The major contribution is a conditional hardness result for the quasi-automatizability of resolution.

We explore the relationships between the computational problem of recognizing expander graphs, and the problem of efficiently approximating proof length in the well-known system of \emph{resolution}. This program builds upon known connections between graph expansion and resolution lower bounds. A proof system $P$ is \emph{(quasi-)automatizable} if there is a search algorithm which finds a $P$-proof of a given formula $f$ in time (quasi)polynomial in the length of a shortest $P$-proof of $f$. It is open whether resolution is (quasi-)automatizable. We prove several conditional non-automatizability results for resolution modulo new conjectures concerning the complexity of identifying bipartite expander graphs. Our reductions use a natural family of formulas and exploit the well-known relationships between expansion and length of resolution proofs. Our hardness assumptions are unsupported; we survey known results as progress towards establishing their plausibility. The major contribution is a conditional hardness result for the quasi-automatizability of resolution.

Our research is in the general area of String Algorithms and Combinatorics on Words. Specifically, we study a generalization of square-free strings, shuffle properties of strings, and formalizing the reasoning about finite strings. The existence of infinitely long square-free strings (strings with no adjacent repeating word blocks) over a three (or more) letter finite set (referred to as Alphabet) is a well-established result. A natural generalization of this problem is that only subsets of the alphabet with predefined cardinality are available, while selecting symbols of the square-free string. This problem has been studied by several authors, and the lowest possible bound on the cardinality of the subset given is four. The problem remains open for subset size three and we investigate this question. We show that square-free strings exist in several specialized cases of the problem and propose approaches to solve the problem, ranging from patterns in strings to Proof Complexity. We also study the shuffle property (analogous to shuffling a deck of cards labeled with symbols) of strings, and explore the relationship between string shuffle and graphs, and show that large classes of graphs can be represented with special type of strings. Finally, we propose a theory of strings, that formalizes the reasoning about finite strings. By engaging in this line of research, we hope to bring the richness of the advanced field of Proof Complexity to Stringology. / Thesis / Doctor of Philosophy (PhD)

[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).

Název práce: O síle slabých rozšírení teorie V0 Autor: Sebastian Müller Katedra: Katedra Algebry Vedoucí disertační práce: Prof. RNDr. Jan Krajíček, DrSc., Katedra Algebry. Abstrakt: V predložené disertacní práci zkoumáme sílu slabých fragmentu arit- metiky. Činíme tak jak z modelově-teoretického pohledu, tak z pohledu důkazové složitosti. Pohled skrze teorii modelu naznačuje, že malý iniciální segment libo- volného modelu omezené aritmetiky bude modelem silnější teorie. Jako příklad ukážeme, že každý polylogaritmický řez modelu V0 je modelem VNC. Užitím známé souvislosti mezi fragmenty omezené aritmetiky a dokazatelností v ro- zličných důkazových systémech dokážeme separaci mezi rezolucí a TC0 -Frege systémem na náhodných 3CNF-formulích s jistým poměrem počtu klauzulí vůci počtu proměnných. Zkombinováním obou výsledků dostaneme slabší separační výsledek pro rezoluci a Fregeho důkazové systémy omezené hloubky. Klíčová slova: omezená aritmetika, důkazová složitost, Fregeho důkazový systém, Fregeho důkazový systém omezené hloubky, rezoluce Title: On the Power of Weak Extensions of V0 Author: Sebastian Müller Department: Department of Algebra Supervisor: Prof. RNDr. Jan Krajíček, DrSc., Department of Algebra....

Les questions <EM>"Qu'est-ce qu'une preuve?"</EM> et <EM>"Quand deux preuves sont-elles identiques?"</EM> sont fondamentales pour la théorie de la preuve. Mais pour la logique classique propositionnelle --- la logique la plus répandue --- nous n'avons pas encore de réponse satisfaisante. C'est embarrassant non seulement pour la théorie de la preuve, mais aussi pour l'informatique, où la logique classique joue un rôle majeur dans le raisonnement automatique et dans la programmation logique. De même, l'architecture des processeurs est fondée sur la logique classique. Tous les domaines dans lesquels la recherche de preuve est employée peuvent bénéficier d'une meilleure compréhension de la notion de preuve en logique classique, et le célèbre problème NP-vs-coNP peut être réduit à la question de savoir s'il existe une preuve courte (c'est-à-dire, de taille polynomiale) pour chaque tautologie booléenne. Normalement, les preuves sont étudiées comme des objets syntaxiques au sein de systèmes déductifs (par exemple, les tableaux, le calcul des séquents, la résolution, ...). Ici, nous prenons le point de vue que ces objets syntaxiques (également connus sous le nom d'arbres de preuve) doivent être considérés comme des représentations concrètes des objets abstraits que sont les preuves, et qu'un tel objet abstrait peut être représenté par un arbre en résolution ou dans le calcul des séquents. Le thème principal de ce travail est d'améliorer notre compréhension des objets abstraits que sont les preuves, et cela se fera sous trois angles différents, étudiés dans les trois parties de ce mémoire: l'algèbre abstraite (chapitre 2), la combinatoire (chapitres 3 et 4), et la complexité (chapitre 5).

[pt] A teoria da prova tradicional da lógica proposicional trata provas cujos tamanhos podem ser demasiado grandes. Estudos teóricos de prova descobriram diferenças exponenciais entre provas normais ou livres de corte e suas respectivas provas não-normais. Assim, o uso de grafos-de-prova, ao invés de árvores ou listas, para representar provas está se tornando mais popular entre teóricos da prova. Os grafos-de-prova servem como uma forma de proporcionar uma melhor simetria para a semântica de provas e uma maneira de estudar a complexidade das provas proposicionais. O objetivo deste trabalho é reduzir o peso/tamanho de deduções. Apresentamos formalismos de grafos de prova que visam capturar a estrutura lógica de uma dedução e uma forma de facilitar a visualização das propriedades. A vantagem destes formalismos é que as fórmulas e sub-deduções em dedução natural, preservadas na estrutura de grafo, podem ser compartilhadas eliminando sub-deduções desnecessárias resultando na prova reduzida. Neste trabalho, damos uma definição precisa de grafos de prova para a lógica puramente implicacional, logo estendemos esse resultado para a lógica proposicional completa e mostramos como reduzir (eliminando fórmulas máximas) essas representações de tal forma que um teorema de normalização pode ser provado através da contagem do número de fórmulas máximas na derivação original. A normalização forte será uma consequência direta desta normalização, uma vez que qualquer redução diminui as medidas correspondentes da complexidade da derivação. Continuando com o nosso objetivo de estudar a complexidade das provas, a abordagem atual também fornece representações de grafo para lógica de primeira ordem, a inferência profunda e lógica bi-intuitionista. / [en] Traditional proof theory of Propositional Logic deals with proofs which size can be huge. Proof theoretical studies discovered exponential gaps between normal or cut free proofs and their respective non-normal proofs. Thus, the use of proof-graphs, instead of trees or lists, for representing proofs is getting popular among proof-theoreticians. Proof-graphs serve as a way to provide a better symmetry to the semantics of proofs and a way to study complexity of propositional proofs and to provide more efficient theorem provers, concerning size of propositional proofs. The aim of this work is to reduce the weight/size of deductions. We present formalisms of proof-graphs that are intended to capture the logical structure of a deduction and a way to facilitate the visualization. The advantage of these formalisms is that formulas and subdeductions in Natural Deduction, preserved in the graph structure, can be shared deleting unnecessary sub-deductions resulting in the reduced proof. In this work, we give a precise definition of proof-graphs for purely implicational logic, then we extend this result to full propositional logic and show how to reduce (eliminating maximal formulas) these representations such that a normalization theorem can be proved by counting the number of maximal formulas in the original derivation. The strong normalization will be a direct consequence of such normalization, since that any reduction decreases the corresponding measures of derivation complexity. Continuing with our aim of studying the complexity of proofs, the current approach also give graph representations for first order logic, deep inference and bi-intuitionistic logic.