×

zbMATH — the first resource for mathematics

Some general results about proof normalization. (English) Zbl 1255.03050
Summary: In this paper, we provide a general setting under which results of normalization of proof trees such as, for instance, the logicality result in equational reasoning and the cut-elimination property in sequent or natural deduction calculi, can be unified and generalized. This is achieved by giving simple conditions which are sufficient to ensure that such normalization results hold, and which can be automatically checked since they are syntactical. These conditions are based on basic properties of elementary combinations of inference rules which ensure that the induced global proof tree transformation processes do terminate.
MSC:
03F05 Cut-elimination and normal-form theorems
03B22 Abstract deductive systems
03F07 Structure of proofs
Software:
CoCasl; Coq; Isabelle
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Aiguier, M., Arnould, A., Boin, C., Le Gall, P., Marre, B.: Testing from algebraic specifications: test data set selection by unfolding axioms. In: Grieskamp, W., Weise, C. (eds.) Formal Approaches to Testing of Software (FATES), Lecture Notes in Computer Science, vol. 3997, pp. 304–317. Springer (2005) · Zbl 1183.68175
[2] Aiguier, M., Arnould, A., Le Gall, P., Longuet, D.: Test selection criteria for quantifier-free first-order specifications. In: Arbab, F., Sirjani, M. (eds.) International Symposium on Fundamentals of Software ENgineering (FSEN), Lecture Notes in Computer Science, vol. 4767, pp. 144–160. Springer (2007) · Zbl 1141.68447
[3] Aiguier M., Bahrami D.: Structures for abstract rewriting. J. Automat. Reason. 38(4), 303–351 (2007) · Zbl 1125.03011 · doi:10.1007/s10817-006-9065-7
[4] Aiguier, M., Bahrami, D., Dubois, C.: On a generalised logicality theorem. In: Artificial Intelligence, Automated Reasoning, and Symbolic Computation, Lecture Notes in Artificial Intelligence, vol. 2385, pp. 51–64. Springer (2002) · Zbl 1072.68536
[5] Aiguier M., Barbier F.: An institution-independent proof of the Beth definability theorem. Studi. Logica 85(3), 333–359 (2007) · Zbl 1134.03043 · doi:10.1007/s11225-007-9043-z
[6] Aiguier M., Diaconescu R.: Stratified institutions and elementary homomorphisms. Inform. Process. Lett. 103(1), 5–13 (2007) · Zbl 1189.03038 · doi:10.1016/j.ipl.2007.02.005
[7] Aiguier, M., Longuet, D.: Test selection criteria for modal specifications of reactive systems. In: Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 159–170. IEEE Computer Society (2007) · Zbl 1141.68447
[8] Baader, F., Nipkow, T.: Term Rewriting and All That. C.U. Press (1998) · Zbl 0948.68098
[9] Belnap N.D.: Display logic. J. Philos. Logic 11, 375–417 (1982) · Zbl 0509.03008
[10] Berger U., Eberl M., Schwichtenberg H.: Term rewriting for normalization by evaluation. Inform. Comput. 183, 19–42 (2003) · Zbl 1054.68078 · doi:10.1016/S0890-5401(03)00014-2
[11] Birkhoff G.: On the structure of abstract algebras. Proc. Camb. Philos. Soc. 31, 433–454 (1935) · JFM 61.1026.07 · doi:10.1017/S0305004100013463
[12] Bittar, E.T.: Strong normalization proofs for cut-elimination in Gentzen’s sequent calculi. In: Proceedings of the Symposium on Algebra and Computer Science, Helena Rasiowa in Memoriam, vol. 46, pp. 179–225. Banach Center Publication (1999) · Zbl 0945.03083
[13] Borzyszkowski T.: Logical systems for structured specifications. Theor. Comput. Sci. 286, 197–245 (2002) · Zbl 1061.68104 · doi:10.1016/S0304-3975(01)00317-6
[14] Cichon, E.-A., Rusinowitch, M., Selhab, S.: Cut elimination and rewriting: termination proofs. Technical report, INRIA-Lorraine, Nancy, France (1996)
[15] Cornes, C., Courant, J., Fillâtre, J.-C., Huet, G., Manoury, P., Munoz, C., Murthy, C., Parent, C., Paulin-Mohring, Ch., Sabi, A., Werner, B.: The Coq proof assistant reference manual, version 5.10. Technical Report 177, INRIA, July (1995)
[16] Dawson, J., Gore, R.: A new machine-checked proof of strong normalisation for display logic. In: Harland, J. (ed.) Electronic Notes in Theoretical Computer Science, vol. 78. Elsevier (2003) · Zbl 1270.03119
[17] Dawson, J.-E., Goré, R.: A general theorem on termination of rewriting. In: Computer Science Logic (CSL’04), vol. 3210 of Lecture Notes in Computer Science, pp. 100–114. Springer (2004) · Zbl 1095.68046
[18] Dawson, J.-E., Goré, R.: Termination of abstract reduction systems computing. In: The Australian Theory Symposium, 2007 (CATS 2007), Conferences in Research and Practice in Information Technology (CRPIT), vol. 65, pp. 35–43. Australian Computer Society (2007)
[19] Dershowitz N.: A note on simplification orderings. Inform. Process. Lett. 9(5), 212–215 (1979) · Zbl 0433.68044 · doi:10.1016/0020-0190(79)90071-1
[20] Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Formal Models and Semantics, vol. B: pp. 243–320. Elsevier (1990) · Zbl 0900.68283
[21] Dershowitz, N., Kirchner, C.: Abstract saturation-based inference. In: Kolaitis, P. (ed.) Proceedings of the Annual Symposium on Logic in Computer Science. IEEE Publiser Society (2003)
[22] Dershowitz N., Kirchner C.: Abstract canonical presentations. Theor. Comput. Sci. 357(1–3), 53–69 (2006) · Zbl 1099.03047 · doi:10.1016/j.tcs.2006.03.012
[23] Diaconescu, R.: Institution-independent Model Theory. Studies in Universal Logic. Birkhuser (2008) · Zbl 1144.03001
[24] Diaconescu, R., Goguen, J., Stefaneas, P.: Logical support for modularization. In: Huet, G., Plotkin, G. (eds.) Logical Environments, pp. 83–130. Proceedings of Workshop on Logical Frameworks (1991)
[25] Dowek, G.: Confluence as a cut-elimination property. In: Nieuwenhuis, R. (ed.) Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 2706, pp. 2–14. Springer (2003) · Zbl 1038.03054
[26] Dowek G., Hardin Th., Kirchner C.: Theorem proving modulo. J. Automat. Reason. 31, 33–72 (2003) · Zbl 1049.03011 · doi:10.1023/A:1027357912519
[27] Dowek, G., Werner, B.: An inconsistent theory modulo defined by a confluent and terminating rewrite system. Available at www.lix.polytechnique.fr/\(\sim\)dowek/
[28] Dowek, G., Werner, B.: Proof normalization modulo. In: International Workshop on Types for Proofs and Programs, pp. 62–77. Springer, London, UK (1999) · Zbl 0944.03052
[29] Dowek G., Werner B.: Proof normalization modulo. J. Symb. Logic 68(4), 1289–1316 (2003) · Zbl 1059.03062 · doi:10.2178/jsl/1067620188
[30] Dragalin, A.-G.: Mathematical intuitionism, introduction to proof theory. Transl. Math. Monogr. 67, 185–199. Translation of the russian original from 1979 (1988)
[31] Fiadeiro, J., Sernadas, A.: Structuring theories on consequence. In: Recent Trends in Algebraic Development Techniques, Lecture Notes in Computer Science, vol. 332, pp. 44–72. Springer (1988)
[32] Gallier, J.-H.: Logic for Computer Science, Volume Foundations of Automatic Theorem Proving. Harper & Row (1986) · Zbl 0605.03004
[33] Gentzen, G.: Untersuchungen ber das logische schlieen. Mathematische Zeitschrift 39(176–210): 405–431 (1935). English translation In: Szabo, M.-E. (ed.) The collected Papers of Gerhard Gentzen, pp. 68–131, North-Holland (1969)
[34] Girard J.-Y.: Linear logic. Theor. Comput. Sci. 50, 1–102 (1987) · Zbl 0625.03037 · doi:10.1016/0304-3975(87)90045-4
[35] Girard J.-Y., Lafont Y., Taylor P.: Proofs and Types. Cambridge University Press, Cambridge (1989) · Zbl 0671.68002
[36] Goguen J.A., Burstall R.-M.: Institutions: Abstract model theory for specification and programming. J. ACM 39(1), 95–146 (1987) · Zbl 0799.68134 · doi:10.1145/147508.147524
[37] Herbelin, H.: A \(\lambda\)-calculus structure isomorphic to Gentzen-style sequent calculus structure. In: Pacholski, L., Tiuryn, J. (eds.) Proceedings of the 8th International Workshop on Computer Science Logic, Lecture Notes in Computer Science, vol. 933, pp. 61–75. Springer (1995) · Zbl 1044.03509
[38] Hermant, O.: A model-based cut elimination proof. In: 2nd St-Petersburg Days of Logic and Computability (2003)
[39] Hermant, O.: Semantic cut elmination in the intuitionistic sequent calculus. In: Urzyczyn, P. (ed.) International Conference on Typed Lambda Calculi and Applications (TLCA), Lecture Notes in Computer Science, vol. 3461, pp. 221–233. Springer (2007) · Zbl 1114.03044
[40] Kaplan S.: Conditional rewrite rules. Theor. Comput. Sci. 33, 175–193 (1984) · Zbl 0577.03013 · doi:10.1016/0304-3975(84)90087-2
[41] Kleene S.-C.: Introduction to Meta-mathematics. North-Holland, Amsterdam (1952) · Zbl 0047.00703
[42] Levy J., Agustí J.: Bi-rewrite systems. J. Symb. Comput. 22, 279–314 (1996) · Zbl 0865.68070 · doi:10.1006/jsco.1996.0053
[43] Longuet, D., Aiguier, M.: Specification-based testing for CoCasl’s modal specifications. In: Mossakowski, T., Montanari, U., Haveraaen, M. (eds.) Conference on Algebra and Coalgebra in Computer Science (CALCO), Lecture Notes in Computer Science, vol. 4624, pp. 356–371. Springer (2007) · Zbl 1214.68231
[44] Longuet, D., Aiguier, M.: Integration testing from structured specifications via deduction modulo. In: International Colloquium on Theoretical Aspects of Computing (2009, To appear). · Zbl 1250.68195
[45] Longuet, D., Aiguier, M., Le Gall, P.: Proof-guided test selection from first-order specifications with equality. J. Automat. Reason. (2009) To appear · Zbl 1214.68221
[46] Meseguer, J.: General logics. In: Logic Colloquium’87, pp. 275–329. Holland (1989) · Zbl 0691.03001
[47] Nipkow, T., Paulson, L., Wenzel, M.: Isabelle’s logics: HOL. http://isabelle.in.tum.de/doc/logics-HOL.pdf · Zbl 0994.68131
[48] Prawitz D.: Natural Deduction: A Proof-Theoretical Study. Almqvist and Wiksell, Stockholm (1965) · Zbl 0173.00205
[49] Salibra, A., Scollo, G.: Compactness and Löwenheim-Skolem properties in categories of pre-institutions. In: Rauszer, C. (ed.) Algebraic Methods in Logic and in Computer Science, Banach Center Publ. vol. 28, pp. 67–94 (1993) · Zbl 0792.03026
[50] Salibra A., Scollo G.: Interpolation and compactness in categories of pre-institutions. Math. Struct. Comput. Sci. 6, 261–286 (1996) · Zbl 0860.03035 · doi:10.1017/S0960129500001006
[51] Schorlemmer, W.M.: Term rewriting in a logic of special relations. In: 7th International Conference on Algebraic Methodology and Software Technology, Lecture Notes in Computer Science, vol. 1548, pp. 178–195. Springer (1998) · Zbl 0924.03048
[52] Struth, G.: Non-symmetric rewriting. Technical report, MPI für Informatik (1996)
[53] Tait, W.-W.: Normal derivability in classical logic. In: Barwise, J. (ed.) The Syntax and Semantics of Infinitary Languages, pp. 204–236. Springer (1989)
[54] Tarlecki A.: On the existence of free models in abstract algebraic institutions. Theor. Comput. Sci. 37, 269–304 (1986) · Zbl 0608.68014 · doi:10.1016/0304-3975(85)90094-5
[55] Tarlecki A.: Quasi-varieties in abstract algebraic institutions. J. Comput. Syst. Sci. 33(3), 269–304 (1986) · Zbl 0622.68033
[56] Tarlecki, A.: Algebraic Foundations of Systems Specification, Chapter Institutions: An Abstract Framework for Formal Specifications, pp. 105–131. IFIP State-of-the-Art Reports. Springer (1999)
[57] Urban C., Bierman G.-M.: Strong normalisation of cut-elimination in classical logic. Acta Informaticae 45(1–2), 123–155 (2001) · Zbl 0982.03032
[58] van Oostrom, V.: Sub-Birkhoff. In: 7th International Symposium on Functional and Logic Programming, Lecture Notes in Computer Science, vol. 2998, pp. 180–195. Springer (2004) · Zbl 1122.68461
[59] Wallen, L.-A.: Automated Deduction for Non Classical Logics. The MIT Press (1990) · Zbl 0782.03003
[60] Yamada T., Avenhaus J., Loria-Saenz C., Middeldorp A.: Logicality of conditional rewrite systems. Theor. Comput. Sci. 236(1,2), 209–232 (2000) · Zbl 0938.68050 · doi:10.1016/S0304-3975(99)00210-8
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.