×

zbMATH — the first resource for mathematics

From LCF to Isabelle/HOL. (English) Zbl 1427.68349
Summary: Interactive theorem provers have developed dramatically over the past four decades, from primitive beginnings to today’s powerful systems. Here, we focus on Isabelle/HOL and its distinctive strengths. They include automatic proof search, borrowing techniques from the world of first order theorem proving, but also the automatic search for counterexamples. They include a highly readable structured language of proofs and a unique interactive development environment for editing live proof documents. Everything rests on the foundation conceived by Robin Milner for Edinburgh LCF: a proof kernel, using abstract types to ensure soundness and eliminate the need to store proofs. Compared with the research prototypes of the 1970s, Isabelle is a practical and versatile tool. It is used by system designers, mathematicians and many others.

MSC:
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
68-03 History of computer science
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Antoy, S.; Hanus, M., Functional logic programming, Commun ACM, 53, 4, 74-85 (2010)
[2] Arthan, R., On definitions of constants and types in HOL, J Autom Reason, 56, 3, 205-219 (2016) · Zbl 1356.68173
[3] Aspinall D (2000) Proof general: a generic tool for proof development. In: Graf S, Schwartzbach M (eds) European joint conferences on theory and practice of software (ETAPS), vol 1785 of LNCS. Springer · Zbl 0971.68627
[4] Ballarin C (2006) Interpretation of locales in Isabelle: theories and proof contexts. In: Borwein JM, Farmer WM (eds) 5th international conference mathematical knowledge management, MKM 2006, vol 4108 of Lecture notes in computer science. Springer, pp 31-43 · Zbl 1188.68258
[5] Ballarin, C., Locales: a module system for mathematical theories, J Autom Reason, 52, 2, 123-153 (2014) · Zbl 1315.68218
[6] Barwise J (1977) An introduction to first-order logic. In: Barwise J (ed) Handbook of mathematical logic. North-Holland, pp 5-46
[7] Bancerek, G.; Bylinski, C.; Grabowski, A.; Kornilowicz, A.; Matuszewski, R.; Naumowicz, A.; Pak, K., The role of the mizar mathematical library for interactive proof development in Mizar, J Autom Reason, 61, 1-4, 9-32 (2018) · Zbl 1433.68530
[8] Berghofer S, Bulwahn L, Haftmann F (2009) Turning inductive into equational specifications. In: Berghofer S, Nipkow T, Urban C, Wenzel M (eds) Theorem proving in higher order logics, vol 5674 of LNCS. Springer, pp 131-146 · Zbl 1252.68249
[9] Blanchette JC, Bulwahn L, Nipkow T (2011) Automatic proof and disproof in Isabelle/HOL. In: Tinelli C, Sofronie- Stokkermans V (eds) Frontiers of combining systems (FroCoS 2011), vol 6989 of LNCS. Springer, pp 12-27 · Zbl 1348.68214
[10] Blanchette, Jc; Böhme, S.; Paulson, Lc, Extending Sledgehammer with SMT solvers, J Autom Reason, 51, 1, 109-128 (2013) · Zbl 1314.68272
[11] Bertot Y, Castéran P (2004) Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions. Springer · Zbl 1069.68095
[12] Bulwahn L, Krauss A, Haftmann F, Erkök L, Matthews J (2008) Imperative functional programming with Isabelle/HOL. In: Mohamed OA, Muñoz CA, Tahar S (eds) 21st international conference theorem proving in higher order logics, TPHOLs 2008. vol 5170 of Lecture notes in computer science. Springer, pp 134-149 · Zbl 1165.68352
[13] Brunner, J.; Lammich, P., Formal verification of an executable LTL model checker with partial order reduction, J Autom Reason, 60, 1, 3-21 (2018) · Zbl 1426.68162
[14] Blanchette JC (2012) Automatic proofs and refutations for higher-order logic. PhD thesis, Technical University Munich
[15] Blanchette, Jc, Relational analysis of (co)inductive predicates, (co)algebraic datatypes, and (co)recursive functions, Softw Qual J, 21, 1, 101-126 (2013)
[16] Boyer RS, Moore JS (1979) A computational logic. Academic Press
[17] Berghofer S, Nipkow T (2002) Executing higher order logic. In: Callaghan P, Luo Z, McKinna J, Pollack R (eds) Types for proofs and programs (TYPES 2000), vol 2277 of LNCS. Springer, pp 24-40 · Zbl 1054.68133
[18] Berghofer S, Nipkow T (2004) Random testing in Isabelle/HOL. In: Cuellar J, Liu Z (eds) Software engineering and formal methods (SEFM 2004). IEEE Computer Society, pp 230-239
[19] Blanchette JC,NipkowT (2010)Nitpick: a counterexample generator for higher-order logic based on a relationalmodel finder. In: Kaufmann M, Paulson LC (eds) Interactive theorem proving, vol 6172 of LNCS. Springer, pp 131-146
[20] Bulwahn L (2012) Counterexample generation for higher-order logic using functional and logic programming. PhD thesis, Technical University Munich · Zbl 1352.68039
[21] Bulwahn L (2012) The new quickcheck for Isabelle: random, exhaustive and symbolic testing under one roof. In: Hawblitzel C, Miller D (eds) Certified programs and proofs, vol 7679 of LNCS. Springer, pp 92-108 · Zbl 1383.68071
[22] Bulwahn L (2012) Smart testing of functional programs in Isabelle. In: Bjørner N, Voronkov A (eds) Logic for programming, artificial intelligence, and reasoning, vol 7180 of LNCS. Springer, pp 153-167 · Zbl 1352.68039
[23] Chamarthi HR, Dillinger PC, Kaufmann M, Manolios P (2011) Integrating testing and interactive theorem proving. In: Hardin D, Schmaltz J (eds) 10th international workshop on the ACL2 theorem prover and its applications, ACL2 2011, vol 70 of EPTCS, pp 4-19
[24] Claessen K, Hughes J (2000) QuickCheck: a lightweight tool for random testing of Haskell programs. In: Odersky M, Wadler P (eds) Fifth ACM SIGPLAN international conference on functional programming (ICFP ’00). ACM, pp 268-279
[25] Clocksin WF, Mellish CS (1987) Programming in prolog, 3rd edn. Springer
[26] Dybjer P, Haiyan Q, Takeyama M (2003) Combining testing and proving in dependent type theory. In: Theorem proving in higher order logics, vol 2758 of LNCS. Springer, pp 188-203
[27] Divasón J, Joosten SJC, Kuncar O, Thiemann R, Yamada A (2018) Efficient certification of complexity proofs: formalizing the Perron-Frobenius theorem (invited talk paper). In: Andronick J, Felty AP (eds) 7th ACM SIGPLAN international conference on certified programs and proofs, CPP 2018. ACM, pp 2-13
[28] Divasón, J.; Joosten, Sjc; Thiemann, R.; Yamada, A., A verified implementation of the Berlekamp-Zassenhaus factorization algorithm (2019), J Autom Reason: Published online, J Autom Reason
[29] de Moura L, Bjørner N (2008) Z3: an efficient SMT solver. In: Ramakrishnan C, Rehof J (eds) Tools and algorithms for the construction and analysis of systems, vol 4963 of Lecture notes in computer science. Springer, pp 337-340
[30] de Moura, L.M., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The Lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) Automated deduction-CADE-25. Lecture notes in computer science, vol. 9195, pp. 378-388. Springer (2015) · Zbl 1465.68279
[31] Debray, Sk; Warren, Ds, Automatic mode inference for logic programs, J Log Program, 5, 3, 207-229 (1988) · Zbl 0647.68010
[32] Eberl M (2015) A decision procedure for univariate real polynomials in Isabelle/HOL. In: 2015 conference on certified programs and proofs, CPP ’15. ACM, pp 75-83
[33] Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.: A fully verified executable LTL model checker. In: Sharygina, N., Veith, H. (eds.) 25th international conference computer aided verification, CAV 2013. Lecture notes in computer science, vol. 8044, pp. 463-478. Springer (2013)
[34] Futatsugi, K.; Goguen, Ja; Jouannaud, J-P; Meseguer, J., Principles of OBJ2, 12th ACM SIGACT-SIGPLAN symposium on principles of programming languages (POPL), 52-66 (1985), USA. ACM: New York, NY, USA. ACM
[35] Giesl, J.; Aschermann, C.; Brockschmidt, M.; Emmes, F.; Frohn, F.; Fuhs, C.; Hensel, J.; Otto, C.; Plücker, M.; Schneider-Kamp, P.; Ströder, T.; Swiderski, S.; Thiemann, R., Analyzing program termination and complexity automatically with AProVE, J Autom Reason, 58, 1, 3-31 (2017) · Zbl 1409.68255
[36] Griffioen, D., Huisman, M.: A comparison of PVS and Isabelle/HOL. In: Grundy, J., Newey, M. (eds.) Theorem proving in higher order logics: TPHOLs ’98, pp. 123-142. Springer (1998)
[37] Gomes, Victor B. F.; Kleppmann, Martin; Mulligan, Dominic P.; Beresford, Alastair R., Verifying strong eventual consistency in distributed systems, Proceedings of the ACM on Programming Languages, 1, OOPSLA, 1-28 (2017)
[38] Grabowski, A.; Korniłowicz, A.; Naumowicz, A., Four decades of Mizar, J Autom Reason, 55, 3, 191-198 (2015) · Zbl 1336.00111
[39] Gordon MJC, Melham TF (eds) (1993) Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press
[40] Gonthier, G., Mahboubi, A.: An introduction to small scale reflection in Coq. J Formaliz Reason 3(2), (2010) · Zbl 1211.68368
[41] Gordon MJC, Milner R, Wadsworth CP (1979) Edinburgh LCF: a mechanised logic of computation. LNCS 78. Springer
[42] Goguen, J.A.: Some design principles and theory for OBJ-O, a language to express and execute algebraic specification for programs. In: Blum, E.K., Paul, M., Takasu, S. (eds.) Mathematical studies of information processing, vol 75 of LNCS, pp. 425-473. Springer (1979)
[43] Gordon, M.J.C.: Why higher-order logic is a good formalism for specifying and verifying hardware. In: Milne, G., Subrahmanyam, P.A. (eds.) Formal aspects of VLSI design, pp. 153-177. North-Holland (1986)
[44] Gordon, M.J.C.: From LCF to HOL: a short history. In: Plotkin, G., Stirling, C., Tofte, M. (eds.) Proof, language, and interaction: essays in honor of Robin Milner, pp. 169-185. MIT Press (2000)
[45] Gordon, M. J. C., Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’, Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, 373, 2039, 20140234 (2015) · Zbl 1353.68250
[46] Hales, T.; Adams, M.; Bauer, G.; Dang, Td; Harrison, J.; Hoang, Lt; Kaliszyk, C.; Magron, V.; Mclaughlin, S.; Nguyen, Tt, A formal proof of the Kepler conjecture, Forum Math Pi, 5, e2 (2017) · Zbl 1379.52018
[47] Haftmann F (2009) Code generation from specifications in higher order logic. PhD thesis, Technische Universität München
[48] Harrison, J.: HOL light: a tutorial introduction. In: Srivas, M.K., Camilleri, A.J. (eds.) Formal methods in computer-aided design: FMCAD ’96, LNCS 1166, pp. 265-269. Springer (1996)
[49] Harper, R.; Honsell, F.; Plotkin, G., A framework for defining logics, J ACM, 40, 1, 143-184 (1993) · Zbl 0778.03004
[50] Hölzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in Isabelle/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) 4th international conference interactive theorem proving, LNCS 7998, pp. 279-294. Springer (2013) · Zbl 1317.68213
[51] Haftmann, F., Krauss, A., Kunčar, O., Nipkow, T.: Data refinement in Isabelle/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) 4th international conference interactive theorem proving, vol 7998 of LNCS, pp. 100-115. Springer (2013) · Zbl 1317.68212
[52] Hunt, Warren A.; Kaufmann, Matt; Moore, J. Strother; Slobodova, Anna, Industrial hardware and software verification with ACL2, Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, 375, 2104, 20150399 (2017)
[53] Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) Functional and logic programming (FLOPS 2010), vol 6009 of LNCS, pp. 103-117. Springer (2010) · Zbl 1284.68131
[54] Hupel, L., Nipkow, T.: A verified compiler from Isabelle/HOL to CakeML. In: Ahmed, A. (ed.) European symposium on programming (ESOP 2018), vol 10801 of LNCS, pp. 999-1026. Springer (2018) · Zbl 1418.68045
[55] Hoffmann Christoph, M.; O’Donnell Michael, J., Programming with equations, ACM Trans Program Lang Syst, 4, 1, 83-112 (1982) · Zbl 0481.68008
[56] Holzmann, Gj, The model checker SPIN, IEEE Trans Softw Eng, 23, 5, 279-295 (1997)
[57] Huet, Gp, A unification algorithm for typed \(\lambda \)-calculus, Theor Comput Sci, 1, 27-57 (1975) · Zbl 0337.68027
[58] Haftmann, F., Wenzel, M.: Constructive type classes in Isabelle. In: Altenkirch, T., McBride, C. (eds.) Types for proofs and programs, vol 4502 of LNCS, pp. 160-174. Springer (2006) · Zbl 1178.68529
[59] Haftmann, F., Wenzel, M.: Local theory specifications in Isabelle/Isar. In: Berardi, S., Damiani, F., de Liguoro, U. (eds.) Types for proofs and programs, TYPES 2008, vol 5497 of LNCS. Springer (2009) · Zbl 1246.68197
[60] Jackson D (2006) Software abstractions. Logic, language, and analysis. MIT Press
[61] Klein, G.; Andronick, J.; Elphinstone, K.; Heiser, G.; Cock, D.; Derrin, P.; Elkaduwe, D.; Engelhardt, K.; Kolanski, R.; Norrish, M.; Sewell, T.; Tuch, H.; Winwood, S., sel4: formal verification of an operating-system kernel, Commun ACM, 53, 6, 107-115 (2010)
[62] Kalvala S (1991) HOL around the world. In: Archer M, Joyce JJ, Levitt KN, Windley PJ (eds) International workshop on the HOL theorem proving system and its applications. IEEE Computer Society, pp 4-12
[63] Kumar R, Myreen MO, Norrish M, Owens S (2014) CakeML: a verified implementation of ML. In: Jagannathan S, Sewell P (eds) The 41st annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’14. ACM, pp 179-192 · Zbl 1284.68405
[64] Kunčar, Ondřej; Popescu, Andrei, Safety and conservativity of definitions in HOL and Isabelle/HOL, Proceedings of the ACM on Programming Languages, 2, POPL, 1-26 (2017)
[65] Kunčar, O.; Popescu, A., A consistent foundation for Isabelle/HOL, J. Autom Reason, 62, 4, 531-555 (2019) · Zbl 1465.68289
[66] Kammüller, F., Wenzel, M., Paulson, L.C.: Locales: a sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Thery, L. (eds.) Theorem proving in higher order logics: TPHOLs ’99, vol 1690 of LNCS. Springer (1999)
[67] Lammich, P.: Automatic data refinement. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) 4th international conference interactive theorem proving ITP 2013. Lecture notes in computer science, vol. 7998, pp. 84-99. Springer (2013) · Zbl 1317.68216
[68] Lammich, P.: Verified efficient implementation of Gabow’s strongly connected component algorithm. In: Klein, G., Gamboa, R. (eds.) 5th international conference interactive theorem proving ITP 2014. Lecture notes in computer science, vol. 8558, pp. 325-340. Springer (2014) · Zbl 1416.68168
[69] Lammich P (2016) Refinement based verification of imperative data structures. In: Avigad J, Chlipala A (eds) 5th ACM SIGPLAN conference on certified programs and proofs. ACM, pp 27-36
[70] Lammich, P.: Efficient verified (UN)SAT certificate checking. In: de Moura, L. (ed.) Automated deduction- CADE-26. Lecture notes in computer science, vol. 10395, pp. 237-254. Springer (2017) · Zbl 06778407
[71] Lammich, P., Refinement to imperative HOL, J Autom Reason, 62, 4, 481-503 (2019) · Zbl 1465.68291
[72] Lochbihler, A., Bulwahn, L.: Animating the formalised semantics of a Java-like language. In: van Eekelen Marko, C.J.D., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) Second international conference interactive theorem proving ITP 2011. Lecture notes in computer science, vol. 6898, pp. 216-232. Springer (2011) · Zbl 1342.68294
[73] Leroy, X., A formally verified compiler back-end, J Autom Reason, 43, 363-446 (2009) · Zbl 1185.68215
[74] Li, W.; Passmore, Go; Paulson, Lc, Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL, J Autom Reason, 62, 1, 69-91 (2019) · Zbl 07024052
[75] Larsen, Kg; Pettersson, P.; Yi, W., UPPAAL in a nutshell. STTT, 1, 1-2, 134-152 (1997) · Zbl 1060.68577
[76] Lammich, P.; Sefidgar, Sr, Formalizing network flow algorithms: a refinement approach in isabelle/hol, J Autom Reason, 62, 2, 261-280 (2019) · Zbl 07024459
[77] Lammich, P., Tuerk, T.: Applying data refinement for monadic programs to Hopcroft’s algorithm. In: Beringer, L., Felty, A.P. (eds.) Third international conference interactive theorem proving ITP, 2012. Lecture notes in computer science, vol. 7406, pp. 166-182. Springer (2012) · Zbl 1360.68757
[78] Milner, R.: The use of machines to assist in rigorous proof. In: Hoare, C.A.R., Shepherdson, J.C. (eds.) Mathematical logic and programming languages, pp. 77-88. Prentice-Hall (1985)
[79] Miller, D., A logic programming language with lambda-abstraction, function variables, and simple unification, J Log Comput, 1, 4, 497-536 (1991) · Zbl 0738.68016
[80] The Mizar Mathematical Library. http://mizar.org · Zbl 1278.68290
[81] Martin-Löf, P., Constructive mathematics and computer programming, Philos Trans R Soc Ser A, 312, 1522, 501-518 (1984) · Zbl 0552.03040
[82] Matichuk, Daniel; Murray, Toby; Wenzel, Makarius, Eisbach: A Proof Method Language for Isabelle, Journal of Automated Reasoning, 56, 3, 261-282 (2016) · Zbl 1356.68195
[83] Meng, J.; Quigley, C.; Paulson, Lc, Automation for interactive proof: first prototype, Inf Comput, 204, 10, 1575-1596 (2006) · Zbl 1103.68113
[84] Matthews D, Wenzel M (2010) Efficient parallel programming in Poly/ML and Isabelle/ML. In: ACM SIGPLAN workshop on declarative aspects of multicore programming (DAMP 2010)
[85] Nipkow T (1991) Higher-order critical pairs. In: Proceedings 6th IEEE symposium logic in computer science. IEEE Press, pp 342-349
[86] Nipkow, T.: Higher-order unification, polymorphism, and subsorts. In: Kaplan, S., Okada, M. (eds.) Proceedings 2nd international workshop conditional and typed rewriting systems, vol 516 of LNCS. Springer (1991)
[87] Nipkow T (1993) Functional unification of higher-order patterns. In: Proceedings 8th IEEE symposium logic in computer science, pp 64-74
[88] Nipkow T (1993) Order-sorted polymorphism in Isabelle. In: Huet G, Plotkin G (eds) Logical environments. Cambridge Uiversity Press, pp 164-188
[89] Nipkow T, Klein G (2014) Concrete semantics with Isabelle/HOL. Springer, 298 pp. http://concrete-semantics.org · Zbl 1410.68004
[90] Nagele, J., Middeldorp, A.: Certification of classical confluence results for left-linear term rewrite systems. In: Blanchette, J.C., Merz, S. (eds.) 7th international conference interactive theorem proving ITP, 2016. Lecture notes in computer science, vol. 9807, pp. 290-306. Springer (2016) · Zbl 06644750
[91] Nelson, G.; Oppen, Dc, Fast decision procedures based on congruence closure, J ACM, 27, 2, 356-364 (1980) · Zbl 0441.68111
[92] Nipkow, T., Paulson, L.C.: Isabelle-91. In: Kapur, D. (ed.) Automated deduction-CADE-11, vol 607 of LNCS, pp. 673-676. Springer (1992)
[93] Nipkow, T.; Prehofer, C., Type checking type classes, Principles of programming languages, POPL ’93, 409-418 (1993), USA. ACM: New York, NY, USA. ACM
[94] Nipkow T, Prehofer C (1998) Higher-order rewriting and equational reasoning. In: Bibel W, Schmitt P (eds) Automated deduction—a basis for applications. Volume I: foundations, vol 8 of Applied logic series. Kluwer, pp 399-430 · Zbl 0970.68081
[95] Nipkow T, Paulson LC, Wenzel M (2002) Isabelle/HOL: a proof assistant for higher-order logic. Springer, Online at http://isabelle.in.tum.de/dist/Isabelle/doc/tutorial.pdf · Zbl 0994.68131
[96] Nipkow, T., Snelting, G.: Type classes and overloading resolution via order-sorted unification. In: Hughes, J. (ed.) Proceedings 5th ACM conference functional programming languages and computer architecture, vol 523 of LNCS, pp. 1-14. Springer (1991)
[97] Obua, S.: Checking conservativity of overloaded definitions in higher-order logic. In: Pfenning, F. (ed.) Term rewriting and applications, vol 4098 of LNCS, pp. 212-226. Springer (2006) · Zbl 1151.68637
[98] O’Donnell MJ (1977) Computing in systems described by equations, vol 58 of LNCS. Springer
[99] Overbeek, R., An implementation of hyper-resolution, Comput Math Appl, 1, 201-214 (1975) · Zbl 0339.68060
[100] Owre S (2006) Random testing in PVS. In: Workshop on automated formal methods (AFM). http://fm.csl.sri.com/AFM06/papers/5-Owre.pdf
[101] Paulson, Lc, Natural deduction as higher-order resolution, J Log Program, 3, 237-258 (1986) · Zbl 0613.68035
[102] Paulson, Lc, The foundation of a generic theorem prover, J Autom Reson, 5, 3, 363-397 (1989) · Zbl 0679.68173
[103] Paulson, L.C.: Isabelle: the next 700 theorem provers. In: Odifreddi, P. (ed.) Logic and computer science, pp. 361-386. Academic Press (1990)
[104] Paulson LC (1993) Isabelle’s object-logics. Technical report 286, Cambridge University Computer Laboratory
[105] Paulson LC (1994) Isabelle—a generic theorem prover (with contributions by T. Nipkow), vol 828 of Lecture notes in computer science. Springer
[106] Paulson, Lc, The inductive approach to verifying cryptographic protocols, J Comput Secur, 6, 1-2, 85-128 (1998)
[107] Paulson, Lc, A generic tableau prover and its integration with Isabelle, J Univers Comput Sci, 5, 3, 73-87 (1999) · Zbl 0961.68116
[108] Paulson, Lawrence C., The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf, LMS Journal of Computation and Mathematics, 6, 198-248 (2003) · Zbl 1053.03009
[109] Paulson, Lc, Organizing numerical theories using axiomatic type classes, J Autom Reason, 33, 1, 29-49 (2004) · Zbl 1071.68092
[110] Paulson, Lawrence C., Computational logic: its origins and applications, Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences, 474, 2210, 20170872 (2018) · Zbl 1402.68160
[111] Peled, Da, Combining partial order reductions with on-the-fly model-checking, Form Methods Syst Des, 8, 1, 39-64 (1996) · Zbl 1425.68267
[112] Paulson, Lc; Grabczewski, K., Mechanizing set theory: cardinal arithmetic and the axiom of choice, J Autom Reason, 17, 3, 291-323 (1996) · Zbl 0868.03005
[113] Paraskevopoulou, Z., Hritcu, C., Dénès, M., Lampropoulos, L., Pierce, B.C.: Foundational property-based testing. In: Urban, C., Zhang, X. (eds.) Interactive theorem proving, vol 9236 of LNCS, pp. 325-343. Springer (2015) · Zbl 1465.68050
[114] Paulson, L.C., Susanto, K.W.: Source-level proof reconstruction for interactive theorem proving. In: Schneider, K., Brandt, J. (eds.) Theorem proving in higher order logics: TPHOLs 2007, LNCS 4732, pp. 232-245. Springer (2007) · Zbl 1144.68364
[115] Rajan SP (1993) Executing HOL specifications: towards an evaluation semantics for classical higher order logic. In: Claesen Luc JM, Gordon Michael JC (eds) Higher order logic theorem proving and its applications, vol A-20 of IFIP transactions. North-Holland/Elsevier, pp 527-536
[116] Runciman C, Naylor M, Lindblad F (2008) SmallCheck and lazy SmallCheck: automatic exhaustive testing for small values. In: Gill A (ed) Proceediong of the 1st ACM SIGPLAN symposium on Haskell. ACM, pp 37-48
[117] Robinson, Ja, A machine-oriented logic based on the resolution principle, J ACM, 12, 23-41 (1965) · Zbl 0139.12303
[118] Riazanov, A.; Voronkov, A., The design and implementation of VAMPIRE, AI Commun, 15, 2, 91-110 (2002) · Zbl 1021.68082
[119] Schulz S (2004) System description: E 0.81. In: Basin D, Rusinowitch M (eds) Automated reasoning—second international joint conference, IJCAR 2004, LNAI 3097. Springer, pp 223-228 · Zbl 1126.68578
[120] Shankar, N.: Little engines of proof. In: Eriksson, L.-H., Lindsay, P. (eds.) FME 2002: formal methods-getting IT right: international symposium of formal methods Europe, LNCS 2391, pp. 1-20. Springer (2002) · Zbl 1064.68558
[121] Siegel, Sf; Dillig, I.; Tasiran, S., What’s wrong with on-the-fly partial order reduction, Computer aided verification (CAV 2019) (2019), LNCS: Springer, LNCS
[122] Spiridonov A, Khurshid S (2007) Automatic generation of counterexamples for ACL2 using alloy. In: Seventh international workshop on the ACL2 theorem prover and its applications
[123] Slind K, Norrish M (2008) A brief overview of HOL4. In: Mohamed O, Muñoz C, Tahar S (eds) Theorem proving in higher order logics, TPHOLs 2008, pp 28-32 · Zbl 1165.68474
[124] Sumners R (2002) Checking ACL2 theorems via SAT checking. In: Third international workshop on the ACL2 theorem prover and its applications
[125] Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) Tools and algorithms for the construction and analysis of systems, vol 4424 of LNCS, pp. 632-647. Springer (2007) · Zbl 1186.68304
[126] Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) 22nd international conference theorem proving in higher order logics, TPHOLs 2009. Lecture notes in computer science, vol. 5674, pp. 452-468. Springer (2009) · Zbl 1252.68265
[127] Weber, T.: Bounded model generation for Isabelle/HOL. In: Ahrendt, W., Baumgartner, P., de Nivelle, H., Ranise, S., Tinelli, C. (eds.) Selected papers from the workshops on disproving and the second international workshop on pragmatics of decision procedures (PDPAR 2004), vol 125(3) of Electronic notes in theoretical computer science, pp. 103-116. Elsevier (2005) · Zbl 1271.68015
[128] Weber T (2008) SAT-based finite model generation for higher-order logic. PhD thesis, Technical University Munich, Germany
[129] Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of automated reasoning, vol II, chapter 27, pp 1965-2013. Elsevier Science (2001) · Zbl 1011.68129
[130] Wenzel Ma (1997) Type classes and overloading in higher-order logic. In: Theorem proving in higher order logics, vol 1275 of LNCS. Springer, pp 307-322
[131] Wenzel M (2007) Isabelle/Isar—a generic framework for human-readable proof documents. Stud Log Gramm Rhetor 10(23):277-297 From Insight to Proof—Festschrift in Honour of Andrzej Trybulec
[132] Wenzel, M.: Isabelle as document-oriented proof assistant. In: Davenport, J.H., et al. (eds.) Conference on intelligent computer mathematics (CICM 2011), vol 6824 of LNAI. Springer (2011) · Zbl 1335.68239
[133] Wenzel, Makarius, READ-EVAL-PRINT in Parallel and Asynchronous Proof-checking, Electronic Proceedings in Theoretical Computer Science, 118, 57-71 (2013)
[134] Wenzel, M.: Shared-memory multiprocessing for interactive theorem proving. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive theorem proving (ITP 2013). Lecture notes in computer science, vol. 7998. Springer (2013) · Zbl 1317.68235
[135] Wenzel, M.: Asynchronous user interaction and tool integration in Isabelle/PIDE. In: Klein, G., Gamboa, R. (eds.) Interactive theorem proving (ITP 2014), vol 8558 of LNCS. Springer (2014) · Zbl 1416.68182
[136] Wenzel M (2019) Interaction with formal mathematical documents in Isabelle/PIDE. In: Kaliszyk C, Brady E, Kohlhase A, Sacerdoti CC (eds) Intelligent computer mathematics (CICM 2019), vol 11617 of LNAI. Springer. https://arxiv.org/abs/1905.01735
[137] Wiedijk, F.; Boulton, Rj; Jackson, Pb, Mizar light for HOL light, Theorem proving in higher order logics, TPHOLs 2001, Berlin, Heidelberg, 378-393 (2001), Berlin: Springer, Berlin · Zbl 1005.68539
[138] Wimmer, S., Lammich, P.: Verified model checking of timed automata. In: Beyer, D., Huisman, M. (eds.) Tools and algorithms for the construction and analysis of systems, TACAS 2018. Lecture notes in computer science, vol. 10805, pp. 61-78. Springer (2018) · Zbl 1423.68294
[139] Wood C (2018) The strange numbers that birthed modern algebra. https://www.quantamagazine.org/the-strange-numbers-that-birthed-modern-algebra-20180906/
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.