zbMATH — the first resource for mathematics

A semantic framework for proof evidence. (English) Zbl 1425.68371
Summary: Theorem provers produce evidence of proof in many different formats, such as proof scripts, natural deductions, resolution refutations, Herbrand expansions, and equational rewritings. In implemented provers, numerous variants of such formats are actually used: consider, for example, such variants of or restrictions to resolution refutations as binary resolution, hyper-resolution, ordered-resolution, paramodulation, etc. We propose the foundational proof certificates (FPC) framework for defining the semantics of a broad range of proof evidence. This framework allows both producers of proof certificates and the checkers of those certificates to have a clear formal definition of the semantics of a wide variety of proof evidence. Employing the FPC framework will allow one to separate a proof from its provenance and to allow anyone to construct their own proof checker for a given style of proof evidence. The foundation on which FPC relies is that of proof theory, particularly recent work into focused proof systems: such proof systems provide protocols by which a checker extracts information from the certificate (mediated by the so called clerks and experts) as well as performs various deterministic and non-deterministic computations. While we shall limit ourselves to first-order logic in this paper, we shall not limit ourselves in many other ways. The FPC framework is described for both classical and intuitionistic logics and for proof structures as diverse as resolution refutations, natural deduction, Frege proofs, and equality proofs.

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
Full Text: DOI
[1] Andreoli, J-M, Logic programming with focusing proofs in linear logic, J. Log. Comput., 2, 297-347, (1992) · Zbl 0764.03020
[2] Armand, M., Faure, G., Grégoire, B., Keller, C., Théry, L., Werner, B.: A modular integration of SAT/SMT solvers to Coq through proof witnesses. In: Jouannaud, J.-P., Shao, Z. (eds.) Certified Programs and Proofs (CPP 2011), LNCS 7086, pp. 135-150 (2011) · Zbl 1350.68223
[3] Baelde, D, Least and greatest fixed points in linear logic, ACM Trans. Comput. Log., 13, 1-48, (2012) · Zbl 1352.03072
[4] Barendregt, H, The impact of the lambda calculus in logic and computer science, Bull. Symb. Log., 3, 181-215, (1997) · Zbl 0887.03008
[5] Barendregt, H; Barendsen, E, Autarkic computations in formal proofs, J. Autom. Reason., 28, 321-336, (2002) · Zbl 1002.68156
[6] Barendregt, HP, Introduction to generalized type systems, J. Funct. Program., 1, 125-154, (1991) · Zbl 0931.03019
[7] Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, New York (2004) · Zbl 1069.68095
[8] Blanco, R., Miller, D.: Proof outlines as proof certificates: a system description. In: Cervesato, I., Schürmann, C. (eds.) Proceedings First International Workshop on Focusing, Suva, Fiji, 23rd November 2015, volume 197 of Electronic Proceedings in Theoretical Computer Science, pp. 7-14. Open Publishing Association (2015)
[9] Boespflug, M., Carbonneaux, Q., Hermant, O.: The \(λ {\varPi }\)-calculus modulo as a universal proof language. In: Pichardie, D., Weber, T. (eds.) Proceedings of PxTP2012: Proof Exchange for Theorem Proving, pp. 28-43 (2012)
[10] Böhme, S., Weber, T.: Designing proof formats: a user’s perspective. In: Fontaine, P., Stump, A. (eds.) PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, pp 27-32 (2011) · Zbl 0644.03033
[11] Chaudhuri, K.: Classical and intuitionistic subexponential logics are equally expressive. In: Dawar, A., Veith, H. (eds.) CSL 2010: Computer Science Logic. LNCS 6247, Brno, Czech Republic, pp. 185-199. Springer (2010) · Zbl 1287.03057
[12] Chaudhuri, K; Hetzl, S; Miller, D, A multi-focused proof system isomorphic to expansion proofs, J. Log. Comput., 26, 577-603, (2016) · Zbl 1403.03118
[13] Chaudhuri, K., Miller, D., Saurin, A.: Canonical sequent proofs via multi-focusing. In: Ausiello, G., Karhumäki, J., Mauri, G., Ong, L. (eds.) Fifth International Conference on Theoretical Computer Science, IFIP 273, pp. 383-396. Springer (2008)
[14] Chaudhuri, K; Pfenning, F; Price, G, A logical characterization of forward and backward chaining in the inverse method, J. Autom. Reason., 40, 133-177, (2008) · Zbl 1151.03006
[15] Chihani, Z.: Certification of first-order proofs in classical and intuitionistic logics. Ph.D. thesis, Ecole Polytechnique (2015) · Zbl 0408.03044
[16] Chihani, Z., Libal, T., Reis, G.: The proof certifier checkers. In: Nivelle, H.D. (ed.) Proceedings of the 24th Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), LNCS 9323, pp. 201-210. Springer (2015) · Zbl 06519943
[17] Chihani, Z., Miller, D.: Proof certificates for equality reasoning. In: Benevides, M., Thiemann, R. (eds.) Post-proceedings of LSFA 2015: 10th Workshop on Logical and Semantic Frameworks, with Applications. Natal, Brazil, ENTCS 18612 (2016)
[18] Chihani, Z., Miller, D., Renaud, F.: Checking foundational proof certificates for first-order logic (extended abstract). In: Blanchette, J.C., Urban, J. (eds.) Third International Workshop on Proof Exchange for Theorem Proving (PxTP 2013), volume 14 of EPiC Series, pp. 58-66. EasyChair (2013) · Zbl 1381.68261
[19] Chihani, Z., Miller, D., Renaud, F.: Foundational proof certificates in first-order logic. In: Bonacina, M.P. (ed.) CADE 24: Conference on Automated Deduction 2013, LNAI 7898, pp. 162-177 (2013) · Zbl 1381.68261
[20] Chihani, Z., Miller, D., Renaud, F.: Supporting \(λ \)Prolog code. http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/fpc-support.tar (2016) · Zbl 1273.68329
[21] Chomsky, N, Three models for the description of language, IRE Trans. Inf. Theory, 2, 113-124, (1956) · Zbl 0156.25401
[22] Church, A, A formulation of the simple theory of types, J. Symb. Log., 5, 56-68, (1940) · JFM 66.1192.06
[23] Cook, SA; Reckhow, RA, The relative efficiency of propositional proof systems, J. Symb. Log., 44, 36-50, (1979) · Zbl 0408.03044
[24] Cousineau, D., Dowek, G.: Embedding pure type systems in the lambda-Pi-calculus modulo. In: Rocca, S.R.D. (ed.) Proceedings of the Typed Lambda Calculi and Applications, 8th International Conference, TLCA 2007, Paris, France, 26-28 June 2007, LNCS 4583, pp. 102-117. Springer (2007) · Zbl 1215.03021
[25] Danos, V; Joinet, J-B; Schellinx, H; Girard, J-Y (ed.); Lafont, Y (ed.); Regnier, L (ed.), LKT and LKQ: sequent calculi for second order logic based upon dual linear decompositions of classical implication, No. 222, 211-224, (1995), Cambridge · Zbl 0829.03031
[26] Bruijn, NG, Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with an application to the church-rosser theorem, Indag. Math., 34, 381-392, (1972) · Zbl 0253.68007
[27] Delande, O; Miller, D; Saurin, A, Proof and refutation in MALL as a game, Ann. Pure Appl. Log., 161, 654-672, (2010) · Zbl 1257.03090
[28] Dowek, G.: Skolemization in simple type theory: the logical and the theoretical points of view. In: Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on His 70th Birthday, number 17 in Studies in Logic, pp. 244-255. College Publications (2008) · Zbl 0156.25401
[29] Dowek, G; Hardin, T; Kirchner, C, HOL-\(λ σ \) an intentional first-order expression of higher-order logic, Math. Struct. Comput. Sci., 11, 1-25, (2001) · Zbl 0972.03012
[30] Dowek, G; Hardin, T; Kirchner, C, Theorem proving modulo, J. Autom. Reason., 31, 31-72, (2003) · Zbl 1049.03011
[31] Dunchev, C., Guidi, F., Coen, C.S., Tassi, E.: ELPI: fast, embeddable, \(λ \)Prolog interpreter. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning—20th International Conference, LPAR-20 2015, Suva, Fiji, 24-28 November 2015, pp. 460-468 (2015) · Zbl 06528800
[32] Dyckhoff, R; Lengrand, S, Call-by-value \(λ \)-calculus and LJQ, J. Log. Comput., 17, 1109-1134, (2007) · Zbl 1133.03030
[33] Felty, A; Huet, G (ed.); Plotkin, GD (ed.), Transforming specifications in a dependent-type lambda calculus to specifications in an intuitionistic logic, (1991), Cambridge
[34] Felty, A.: Encoding the calculus of constructions in a higher-order logic. In: Vardi, M. (ed.) 8th Symposium on Logic in Computer Science, pp. 233-244. IEEE (1993)
[35] Felty, A, Implementing tactics and tacticals in a higher-order logic programming language, J. Autom. Reason., 11, 43-81, (1993) · Zbl 0783.68117
[36] Fontaine, P., Marion, J.-Y., Merz, S., Nieto, L.P., Tiu, A.F.: Expressiveness + automation + soundness: towards combining SMT solvers and interactive proof assistants. In: Hermanns, H., Palsberg, J. (eds.) TACAS: Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, LNCS 3920, pp. 167-181. Springer (2006) · Zbl 1180.68240
[37] Gallier, J.H.: Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row, New York (1986) · Zbl 0605.03004
[38] Gelder, AV, Producing and verifying extremely large propositional refutations: have your cake and eat it too, Ann. Math. Artif. Intell., 65, 329-372, (2012) · Zbl 1273.68329
[39] Gentzen, G; Szabo, ME (ed.), Investigations into logical deduction, 68-131, (1935), Amsterdam
[40] Gentzen, G.: Die widerspruchfreiheit der reinen zahlentheorie. Math. Ann. 112, 493-565 (1936). Reprinted in English translation as “The consistency of Elementary Number Theory” in The collected papers of Gerhard Gentzen, M. E. Szabo, ed · Zbl 0014.38801
[41] Girard, J-Y, Linear logic, Theoret. Comput. Sci., 50, 1-102, (1987) · Zbl 0625.03037
[42] Girard, J-Y, A new constructive logic: classical logic, Math. Struct. Comp. Sci., 1, 255-296, (1991) · Zbl 0752.03027
[43] Girard, J.-Y., Taylor, P., Lafont, Y.: Proofs and Types. Cambridge University Press, Cambridge (1989) · Zbl 0671.68002
[44] Gödel, K.: Zur intuitionistischen arithmetik und zahlentheorie. Ergeb. Eines Math. Kolloqu. 34-38 (1932). English translation in The Undecidable (M. Davis, ed.) 75-81 (1965)
[45] Gödel, K.: Eine interpretation des intuitionistischen aussagenkalkuls. Ergeb. Eines Math. Kolloqu. 4, 39-40 (1933). Available in “Kurt Gödel: Collected Works. Volume 1” edited by S. Feferman and et al
[46] Gordon, M; Plotkin, GD (ed.); Stirling, C (ed.); Tofte, M (ed.), From LCF to HOL: a short history, 169-186, (2000), Cambridge
[47] Gordon, M.J., Milner, A.J., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation, LNCS 78. Springer, New York (1979) · Zbl 0421.68039
[48] Harper, R; Honsell, F; Plotkin, G, A framework for defining logics, J. ACM, 40, 143-184, (1993) · Zbl 0778.03004
[49] Heath, Q., Miller, D.: A framework for proof certificates in finite state exploration. In: Kaliszyk, C., Paskevich, A. (eds.) Proceedings of the Fourth Workshop on Proof eXchange for Theorem Proving, number 186 in Electronic Proceedings in Theoretical Computer Science, pp. 11-26. Open Publishing Association (2015) · Zbl 0625.03037
[50] Herbelin, H.: Séquents qu’on calcule: de l’interprétation du calcul des séquents comme calcul de lambda-termes et comme calcul de stratégies gagnantes. Ph.D. thesis, Université Paris 7 (1995)
[51] Hodges, W; Zalta, EN (ed.), Logic and games, (2013), Stanford
[52] Honsell, F., Lenisa, M., Liquori, L., Maksimovic, P., Scagnetto, I.: LFP: a logical framework with external predicates. In: Chlipala, A., Schürmann, C. (eds.) LFMTP 2012: Proceedings of the Seventh International Workshop on Logical Frameworks and Meta-Languages, Theory and Practice, pp. 13-22. ACM, New York (2012) · Zbl 1352.68061
[53] Howe, J.M.: Proof search issues in some non-classical logics. Ph.D. thesis, University of St Andrews (1998). Available as University of St Andrews Research Report CS/99/1
[54] Hughes, DJD, Proofs without syntax, Ann. Math., 143, 1065-1076, (2006) · Zbl 1130.03009
[55] Hurd, J.: The OpenTheory standard theory library. In: Bobaru, M.G., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) The Third International Symposium on NASA Formal Methods, LNCS 6617, pp. 177-191 (2011) · Zbl 0783.68117
[56] Johnson, S.C.: Yacc: Yet Another Compiler-Compiler, vol. 32. Bell Laboratories, Murray Hill (1975)
[57] Kahn, G.: Natural semantics. In: Brandenburg, F.-J., Vidal-Naquet, G., Wirsing, M. (eds.) Proceedings of the Symposium on Theoretical Aspects of Computer Science, LNCS 247, pp. 22-39. Springer (1987) · Zbl 0635.68007
[58] Kolmogorov, A N, On the principle of the excluded middle, Mat. Sb., 32, 646-667, (1925)
[59] Laurent, O.: Etude de la polarisation en logique. Ph.D. thesis, Université Aix-Marseille II (2002) · Zbl 0887.03008
[60] Liang, C; Miller, D, Focusing and polarization in linear, intuitionistic, and classical logics, Theoret. Comput. Sci., 410, 4747-4768, (2009) · Zbl 1187.68528
[61] Liang, C; Miller, D, A focused approach to combining logics, Ann. Pure Appl. Log., 162, 679-697, (2011) · Zbl 1225.03086
[62] Lorenzen, P.: Ein dialogisches konstruktivitätskriterium. In: Infinitistic Methods: Proceedings of the Symposium on the Foundations of Mathematics, pp. 193-200. PWN (1961) · Zbl 0679.68173
[63] Miller, D, A compact representation of proofs, Stud. Log., 46, 347-370, (1987) · Zbl 0644.03033
[64] Miller, D.: Communicating and trusting proofs: the case for broad spectrum proof certificates. In: Schroeder-Heister, P., Hodges, W., Heinzmann, G., Bour, P.E. (eds.) Logic, Methodology, and Philosophy of Science. Proceedings of the Fourteenth International Congress, pp. 323-342. College Publications (2014) · Zbl 1366.03100
[65] Miller, D; Falaschi, M (ed.), Proof checking and logic programming, 3-17, (2015), New York · Zbl 1362.68055
[66] Miller, D., Nadathur, G.: Programming with Higher-Order Logic. Cambridge University Press, Cambridge (2012) · Zbl 1267.68014
[67] Miller, D; Nadathur, G; Pfenning, F; Scedrov, A, Uniform proofs as a foundation for logic programming, Ann. Pure Appl. Log., 51, 125-157, (1991) · Zbl 0721.03037
[68] Miller, D; Saurin, A; Duparc, J (ed.); Henzinger, TA (ed.), From proofs to focused proofs: a modular proof of focalization in linear logic, 405-419, (2007), New York · Zbl 1179.03064
[69] Miller, D., Volpe, M.: Focused labeled proof systems for modal logic. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), LNCS 9450, pp. 266-280. Springer (2015) · Zbl 06528787
[70] Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (Revised). The MIT Press, Cambridge (1997)
[71] Nadathur, G., Mitchell, D.J.: System description: Teyjus—a compiler and abstract machine based implementation of \(λ \)Prolog. In: Ganzinger, H. (ed.) 16th Conference on Automated Deduction (CADE), LNAI 1632, pp. 287-291. Springer, Trento (1999) · Zbl 1403.03118
[72] Necula, G.C., Rahul, S.P.: Oracle-based checking of untrusted software. In: Hankin, C., Schmidt, D. (eds.) 28th ACM Symposium on Principles of Programming Languages, pp. 142-154 (2001) · Zbl 1323.68222
[73] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic. LNCS 2283. Springer, New York (2002) · Zbl 0994.68131
[74] Paulson, LC, The foundation of a generic theorem prover, J. Autom. Reason., 5, 363-397, (1989) · Zbl 0679.68173
[75] Pereira, F.C.N., Shieber, S.M.: Prolog and Natural-Language Analysis, vol. 10. CLSI, Stanford (1987) · Zbl 0684.68010
[76] Pfenning, F., Schürmann, C.: System description: Twelf—a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) 16th Conference on Automated Deduction (CADE), LNAI 1632, pp. 202-206. Springer, Trento (1999)
[77] Plotkin, G.D.: A Structural Approach to Operational Semantics. DAIMI FN-19. Aarhus University, Aarhus (1981)
[78] Plotkin, GD, The origins of structural operational semantics, J. Log. Algebraic Program., 60, 3-15, (2004) · Zbl 1072.68063
[79] Prawitz, D.: Natural Deduction. Almqvist & Wiksell, Uppsala (1965) · Zbl 0173.00205
[80] Qi, X., Gacek, A., Holte, S., Nadathur, G., Snow, Z.: The Teyjus system—version 2. http://teyjus.cs.umn.edu/ (2015) · Zbl 1049.03011
[81] Rabe, F.: The future of logic: foundation-independence. Log. Universalis. 10(1), 1-20 (2016) · Zbl 1436.03179
[82] Saillard, R.: Towards explicit rewrite rules in the \(λ {\varPi }\)-calculus modulo. In: Schulz, S., Sutcliffe, G., Konev, B. (eds.) IWIL-10th International Workshop on the Implementation of Logics, (2013) · Zbl 1187.68528
[83] Schwichtenberg, H; Wiedijk, F (ed.), Minlog, 151-157, (2006), New York
[84] Shieber, SM; Schabes, Y; Pereira, FCN, Principles and implementation of deductive parsing, J. Log. Program., 24, 3-36, (1995) · Zbl 0866.68062
[85] Slaney, J, Solution to a problem of ono and komori, J. Philos. Log., 18, 103-111, (1989) · Zbl 0671.03036
[86] Snow, Z., Baelde, D., Nadathur, G.: A meta-programming approach to realizing dependently typed logic programming. In: Kutsia, T., Schreiner, W., Fernández, M. (eds.) ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP), pp. 187-198 (2010)
[87] Stoy, J.E.: Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge (1977) · Zbl 0503.68059
[88] Stump, A.: Proof checking technology for satisfiability modulo theories. Electron. Notes Theor. Comput. Sci. 228, 121-133 (2009) · Zbl 1072.68063
[89] Stump, A; Oe, D; Reynolds, A; Hadarean, L; Tinelli, C, SMT proof checking using a logical framework, Form. Methods Syst. Des., 42, 91-118, (2013) · Zbl 1284.68521
[90] Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory, 2nd edn. Cambridge University Press, Cambridge (2000) · Zbl 0957.03053
[91] Wetzler, N; Heule, MJH; Hunt, JWA; Sinz, C (ed.); Egly, U (ed.), DRAT-trim: efficient checking and trimming using expressive clausal proofs, 422-429, (2014), New York · Zbl 1423.68475
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.