Stefano Cavagnetto

Propositional Proof Complexity and Rewriting

Download

Charles University in Prague Faculty of Mathematics and Physics 2008

Abstract:
In this work we want to find a new framework for propositional proofs (and in particular for resolution proofs) utilizing rewriting techniques. We interpret the well-known propositional proof system resolution using string rewriting systems $\Sigma^{*}_{n}$ and $\Sigma_{n}$ corresponding to tree-like proofs and sequence-like proofs, respectively. We prove that the system $\Sigma^{*}_{n}$ is complete and sound with respect to tree-like Resolution $R^{*}$ (and we show how it is possible to obtain the same result for $R$). Using this interpretation we give a representation of $\Sigma^{*}_{n}$ using planar diagrams in van Kampen style. In this representation we show how the classical complexity measures for Resolution (size, width and space) can be interpreted.

Subsequently, we consider rewriting in a synchronous, parallel fashion as it is used in the theory of cellular automata. In this respect, we give a new proof of Richardson theorem (a global function $G_{\mathbb{A}}$ of a cellular automaton ${\mathbb{A}}$ is injective if and only if the inverse of $G_{\mathbb{A}}$ is a global function of a cellular automaton), a classical result in the field, exploiting only propositional logic. In particular, we show how compactness of propositional logic and Craig's interpolation theorem suffice in order to prove the theorem. Moreover, we show a way how to construct the inverse cellular automaton using the method of feasible interpolation.

We also solve two problems regarding complexity of cellular automata formulated by Durand in \emph{Inversion of 2D cellular automata: some complexity results}. The first problem can be stated as follows: consider finite bounded configurations and a reversible cellular automaton that is given by a \lq\lq simple\rq\rq \ algorithm. Is the inverse automaton given by a \lq\lq simple\rq\rq \ algorithm too? The second problem is the following: the injectivity problem of cellular automata on bounded size is ${co\cal{NP}}$-complete; does the result still hold if we consider instead of the size of the transition table, the smallest program (circuit) which computes its transition table?

Finally, we present a new proof system based on cellular automata.

Table of Contents:

1. Propositional Proof Complexity
1. Some technical preliminaries
2. The complexity of propositional proofs
3. Resolution
4. Interpolation and effective interpolation
5. Mathematical proof systems
   
   
2. String Rewriting and Propositional Proof Complexity
1. The string rewriting system $\Sigma^{*}_{n}$
2. $\Sigma^{*}_{n}$ and $R^{*}$: the tree-like case
3. Planar diagrams representing proofs in $\Sigma^{*}_{n}$
4. Resolution and $\Sigma_{n}$: the dag-like case
5. Some remarks
   
   
3. Applications of Propositional Logic to Cellular Automata
1. Cellular Automata: definitions and some basics results
2. A proof of the richardson theorem via propositional logic
3. Some complexity results
   
   
4. Inverse Cellular Automata as propositional proofs
1. Durand's Theorem
2. A proof system based on cellular automata
3. Some remarks

Number of pages: 90

---

ISSN 1433-8092 | Imprint