String Rewriting and Proof Complexity: an interpretation of Resolution

• Autorzy: Cavagnetto S.
• Języki publikacji: EN

Abstrakty

EN

We interpret the well-known propositional proof system Resolution using string rewriting systems Sigma*n n and Sigma n corresponding to tree-like proofsa and sequence-like proofs, respectively. We give a representation of Sigma*n n using planar diagrams.

• Wydawca: Wydawnictwo Uniwersytetu Jagiellońskiego
• Czasopismo: Reports on Mathematical Logic
• Rocznik: 2009
• Tom: Vol. 44
• Strony: 167--200
• Opis fizyczny: Bibliogr. 25 poz., rys.

Twórcy

autor

Cavagnetto S.

• Institute of Mathematics Academy of Sciences of Czech Republic Žitná 25, 11567 Prague 1 Czech Republic,

Bibliografia

• [1] A. Atserias, M. L. Bonet, On the automatizability of resolution and related Propositional Proof Systems, Information and Computation 189, 2 (2004), pp. 182–201.
• [2] E. Ben-Sasson, R. Impagliazzo, and A. Wigderson, Near-optimal separation of treelike and general resolution, ECCC, Report TR02-005 (2000).
• [3] E. Ben-Sasson, and A.Wigderson, Short proofs are Narrow–Resolution made Simple, Journal of the ACM 48, 2 (2001), pp. 149–169.
• [4] A. Blake, Canonical expression in boolean Algebra, Ph.D Thesis (1937), University of Chicago.
• [5] M.L. Bonet, J.L. Esteban, N. Galesi and J. Johannsen, Exponential separations between Restricted Resolution and Cutting Planes Proof Systems, in 39th Symposium on Foundations of Computer Science (FOCS 1998), pp. 638–647.
• [6] M. Bridson, The geometry of the word problem, in: Invitations to Geometry and Topology, Oxford University Press, (2002).
• [7] K. Büning, T. Lettman, Aussangenlogik: Deduktion und Algorithmen (1994), B.G Teubner Stuttgart.
• [8] N. Chomsky, Three models for the Description of Language, IRE Transactions on Information Theory 2, 2 (1956), pp. 113–123.
• [9] P. Clote and A. Setzer, On PHP st-connectivity and odd charged graphs—, in P. Beame and S. Buss, editors, Proof Complexity and Feasible Arithmetics, AMS DIMACS Series 39 (1998), pp. 93–117.
• [10] S.A. Cook, and A.R. Reckhow, The relative efficiency of propositional proof systems, Journal of Symbolic Logic 44, 1 (1977), pp. 36–50.
• [11] M. Davis, Computability and Unsolvability, Dover Pubblications, Inc, New York, (1958).
• [12] M. Delorme and J. Mazoyer, editors, Cellular Automata: a parallel model, Mathematics and its Application, Springer, (1998).
• [13] J.L. Esteban, J. Tor´an, Space bounds for resolution, Information and Computation, 171, 1 (2001), pp. 84–97.
• [14] Z. Galil, On resolution with clauses of bounded size, SIAM Journal of Computing 6 (1977), pp. 444–459.
• [15] K. Iwama and S. Miyazaki, Tree-like Resolution is superpolinomially slower then dag-like resolution for the Pigeonhole Principle, in A. Aggarwal and C.P. Rangan, editors, Proceedings: Algorithms and Computation, 10th International Symposium, ISAAC’99, Vol. 1741 (1999), pp. 133–143.
• [16] H. von Koch, Sur une courbe continue sans tangente obtenue par une construction géométrique élémentaire, Archiv. für Matem. Fys., 1 (1904), pp. 681–702.
• [17] J. Kari, Reversible Cellular Automata, Proceedings of DLT 2005, Developments in Language Theory, Lecture Notes in Computer Science 3572, Springer-Verlag, 2005, pp. 57–68.
• [18] J. Krajíček, Bounded arithmetic, propositional logic, and complexity theory, Encyclopedia of Mathematics and Its Applications 60, Cambridge University Press, 1995.
• [19] J. Krajíček, Propositional proof complexity I., Lecture notes, available at http://www.math.cas.cz/krajicek/biblio.html.
• [20] J. Krajíček, Dehn function and length of proofs, International Journal of Algebra and Computation, 13, 5 (2003), pp. 527–542.
• [21] A. Thue, Die Lösung eines Spezialfalles eines gnerellen Logischen Problems, Kra.Videnskabs-Selskabets Skriften I. Mat. Nat. Kl., 8 (1910).
• [22] A. Thue, Probleme über Veranderungen von Zeichenreihen nach gegeben Regeln, Skr.Vid. Kristianaia I. Mat. Natarv. Klasse, 10/13 (1914).
• [23] R. Raz and P. McKenzie, Separation of the monotone NC hierarchy, in Proc. 38th Symposium on Foundations of Computer Science (1997), pp. 234–243.
• [24] A. Urquhart, The Complexity of Propositional Proofs, Bulletin of Symbolic Logic, 1, 4 (1996), pp. 425–467.
• [25] K. Wagner and G. Wechsung, Computational Complexity, Riedel, 1986.