×

zbMATH — the first resource for mathematics

Towards Hilbert’s 24th problem: combinatorial proof invariants (preliminary version). (English) Zbl 1262.03120
Mints, G. (ed.) et al., Proceedings of the 13th workshop on logic, language, information and computation (WoLLIC 2006), Stanford, CA, USA, July 18–21, 2006. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 165, 37-63 (2006).
Summary: In [Ann. Math. (2) 164, No. 3, 1065–1076 (2006; Zbl 1130.03009)], the author introduced polynomial-time checkable combinatorial proofs for classical propositional logic. This sequel approaches Hilbert’s 24th Problem with combinatorial proofs as abstract invariants for sequent calculus proofs, analogous to homotopy groups as abstract invariants for topological spaces.
The paper lifts a simple, strongly normalising cut elimination from combinatorial proofs to sequent calculus, factorising away the mechanical commutations of structural rules which litter traditional syntactic cut elimination.
Sequent calculus fails to be surjective onto combinatorial proofs: the paper extracts a semantically motivated closure of sequent calculus from which there is a surjection, pointing towards an abstract combinatorial refinement of Herbrand’s theorem.
For the entire collection see [Zbl 1118.03304].

MSC:
03F07 Structure of proofs
03F05 Cut-elimination and normal-form theorems
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abramsky, S.; Jagadeesan, R., Games and full completeness for multiplicative linear logic, J. symb. logic, 59, 2, 543-574, (1994) · Zbl 0822.03007
[2] Abramsky, S.; Jagadeesan, R., New foundations for the geometry of interaction, Information and computation, 111, 1, 53-119, (1994) · Zbl 0803.03014
[3] Andrews, P.B., Theorem proving via general matings, J. ACM, 28, 193-214, (1981) · Zbl 0456.68119
[4] Baaz, M.; Leitsch, A., Fast cut-elimination by projection, Proc. comp. sci. logic ’96, Lec. notes in comp. sci., 1258, 18-33, (1996) · Zbl 0889.03048
[5] Bibel, W., An approach to a systematic theorem proving procedure in first-order logic, Computing, 12, 43-55, (1974) · Zbl 0273.68058
[6] Bellin, G., J.M.E. Hyland, E.P. Robinson. & C. Urban. Proof theory of classical propositional calculus. Theoretical Computer Science. To appear. Submitted 2004 · Zbl 1121.03086
[7] Bierman, G.M.; Urban, C., Strong normalisation of cut-elimination in classical logic, Fund. informaticae, 45, 1-2, 123-155, (2001) · Zbl 0982.03032
[8] Blass, A., A game semantics for linear logic, Ann. pure and applied logic., 56, 183-220, (1992) · Zbl 0763.03008
[9] Brandstädt, A.; Le, V.B.; Spinrad, J.P., Graph classes: A survey, SIAM monographs on discr. math. & applic., (1999) · Zbl 0919.05001
[10] Brünnler, K. Deep inference and Symmetry in Classical Proofs. Ph.D. thesis, Dresden Technical University, September 2003. Revised March 2004
[11] Cook, S.A.; Reckhow, R.A., The relative efficiency of propositional proof systems, J. symb. logic, 44, 1, 36-50, (1979) · Zbl 0408.03044
[12] Corneil, D.G.; Lerchs, H.; Stewart-Burlingham, L., Complement reducible graphs, Discr. appl. math., 3, 163-174, (1981) · Zbl 0463.05057
[13] Danos, V. La Logique Linéaire Appliquée à l’étude de Divers Processus de Normalisation (Principalement du λ-Calcul). PhD thesis, U. Paris VII, June 1990
[14] Danos, V.; Joinet, J.-B.; Schellinx, H., A new deconstructive logic: linear logic, J. symb. logic, 62, 3, 755-807, (1997) · Zbl 0895.03023
[15] Danos, V.; Regnier, L., The structure of multiplicatives, Arch. math. logic, 28, 181-203, (1989) · Zbl 0689.03013
[16] Davydov, G.V., The synthesis of the resolution method and the inverse method, Zapiski nauchnykh seminarov lomi, J. sov. math., 1, 1, 12-18, (1973), Translation in · Zbl 0265.68044
[17] Devarajan, H., D.J.D. Hughes, G. Plotkin & V.R. Pratt. Full completeness of the multiplicative linear logic of Chu spaces. Proc. Logic in Comp. Sci. 1999 234-245
[18] Dosen, K.; Petric, Z., Proof-theoretical coherence, (2004), KCL Publications London · Zbl 1153.03003
[19] Eilenberg, S.; Kelly, G.M., A generalization of the functorial calculus, J. algebra, 3, 366-375, (1966) · Zbl 0146.02501
[20] Führmann, C. & D. Pym. On the Geometry of Interaction for Classical Logic. Proc. IEEE Symp. on Logic in Comp. Sci. (LICS 2004), 2004
[21] Führmann, C.; Pym, D., Order-enriched categorical models of the classical sequent calculus, J. pure and applied algebra, 204, 1, 21-78, (2006) · Zbl 1081.03068
[22] Gentzen, G.; Szabo, M.E., The collected papers of gerhard Gentzen, Mathematische zeitschrift, 39, 176-210, (1969), North-Holland, Translation in
[23] Girard, J.-Y., Linear logic, Th. comp. sci., 50, 1-102, (1987) · Zbl 0625.03037
[24] Girard, J.-Y., Towards a geometry of interaction, (), 69-108
[25] Girard, J.-Y., A new constructive logic: classical logic, Math. struc. comp. sci., 1, 255-296, (1991) · Zbl 0752.03027
[26] Girard, J.-Y., Proof-nets: the parallel syntax for proof theory. logic and algebra, Lec. notes in pure and applied math., 180, (1996)
[27] Gray, J.W., Fibred and cofibred categories, (), 21-83 · Zbl 0192.10701
[28] Grothendieck, A. Technique de descente et théorèmes d’existence en géométrie algébrique, I. Généralités. Descente par morphismes fidélement plats. Seminaire Bourbaki 190 1959-60 · Zbl 0229.14007
[29] Guerrini, S. Correctness of Multiplicative Proof Nets is Linear. Proc. Logic in Comp. Sci. 14 1999 454-463
[30] Kelly, G.M.; Mac Lane, S., Coherence in closed categories, Journal of pure and applied algebra, 1, 97-140, (1971) · Zbl 0212.35001
[31] Herbrand, J. Recherches sur la theorie de la demonstration. Ph.D. thesis, U. Paris 1930 · JFM 56.0824.02
[32] Hu, H., Contractible coherence spaces and maximal maps, Electr. notes theor. comp. sci., 20, (1999) · Zbl 0935.18001
[33] Hu, H.; Joyal, A., Coherence completions of categories and their enriched softness, Electr. notes theor. comp. sci., 6, (1997) · Zbl 0911.68111
[34] Hu, H.; Joyal, A., Coherence completions of categories, Th. comp. sci., 227, 1-2, 153-184, (1999) · Zbl 0974.03052
[35] Hughes, D.J.D. Proofs Without Syntax, submitted version, 20 August 2004. http://arxiv.org/abs/math/0408282 (v1)
[36] Hughes, D.J.D. Deep inference proof theory equals categorical proof theory minus coherence. Draft of October 6, 2004. Downloadable from http://boole.stanford.edu/ dominic/papers/di
[37] Hughes, D.J.D. Proofs Without Syntax. Annals of Mathematics 2006 (to appear), http://arxiv.org/abs/math/0408282 (v3). August 2004 submitted version also available: [35] · Zbl 1130.03009
[38] Hughes, D.J.D. & R.J. van Glabbeek. Proof nets for unit-free multiplicative additive linear logic (extended abstract). Proc. Logic in Computer Science ’03, 2003
[39] Hughes, D.J.D.; van Glabbeek, R.J., Proof nets for unit-free multiplicative-additive linear logic, ACM transactions of computational logic, (2005) · Zbl 1367.03111
[40] Hyland, J.M.E., Proof theory in the abstract, Ann. pure appl. logic, 114, 1-3, 43-78, (2002) · Zbl 1007.03056
[41] Hyland, J.M.E. Abstract interpretation of proofs: Classical propositional calculus. Proceedings of CSL 2004, ed. Marcinkowski & Tarlecki, 2004 · Zbl 1095.03059
[42] Joyal, A.; Street, R.; Verity, D., Traced monoidal categories, Math. proc. camb. phil. soc., 119, 447-468, (1996) · Zbl 0845.18005
[43] Ketonen, J.; Weyhrauch, R., A decidable fragment of predicate calculus, Th. comp. sci., 32, 297-307, (1984) · Zbl 0579.03007
[44] Lamarche, F.; Straßburger, L., Naming proofs in classical propositional logic, (), 246-261 · Zbl 1114.03005
[45] Lamarche, F. & L. Straßburger. Constructing free Boolean Categories. Proc. IEEE Symp. on Logic in Comp. Sci. (LICS 2005), 2005 · Zbl 1127.03044
[46] McKinley, R. Categorical models of first-order classical proofs. Ph.D. thesis, University of Bath, 2006
[47] de Oliviera, A.; de Queiroz, R., Geometry of deduction via graphs of proof, ()
[48] Poincaré, H., Analysis situs, J. ecole polytech, (1895) · JFM 26.0541.07
[49] Retoré, C., Perfect matchings and series-parallel graphs: multiplicative proof nets as R&B-graphs [extended abstract], Elec. notes in th. comp. sci., 3, 167-182, (1996)
[50] Retoré, C., Handsome proof-nets: perfect matchings and cographs, Th. comp. sci., 294, 473-488, (2003) · Zbl 1028.68154
[51] Robinson, E.P., Proof nets for classical logic, J. logic & computation, 13, 5, 777-797, (2003) · Zbl 1036.03037
[52] Seely, R.A.G., Linear logic, ∗-autonomous categories and cofree algebra, Contemporary math., 92, (1989) · Zbl 0674.03007
[53] Tait, W.W., A nonconstructive proof of Gentzen’s hauptstatz for second-order predicate logic, Bul. AMS, 72, 980-988, (1968) · Zbl 0199.00801
[54] Taylor, R.; Wiles, A., Ring-theoretic properties of certain Hecke algebras, Annals of mathematics, 141, 553-572, (1995) · Zbl 0823.11030
[55] Thiele, R., Hilbert’s twenty-fourth problem, Amer. math. monthly, (Jan 2003)
[56] Troelstra, A.S.; Schwichtenberg, H., Basic proof theory, Cambridge tracts in theoretical computer science, (1996), Cambridge University Press · Zbl 0868.03024
[57] Urquhart, A., The complexity of propositional proofs, Bull. symb. logic, 1, 4, 425-467, (1995) · Zbl 0845.03025
[58] Whitehead, G.W., Elements of homotopy theory, (1978), Springer · Zbl 0406.55001
[59] Wiles, A., Modular elliptic-curves and Fermat’s last theorem, Annnals of mathematics, 141, 443-551, (1995) · Zbl 0823.11029
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.