diff --git a/thys/Boolos_Curious_Inference_Automated/Boolos_Curious_Inference_Automated.thy b/thys/Boolos_Curious_Inference_Automated/Boolos_Curious_Inference_Automated.thy new file mode 100644 --- /dev/null +++ b/thys/Boolos_Curious_Inference_Automated/Boolos_Curious_Inference_Automated.thy @@ -0,0 +1,170 @@ +section \Boolos Curious Proof Problem\ + +theory Boolos_Curious_Inference_Automated imports Main +begin (* sledgehammer_params[timeout=60] *) + +text\First declare a non-empty type @{term "i"} of objects (natural numbers in the context of this paper).\ +typedecl i + + +text \The signature for BCP consists of four uninterpreted constant symbols.\ +consts + e :: "i" ("\<^bold>e") \\one\ + s :: "i\i" ("\<^bold>s_") \\successor function\ + f :: "i\i\i" ("\<^bold>f__") \\binary function; axiomatised below as Ackermann function\ + d :: "i\bool" ("\<^bold>d_") \\arbitrary uninterpreted unary predicate\ + + +text \Axioms @{term "A1"}-@{term "A3"} model the Ackermann function and Axioms @{term "A4"} and @{term "A5"} +stipulate the properties of predicate @{term "d"}.\ +axiomatization where +A1: "\n. \<^bold>fn\<^bold>e = \<^bold>s\<^bold>e" and \\Axiom 1 for Ackermann function @{term "f"}\ +A2: "\y. \<^bold>f\<^bold>e\<^bold>sy = \<^bold>s\<^bold>s\<^bold>f\<^bold>ey" and \\Axiom 2 for Ackermann function @{term "f"}\ +A3: "\x y. \<^bold>f\<^bold>sx\<^bold>sy = \<^bold>fx\<^bold>f(\<^bold>sx)y" and \\Axiom 3 for Ackermann function @{term "f"}\ +A4: "\<^bold>d\<^bold>e" and \\@{term "d"} (an arbitrary predicate) holds for one\ +A5: "\x. \<^bold>dx \ \<^bold>d\<^bold>sx" \\if @{term "d"} holds for @{term "x"} it also holds for the successor of @{term "x"}\ + +text \Trying to prove automatically with \textit{Sledgehammer} @{cite Sledgehammer} that @{term "d"} holds +for fssssesssse still fails at this point. As Boolos' +explains, a naive first-order proof would require more modus ponens steps (with A5 and A4) than +there are atoms in the +universe.\ +lemma "\<^bold>d\<^bold>f\<^bold>s\<^bold>s\<^bold>s\<^bold>s\<^bold>e\<^bold>s\<^bold>s\<^bold>s\<^bold>s\<^bold>e" \\sledgehammer\ oops \\no proof found; timeout\ + +section \Automated Proof: Using Two Definitions\ + +text \We interactively provide two shorthand notations @{term "ind"} and @{term "p"}. After their +introduction a proof can be found fully automatically with \textit{Sledgehammer}. @{term "ind X"} +is defined to hold if +and only if @{term "X"} is `inductive' over @{term "e"} and @{term "s"}. + @{term "pxy"} holds if and only if @{term "pxy"} is in smallest inductive set +over @{term "e"} and @{term "s"}. +Note that the symbols @{term "ind"} and @{term "p"} do not occur in the BCP problem +statement.\ +definition ind ("\<^bold>i\<^bold>n\<^bold>d_") where "ind \ \X. X\<^bold>e \ (\x. X x \ X \<^bold>sx)" +definition p ("\<^bold>p_") where "p \ \x y. (\z::i. (\X. \<^bold>i\<^bold>n\<^bold>d X \ X z)) \<^bold>f x y" + +text \Using these definitions, state-of-art higher-order ATPs integrated with Isabelle/HOL can now fully +automatically prove Boolos' Curious Problem:\ +theorem "\<^bold>d\<^bold>f\<^bold>s\<^bold>s\<^bold>s\<^bold>s\<^bold>e\<^bold>s\<^bold>s\<^bold>s\<^bold>s\<^bold>e" \\@{term sledgehammer}\ (* + sledgehammer [z3] (* z3 found a proof... *) + sledgehammer [vampire] (* vampire found a proof... *) + sledgehammer [remote_leo2] (* remote_leo2 found a proof... *) + sledgehammer [e] (* e found a proof ... *) + sledgehammer [zipperposition] (* zipperposition found a proof... *) + sledgehammer [cvc4] (* No proof found *) + sledgehammer [verit] (* No proof found *) + sledgehammer [spass] (* No proof found *) + sledgehammer [remote_leo3] (* No proof found *) *) + by (metis A1 A2 A3 A4 A5 ind_def p_def) \\metis proof reconstruction succeeds\ + +text \In experiments (using a MacBook Pro (16-inch, 2019), 2,6 GHz 6-Core Intel Core i7, +16 GB 2667 MHz DDR4) running Isabelle2022 automatically found proofs were reported by various theorem +provers, including +@{term "Z3"} @{cite Z3}, +@{term "Vampire"} @{cite Vampire}, +@{term "Zipperposition"} @{cite Zipperpin}, +@{term "E"} @{cite Eprover}, +and Leo-II (@{term "remote_leo2"}) @{cite Leo2}.\ + +section \Automated Proof: Using a Single Definition\ + +definition p' ("\<^bold>p'_") where + "p' \ \x y. (\z::i. (\X. (X\<^bold>e \ (\x. X x \ X \<^bold>sx)) \ X z)) \<^bold>f x y" + +theorem "\<^bold>d\<^bold>f\<^bold>s\<^bold>s\<^bold>s\<^bold>s\<^bold>e\<^bold>s\<^bold>s\<^bold>s\<^bold>s\<^bold>e" \\@{term "sledgehammer (A1 A2 A3 A4 A5 p'_def)"}\ (* + sledgehammer[remote_leo2] (A1 A2 A3 A4 A5 p'_def) + \\sledgehammer [z3] (A1 A2 A3 A4 A5 p'\_def) (* z3 found a proof... *) + sledgehammer [vampire] (A1 A2 A3 A4 A5 p'\_def) (* vampire found a proof... *) + sledgehammer [remote\_leo2] (A1 A2 A3 A4 A5 p'\_def) (* remote\_leo2 found a proof... *) + sledgehammer [zipperposition] (A1 A2 A3 A4 A5 p'\_def) (* zipperposition found a proof... *) + sledgehammer [e] (A1 A2 A3 A4 A5 p'\_def) (* e found a proof ... *) + sledgehammer [cvc4] (A1 A2 A3 A4 A5 p'\_def) (* No proof found *) + sledgehammer [verit] (A1 A2 A3 A4 A5 p'\_def) (* No proof found *) + sledgehammer [spass] (A1 A2 A3 A4 A5 p'\_def) (* No proof found *) + sledgehammer [remote\_leo3] (A1 A2 A3 A4 A5 p'\_def) (* No proof found *)\ *) + by (smt A1 A2 A3 A4 A5 p'_def) \\smt proof reconstruction succeeds\ + +text \In experiments (using the same environment as above) several provers reported +proofs, including @{term "Z3"} and @{term "E"}.\ + + +section\Proof Reconstruction: E's Proof from @{cite BCI}\ +text \In this section we reconstruct and verify in Isabelle/HOL the proof argument found by E +as reported in @{cite BCI}. Analysing E's proof we can identify the following five lemmata:\ +lemma L1a: "\<^bold>i\<^bold>n\<^bold>d d" by (simp add: A4 A5 ind_def) +lemma L1b: "\x. \<^bold>px\<^bold>e" by (simp add: A1 ind_def p_def) +lemma L1c: "\<^bold>i\<^bold>n\<^bold>d \<^bold>p\<^bold>e" by (metis A2 L1b ind_def p_def) +lemma L2: "\x Y. (\<^bold>i\<^bold>n\<^bold>d \<^bold>px \ \<^bold>i\<^bold>n\<^bold>d \<^bold>p\<^bold>sx \ \<^bold>i\<^bold>n\<^bold>d Y) \ Y\<^bold>f\<^bold>sx\<^bold>s\<^bold>s\<^bold>s\<^bold>s\<^bold>e" by (metis ind_def p_def) +lemma L3: "\x. \<^bold>i\<^bold>n\<^bold>d \<^bold>px \ \<^bold>i\<^bold>n\<^bold>d \<^bold>p\<^bold>sx" by (metis A3 L1b ind_def p_def) + + +text \Using these lemmata E then constructs the following refutation argument:\ +theorem "\<^bold>d\<^bold>f\<^bold>s\<^bold>s\<^bold>s\<^bold>s\<^bold>e\<^bold>s\<^bold>s\<^bold>s\<^bold>s\<^bold>e" + proof - + { assume L4: "\\<^bold>d\<^bold>f\<^bold>s\<^bold>s\<^bold>s\<^bold>s\<^bold>e\<^bold>s\<^bold>s\<^bold>s\<^bold>s\<^bold>e" + have L5: "\\<^bold>i\<^bold>n\<^bold>d \<^bold>p\<^bold>s\<^bold>s\<^bold>s\<^bold>s\<^bold>e \ \\<^bold>i\<^bold>n\<^bold>d \<^bold>p\<^bold>s\<^bold>s\<^bold>s\<^bold>e" using L1a L1b L1c L2 L4 by blast + have L6: "\\<^bold>i\<^bold>n\<^bold>d \<^bold>p\<^bold>s\<^bold>s\<^bold>s\<^bold>e \ \\<^bold>i\<^bold>n\<^bold>d \<^bold>p\<^bold>s\<^bold>s\<^bold>e \ \\<^bold>i\<^bold>n\<^bold>d \<^bold>p\<^bold>s\<^bold>e" using L3 L5 by blast + have "False" using L1c L3 L6 by auto + } + then show ?thesis by blast + qed + +text \This refutation argument can alternatively be replaced by:\ +theorem "\<^bold>d\<^bold>f\<^bold>s\<^bold>s\<^bold>s\<^bold>s\<^bold>e\<^bold>s\<^bold>s\<^bold>s\<^bold>s\<^bold>e" + proof - + have L7: "\<^bold>i\<^bold>n\<^bold>d \<^bold>p\<^bold>s\<^bold>e" using L1c L3 by blast + have L8: "\<^bold>i\<^bold>n\<^bold>d \<^bold>p\<^bold>s\<^bold>s\<^bold>e" using L3 L7 by blast + have L9: "\<^bold>i\<^bold>n\<^bold>d \<^bold>p\<^bold>s\<^bold>s\<^bold>s\<^bold>e" using L3 L8 by blast + have L10: "\<^bold>i\<^bold>n\<^bold>d \<^bold>p\<^bold>s\<^bold>s\<^bold>s\<^bold>s\<^bold>e" using L3 L9 by blast + have L11: "(\<^bold>i\<^bold>n\<^bold>d \<^bold>p\<^bold>s\<^bold>s\<^bold>s\<^bold>e \ \<^bold>i\<^bold>n\<^bold>d \<^bold>p\<^bold>s\<^bold>s\<^bold>s\<^bold>s\<^bold>e \ \<^bold>i\<^bold>n\<^bold>d d)" using L10 L1a L9 by blast + then show ?thesis using L2 by blast +qed + + +text \Lemma @{term "L2"} can actually be simplified (this was also hinted at by an anonymous +reviewer of @{cite J63}):\ +lemma L2_1: "\x Y. (\<^bold>i\<^bold>n\<^bold>d \<^bold>px \ \<^bold>i\<^bold>n\<^bold>d Y) \ Y\<^bold>fx\<^bold>e" by (metis ind_def p_def) +lemma L2_2: "\x Y. (\<^bold>i\<^bold>n\<^bold>d \<^bold>px \ \<^bold>i\<^bold>n\<^bold>d Y) \ Y\<^bold>fx\<^bold>s\<^bold>e" by (metis ind_def p_def) +lemma L2_3: "\x Y. (\<^bold>i\<^bold>n\<^bold>d \<^bold>px \ \<^bold>i\<^bold>n\<^bold>d Y) \ Y\<^bold>fx\<^bold>s\<^bold>s\<^bold>e" by (metis ind_def p_def) +lemma L2_4: "\x Y. (\<^bold>i\<^bold>n\<^bold>d \<^bold>px \ \<^bold>i\<^bold>n\<^bold>d Y) \ Y\<^bold>fx\<^bold>s\<^bold>s\<^bold>s\<^bold>e" by (metis ind_def p_def) +lemma L2_5: "\x Y. (\<^bold>i\<^bold>n\<^bold>d \<^bold>px \ \<^bold>i\<^bold>n\<^bold>d Y) \ Y\<^bold>fx\<^bold>s\<^bold>s\<^bold>s\<^bold>s\<^bold>e" by (metis ind_def p_def) +text \etc.\ + +text \The following statement, however, has a countermodel.\ +lemma L2_1: "\x y Y. (\<^bold>i\<^bold>n\<^bold>d \<^bold>px \ \<^bold>i\<^bold>n\<^bold>d Y) \ Y\<^bold>f x y" + nitpick[user_axioms,expect=genuine] oops \\countermodel by nitpick\ + + + text \Instead of using @{term "L2"} we can now use @{term "L2_5"} in our proof of BCP from above:\ + +theorem "\<^bold>d\<^bold>f\<^bold>s\<^bold>s\<^bold>s\<^bold>s\<^bold>e\<^bold>s\<^bold>s\<^bold>s\<^bold>s\<^bold>e" + proof - + have L7: "\<^bold>i\<^bold>n\<^bold>d \<^bold>p\<^bold>s\<^bold>e" using L1c L3 by blast + have L8: "\<^bold>i\<^bold>n\<^bold>d \<^bold>p\<^bold>s\<^bold>s\<^bold>e" using L3 L7 by blast + have L9: "\<^bold>i\<^bold>n\<^bold>d \<^bold>p\<^bold>s\<^bold>s\<^bold>s\<^bold>e" using L3 L8 by blast + have L10: "\<^bold>i\<^bold>n\<^bold>d \<^bold>p\<^bold>s\<^bold>s\<^bold>s\<^bold>s\<^bold>e" using L3 L9 by blast + have L11: "(\<^bold>i\<^bold>n\<^bold>d \<^bold>p\<^bold>s\<^bold>s\<^bold>s\<^bold>e \ \<^bold>i\<^bold>n\<^bold>d \<^bold>p\<^bold>s\<^bold>s\<^bold>s\<^bold>s\<^bold>e \ \<^bold>i\<^bold>n\<^bold>d d)" using L10 L1a L9 by blast + then show ?thesis using L2_5 by blast +qed + + + +section\Conclusion\ +text \Isabelle/HOL data sources were provided in relation to @{cite J63}, which describes recent progress +and remaining challenges in automating Boolos' Curious Problem. +The interactive introduction of lemmas, as still exercised in @{cite KetlandAFP} and earlier +in @{cite BoolosOmegaMizar}, is no longer necessary, since higher-order theorem provers are +now able to speculate the required lemmas automatically, provided that appropriate shorthand +notations are provided (see the definitions of @{term "ind"} and @{term "p"}). + +Since Boolos' example for speeding up proofs is interesting in several respects, it is now being used as +an exercise in lecture courses at several universities (including University of Bamberg, University +of Greifswald, University of Luxembourg, Free University of Berlin); having our source files +permanently maintained in AFP hence makes sense.\ + +end + + + + diff --git a/thys/Boolos_Curious_Inference_Automated/ROOT b/thys/Boolos_Curious_Inference_Automated/ROOT new file mode 100644 --- /dev/null +++ b/thys/Boolos_Curious_Inference_Automated/ROOT @@ -0,0 +1,12 @@ +chapter AFP + +session "Boolos_Curious_Inference_Automated" (AFP) = HOL + + + options [timeout = 600] + + theories + Boolos_Curious_Inference_Automated + + document_files + "root.bib" + "root.tex" diff --git a/thys/Boolos_Curious_Inference_Automated/document/root.bib b/thys/Boolos_Curious_Inference_Automated/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/Boolos_Curious_Inference_Automated/document/root.bib @@ -0,0 +1,732 @@ +@inproceedings{IsabelleJEDIT, + author = {Makarius Wenzel}, + editor = {Johan Jeuring and + John A. Campbell and + Jacques Carette and + Gabriel Dos Reis and + Petr Sojka and + Makarius Wenzel and + Volker Sorge}, + title = {Isabelle/jEdit - {A} Prover {IDE} within the {PIDE} Framework}, + booktitle = {Intelligent Computer Mathematics - 11th International Conference, + {AISC} 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, + {DML} 2012, 11th International Conference, {MKM} 2012, Systems and + Projects, Held as Part of {CICM} 2012, Bremen, Germany, July 8-13, + 2012. Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = {7362}, + pages = {468--471}, + publisher = {Springer}, + year = {2012}, + url = {https://doi.org/10.1007/978-3-642-31374-5\_38}, + doi = {10.1007/978-3-642-31374-5\_38}, + timestamp = {Sun, 02 Jun 2019 21:23:46 +0200}, + biburl = {https://dblp.org/rec/conf/aisc/Wenzel12.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + + +@article{Sledgehammer, + title={Hammering towards {QED}}, + author={Blanchette, Jasmin C. and Kaliszyk, Cezary and Paulson, Lawrence C. and Urban, Josef}, + journal={Journal of Formalized Reasoning}, + volume={9}, + number={1}, + pages={101--148}, + year={2016} +} + + +@inproceedings{Z3, + author = {Leonardo Mendon{\c{c}}a de Moura and + Nikolaj S. Bj{\o}rner}, + editor = {C. R. Ramakrishnan and + Jakob Rehof}, + title = {{Z3:} An Efficient {SMT} Solver}, + booktitle = {Tools and Algorithms for the Construction and Analysis of Systems, + 14th International Conference, {TACAS} 2008, Held as Part of the Joint + European Conferences on Theory and Practice of Software, {ETAPS} 2008, + Budapest, Hungary, March 29-April 6, 2008. Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = {4963}, + pages = {337--340}, + publisher = {Springer}, + year = {2008}, + url = {https://doi.org/10.1007/978-3-540-78800-3\_24}, + doi = {10.1007/978-3-540-78800-3\_24}, + timestamp = {Thu, 14 Apr 2022 20:26:15 +0200}, + biburl = {https://dblp.org/rec/conf/tacas/MouraB08.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + + +@inproceedings{Vampire, + author = {Kotelnikov, Evgenii and Kov\'{a}cs, Laura and Reger, Giles and Voronkov, Andrei}, + title = {The Vampire and the FOOL}, + booktitle = {Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs}, + series = {CPP 2016}, + year = {2016}, + location = {St. Petersburg, FL, USA}, + pages = {37--48}, + numpages = {12}, + publisher = {ACM}, +} + + +@article{J63, + OPtdoi = {}, + author = {Benzmüller, Christoph and Fuenmayor, David and Steen, Alexander and Sutcliffe, Geoff}, + title = {Who Finds the Short Proof? An Exploration of Variants of {Boolos' Curious Inference} using Higher-order Automated Theorem Provers}, + journal = {Logic Journal of the IGPL}, + OPTnumber = {}, + OPTvolume = {}, + year = 2023, + note = {In print; arXiv preprint: \url{http://doi.org/10.48550/arXiv.2208.06879}}, +} + +@inproceedings{HeuleKB17, + author = {Marijn J. H. Heule and + Benjamin Kiesl and + Armin Biere}, + editor = {Leonardo de Moura}, + title = {Short Proofs Without New Variables}, + booktitle = {Automated Deduction - {CADE} 26 - 26th International Conference on + Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = {10395}, + pages = {130--147}, + publisher = {Springer}, + address = {Cham}, + year = {2017}, + doi = {10.1007/978-3-319-63046-5\_9}, + timestamp = {Thu, 29 Sep 2022 08:36:56 +0200}, + biburl = {https://dblp.org/rec/conf/cade/HeuleKB17.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@book{ComputationalLogic, + author = {Boyer, Robert S. and Moore, J. Strother}, + title = {A computational logic}, + series = {{ACM} monograph series}, + publisher = {Academic Press}, + address = {London}, + year = {1979} +} + +@article{BoolosCut, + year = {1984}, + number = {4}, + author = {George Boolos}, + publisher = {Springer}, + title = {Don't Eliminate Cut}, + doi = {10.1007/BF00247711}, + pages = {373--378}, + journal = {Journal of Philosophical Logic}, + volume = {13} +} + +@InProceedings{SST14old, + Author = {Stump, A. and Sutcliffe, G. and Tinelli, C.}, + Year = 2014, + Title = {{StarExec}: {A} Cross-Community Infrastructure for + Logic Solving}, + Editor = {Demri, S. and Kapur, D. and Weidenbach, C.}, + optbooktitle = {{IJCAR} 2014}, + BookTitle = {Proceedings of the 7th International Joint + Conference on Automated Reasoning}, + Series = {Lecture Notes in Artificial Intelligence}, + Number = 8562, + Pages = {367-373}, + Publisher = {Springer}, +} + +@inproceedings{SST14, + author = {Aaron Stump and + Geoff Sutcliffe and + Cesare Tinelli}, + editor = {St{\'{e}}phane Demri and + Deepak Kapur and + Christoph Weidenbach}, + title = {{StarExec}: {A} Cross-Community Infrastructure for Logic Solving}, + booktitle = {Automated Reasoning - 7th International Joint Conference, {IJCAR} + 2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna, + Austria, July 19-22, 2014. Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = {8562}, + pages = {367--373}, + publisher = {Springer}, + address = {Cham}, + year = {2014}, + opturl = {https://doi.org/10.1007/978-3-319-08587-6_28}, + doi = {10.1007/978-3-319-08587-6_28}, + timestamp = {Fri, 09 Apr 2021 18:50:53 +0200}, + biburl = {https://dblp.org/rec/conf/cade/StumpST14.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@Article{Sut22-IGPL, + Author = {Sutcliffe, Geoff}, + Year = 2022, + Title = {The Logic Languages of the {TPTP} World}, + Journal = {Logic Journal of the IGPL}, + url = {https://doi.org/10.1093/jigpal/jzac068}, + doi = {10.1093/jigpal/jzac068}, + Comment = "TPTPCite" +} + +@InProceedings{SB18, + Author = {Steen, Alexander and Benzm{\"u}ller, Christoph}, + Year = 2018, + Title = {The Higher-Order Prover {Leo-III}}, + Editor = {Galmiche, D. and Schulz, S. and Sebastiani, R.}, + BookTitle = {Proceedings of the 8th International Joint + Conference on Automated Reasoning}, + Series = {Lecture Notes in Artificial Intelligence}, + Number = 10900, + Pages = {108-116}, + Publisher = {Springer}, +} + +@InProceedings{KV13old, + Author = {Kovacs, Laura and Voronkov, Andrei}, + Year = 2013, + Title = {First-Order Theorem Proving and {Vampire}}, + Editor = {Sharygina, N. and Veith, H.}, + BookTitle = {Proceedings of the 25th International Conference on + Computer Aided Verification}, + optBooktitle = {{CAV} 2013}, + Series = {Lecture Notes in Artificial Intelligence}, + Number = 8044, + Pages = {1-35}, + Publisher = {Springer}, +} + +@inproceedings{KV13, + author = {Laura Kov{\'{a}}cs and + Andrei Voronkov}, + editor = {Natasha Sharygina and + Helmut Veith}, + title = {First-Order Theorem Proving and {Vampire}}, + booktitle = {Computer Aided Verification - 25th International Conference, {CAV} + 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = {8044}, + pages = {1--35}, + publisher = {Springer}, + address = {Berlin, Heidelberg}, + year = {2013}, + opturl = {https://doi.org/10.1007/978-3-642-39799-8_1}, + doi = {10.1007/978-3-642-39799-8_1}, + timestamp = {Tue, 14 May 2019 10:00:43 +0200}, + biburl = {https://dblp.org/rec/conf/cav/KovacsV13.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + + +@incollection{BoolosOmegaMizar, + Author = {Christoph Benzm{\"u}ller and Chad Brown}, + Booktitle = {From Insight to Proof -- Festschrift in Honour of + {Andrzej} {Trybulec}}, + Editor = {Roman Matuszewski and Anna Zalewska}, + Isbn = {978-83-7431-128-1}, + Keywords = {own, Proof Assistants, OMEGA, Interactive Proof, + Higher Order Logic}, + Pages = {299-388}, + Publisher = {The University of Bialystok}, + address = {Poland}, + OPTurl = {http://mizar.org/trybulec65/book.pdf}, + Series = {Studies in Logic, Grammar, and Rhetoric}, + Title = {The curious inference of {B}oolos in {MIZAR} and + {OMEGA}}, + url_preprint = {http://christoph-benzmueller.de/papers/B6.pdf}, + Volume = {10(23)}, + Year = 2007, + note = {\href{http://mizar.org/trybulec65/20.pdf}{http://mizar.org/trybulec65/20.pdf}}, +} + +@inproceedings{LostProof, + Address = {Siena, Italy}, + Author = {Christoph Benzm{\"u}ller and Manfred Kerber}, + Booktitle = {Proceedings of the IJCAR 2001 Workshop: Future + Directions in Automated Reasoning}, + Pages = {13-24}, + Title = {A Lost Proof}, + url_preprint = {http://christoph-benzmueller.de/papers/W13.pdf}, + url = {https://www.inf.ed.ac.uk/publications/online/0046/b040.pdf}, + Year = 2001, +} + +@article{BCI, + author = {George Boolos}, + title = {A curious inference}, + journal = {J. Philos. Log.}, + volume = 16, + number = 1, + pages = {1--12}, + year = 1987, + url = {https://doi.org/10.1007/BF00250612}, + doi = {10.1007/BF00250612}, + timestamp = {Mon, 11 May 2020 23:01:28 +0200}, + biburl = {https://dblp.org/rec/journals/jphil/Boolos87.bib}, + bibsource = {dblp computer science bibliography, + https://dblp.org} +} + +@article{ackermann1928, + title = "{Zum Hilbertschen Aufbau der reellen Zahlen}", + author = {Ackermann, Wilhelm}, + journal = {Mathematische Annalen}, + volume = 99, + number = 1, + pages = {118--133}, + year = 1928, + doi = {10.1007/BF01459088}, + publisher = {Springer-Verlag} +} + +@article{KetlandAFP, + author = {Jeffrey Ketland}, + title = {Boolos's Curious Inference in {Isabelle/HOL}}, + journal = {Archive of Formal Proofs}, + month = {June}, + year = 2022, + pages = {1-19}, + url = + {https://isa-afp.org/entries/Boolos_Curious_Inference.html}, + ISSN = {2150-914x}, + note = {\href{https://isa-afp.org/entries/Boolos_Curious_Inference.html}{https://isa-afp.org/entries/Boolos\_Curious\_Inference.html}}, +} + +@book{AndrewsOld, + author = {Peter B. Andrews}, + title = {An Introduction to Mathematical Logic and Type Theory -- To Truth Through Proof}, + series = {Computer science and applied mathematics}, + publisher = {Academic Press}, + year = 1986, + isbn = {978-0-12-058535-9}, + timestamp = {Thu, 14 Apr 2011 14:43:25 +0200}, + biburl = {https://dblp.org/rec/books/daglib/0070479.bib}, + bibsource = {dblp computer science bibliography, + https://dblp.org} +} + + +@book{Andrews, + title={An Introduction to Mathematical Logic and Type Theory}, + author={Andrews, P.B.}, + isbn={9781402007637}, + lccn={2002031656}, + doi = {10.1007/978-94-015-9934-4}, + series={Applied Logic Series}, + opturl={https://books.google.de/books?id=nV4zAsWAvT0C}, + year={2002}, + publisher={Springer}, + address = {Netherlands} +} + + +@inproceedings{Eprover, + author = {Stephan Schulz and Simon Cruanes and Petar + Vukmirovic}, + editor = {Pascal Fontaine}, + title = {Faster, Higher, Stronger: {E} 2.3}, + optbooktitle = "{Automated Deduction - {CADE} 27 - 27th International + Conference on Automated Deduction, Natal, Brazil, + August 27-30, 2019, Proceedings}", + booktitle = {{CADE} 2019}, + series = {Lecture Notes in Computer Science}, + volume = 11716, + pages = {495--507}, + publisher = {Springer}, + address = {Cham}, + year = 2019, + opturl = {https://doi.org/10.1007/978-3-030-29436-6_29}, + doi = {10.1007/978-3-030-29436-6_29}, + timestamp = {Sat, 19 Oct 2019 20:28:03 +0200}, + biburl = {https://dblp.org/rec/conf/cade/0001CV19.bib}, + bibsource = {dblp computer science bibliography, + https://dblp.org} +} + +@InCollection{GoedelProofLength, + title = {{Über die Länge von Beweisen}}, + author = {Kurt Gödel}, + booktitle = {{Ergebnisse} eines mathematischen {Kolloquiums}: {Heft} x7: 1934-1935}, + editor = {Menger, K. and G{\"o}del, K. and Wald, A.}, + opturl = {https://books.google.de/books?id=BENTtQEACAAJ}, + year = 1936, + pages = {23–24}, + publisher = {Franz Deuticke}, + address = {Vienna} +} + +@incollection{Omega, + Author = {Serge Autexier and Christoph Benzm{\"u}ller and + Dominik Dietrich and J\"org Siekmann}, + Booktitle = {Resource-Adaptive Cognitive Processes}, + Doi = {10.1007/978-3-540-89408-7_17}, + Editor = {Matthew W. Crocker and J\"org Siekmann}, + Isbn = {978-3-540-89407-0}, + Keywords = {own, Proof Assistants, OMEGA, Interactive Proof, + Automated Reasoning, Proof Planning, System + Integration, Agents}, + optNote = {(Final project report, DFG SFB 378)}, + Pages = {389-423}, + Publisher = {Springer}, + address = {Berlin, Heidelberg}, + Series = {Cognitive Technologies}, + Title = {{OMEGA}: Resource-Adaptive Processes in an Automated + Reasoning Systems}, + year = 2010, +} + +@inproceedings{Mizar, + author = {Grzegorz Bancerek and Czeslaw Bylinski and Adam + Grabowski and Artur Kornilowicz and Roman + Matuszewski and Adam Naumowicz and Karol Pak and + Josef Urban}, + editor = {Manfred Kerber and Jacques Carette and Cezary + Kaliszyk and Florian Rabe and Volker Sorge}, + title = {Mizar: State-of-the-art and Beyond}, + booktitle = {Intelligent Computer Mathematics - International + Conference, {CICM} 2015, Washington, DC, USA, July + 13-17, 2015, Proceedings}, + optbooktitle = {{CICM 2015}}, + series = {Lecture Notes in Computer Science}, + volume = 9150, + pages = {261--279}, + publisher = {Springer}, + address = {Cham}, + year = 2015, + opturl = {https://doi.org/10.1007/978-3-319-20615-8_17}, + doi = {10.1007/978-3-319-20615-8_17}, + timestamp = {Fri, 20 Nov 2020 16:08:54 +0100}, + biburl = {https://dblp.org/rec/conf/mkm/BancerekBGKMNPU15.bib}, + bibsource = {dblp computer science bibliography, + https://dblp.org} +} + +@book{Isabelle, + author = {Tobias Nipkow and Lawrence C. Paulson and Markus + Wenzel}, + title = {{Isabelle/HOL} - {A} Proof Assistant for Higher-Order + Logic}, + series = {Lecture Notes in Computer Science}, + volume = 2283, + publisher = {Springer}, + address = {Berlin, Heidelberg}, + year = 2002, + opturl = {https://doi.org/10.1007/3-540-45949-9}, + doi = {10.1007/3-540-45949-9}, + isbn = {3-540-43376-7}, + timestamp = {Tue, 14 May 2019 10:00:35 +0200}, + biburl = {https://dblp.org/rec/books/sp/NipkowPW02.bib}, + bibsource = {dblp computer science bibliography, + https://dblp.org} +} + +@article{THF, + Author = {Geoff Sutcliffe and Christoph Benzm{\"u}ller}, + Issn = {1972-5787}, + Journal = {Journal of Formalized Reasoning}, + Keywords = {own, Higher Order Logic, Automated Reasoning, Henkin + Semantics}, + Number = 1, + Pages = {1-27}, + Title = {Automated Reasoning in Higher-Order Logic using the + {TPTP THF} Infrastructure}, + url_preprint = {https://www.researchgate.net/publication/49595291}, + opturl = {https://jfr.unibo.it/article/view/1710}, + Volume = 3, + Year = 2010, + doi = {10.6092/issn.1972-5787/1710}, +} + +@inproceedings{ScienceOfReasoning, + author = {Alan Bundy}, + editor = {Jean{-}Louis Lassez and Gordon D. Plotkin}, + title = {A Science of Reasoning}, + booktitle = {Computational Logic - Essays in Honor of Alan + Robinson}, + pages = {178--198}, + publisher = {The {MIT} Press}, + address = {Cambridge, MA, USA}, + year = 1991, + note = {\href{https://mitpress.mit.edu/9780262121569/}{https://mitpress.mit.edu/9780262121569/}}, +} + +@article{SiekmannMelis, + author = {Erica Melis and J{\"{o}}rg H. Siekmann}, + title = {Knowledge-Based Proof Planning}, + journal = {Artificial Intelligence}, + volume = 115, + number = 1, + pages = {65--105}, + year = 1999, + opturl = {https://doi.org/10.1016/S0004-3702(99)00076-4}, + doi = {10.1016/S0004-3702(99)00076-4}, + timestamp = {Sat, 27 May 2017 14:24:42 +0200}, + biburl = {https://dblp.org/rec/journals/ai/MelisS99.bib}, + bibsource = {dblp computer science bibliography, + https://dblp.org} +} + +@article{Leo3, + Author = {Steen, Alexander and Benzm{\"u}ller, Christoph}, + title = {Extensional Higher-Order Paramodulation in {Leo-III}}, + journal = {Journal of Automated Reasoning}, + volume = 65, + number = 6, + pages = {775--807}, + year = 2021, + url = {https://doi.org/10.1007/s10817-021-09588-x}, + doi = {10.1007/s10817-021-09588-x} +} + +@inproceedings{CVC5, + author = {Haniel Barbosa and Clark W. Barrett and Martin Brain + and Gereon Kremer and Hanna Lachnitt and Makai Mann + and Abdalrhman Mohamed and Mudathir Mohamed and Aina + Niemetz and Andres N{\"{o}}tzli and Alex Ozdemir and + Mathias Preiner and Andrew Reynolds and Ying Sheng + and Cesare Tinelli and Yoni Zohar}, + editor = {Dana Fisman and Grigore Rosu}, + title = {cvc5: {A} Versatile and Industrial-Strength {SMT} + Solver}, + booktitle = {Tools and Algorithms for the Construction and + Analysis of Systems - 28th International Conference, + {TACAS} 2022, Held as Part of the European Joint + Conferences on Theory and Practice of Software, + {ETAPS} 2022, Munich, Germany, April 2-7, 2022, + Proceedings, Part {I}}, + optbooktitle = {{TACAS} 2022}, + series = {Lecture Notes in Computer Science}, + volume = 13243, + pages = {415--442}, + publisher = {Springer}, + address = {Cham}, + year = 2022, + opturl = {https://doi.org/10.1007/978-3-030-99524-9_24}, + doi = {10.1007/978-3-030-99524-9_24}, + timestamp = {Fri, 29 Apr 2022 14:50:36 +0200}, + biburl = + {https://dblp.org/rec/conf/tacas/BarbosaBBKLMMMN22.bib}, + bibsource = {dblp computer science bibliography, + https://dblp.org} +} + +@article{Ehoh, + author = {Petar Vukmirovic and Jasmin Blanchette and Simon + Cruanes and Stephan Schulz}, + title = {Extending a brainiac prover to lambda-free + higher-order logic}, + journal = {International Journal on Software Tools for Technology Transfer}, + volume = 24, + number = 1, + pages = {67--87}, + year = 2022, + opturl = {https://doi.org/10.1007/s10009-021-00639-7}, + doi = {10.1007/s10009-021-00639-7}, + timestamp = {Fri, 13 May 2022 19:53:01 +0200}, + biburl = + {https://dblp.org/rec/journals/sttt/VukmirovicBCS22.bib}, + bibsource = {dblp computer science bibliography, + https://dblp.org} +} + +@article{Zipperpin, + author = {Alexander Bentkamp and Jasmin Blanchette and Sophie + Tourret and Petar Vukmirovic and Uwe Waldmann}, + title = {Superposition with Lambdas}, + journal = {Journal of Automated Reasoning}, + volume = 65, + number = 7, + pages = {893--940}, + year = 2021, + opturl = {https://doi.org/10.1007/s10817-021-09595-y}, + doi = {10.1007/s10817-021-09595-y}, + timestamp = {Mon, 03 Jan 2022 22:07:16 +0100}, + biburl = + {https://dblp.org/rec/journals/jar/BentkampBTVW21.bib}, + bibsource = {dblp computer science bibliography, + https://dblp.org} +} + +@article{TPTP, + author = {Geoff Sutcliffe}, + title = {The {TPTP} Problem Library and Associated + Infrastructure - From {CNF} to {TH0}, {TPTP} v6.4.0}, + journal = {Journal of Automated Reasoning}, + volume = 59, + number = 4, + pages = {483--502}, + year = 2017, + url = {https://doi.org/10.1007/s10817-017-9407-7}, + doi = {10.1007/s10817-017-9407-7}, + timestamp = {Wed, 02 Sep 2020 13:30:01 +0200}, + biburl = {https://dblp.org/rec/journals/jar/Sutcliffe17.bib}, + bibsource = {dblp computer science bibliography, + https://dblp.org} +} + +@InCollection{SEP, + author = {Benzm{\"u}ller, Christoph and Andrews, Peter}, + title = {Church's Type Theory}, + booktitle = {The Stanford Encyclopedia of Philosophy}, + editor = {Edward N. Zalta}, + year = 2019, + edition = {Summer 2019}, + pages = {1--62 (in pdf version)}, + publisher = {Metaphysics Research Lab, Stanford University}, + address = {CA, USA}, + OPTurl = {https://plato.stanford.edu/entries/type-theory-church/}, + note = {\href{https://plato.stanford.edu/entries/type-theory-church/}{https://plato.stanford.edu/entries/type-theory-church/}} +} + +@article{PrimSubst, + Author = {Christoph Benzm{\"u}ller}, + Doi = {10.1023/A:1020840027781}, + Issn = {0039-7857}, + Journal = {Synthese}, + Keywords = {own, LEO Prover, Automated Reasoning, Higher Order + Logic, Henkin Semantics, ERIH PLUS, History of + Logic}, + Number = {1-2}, + Pages = {203-235}, + Title = {Comparing Approaches to Resolution based + Higher-Order Theorem Proving}, + url_preprint = {http://christoph-benzmueller.de/papers/J5.pdf}, + Volume = 133, + Year = 2002, +} + +@article{Andrews89, + author = {Peter B. Andrews}, + title = {On Connections and Higher-Order Logic}, + journal = {Journal of Automated Reasoning}, + volume = 5, + number = 3, + pages = {257--291}, + year = 1989, + opturl = {https://doi.org/10.1007/BF00248320}, + doi = {10.1007/BF00248320}, + timestamp = {Wed, 02 Sep 2020 13:30:04 +0200}, + biburl = {https://dblp.org/rec/journals/jar/Andrews89.bib}, + bibsource = {dblp computer science bibliography, + https://dblp.org} +} + +@inproceedings{Critique, + author = {Alan Bundy}, + editor = {Antonis C. Kakas and Fariba Sadri}, + title = {A Critique of Proof Planning}, + booktitle = {Computational Logic: Logic Programming and Beyond, + Essays in Honour of {Robert} {A.} {Kowalski}, Part {II}}, + series = {Lecture Notes in Computer Science}, + volume = 2408, + pages = {160--177}, + publisher = {Springer}, + address = {Berlin, Heidelberg}, + year = 2002, + opturl = {https://doi.org/10.1007/3-540-45632-5_7}, + doi = {10.1007/3-540-45632-5_7}, + timestamp = {Tue, 14 May 2019 10:00:52 +0200}, + biburl = {https://dblp.org/rec/conf/birthday/Bundy02.bib}, + bibsource = {dblp computer science bibliography, + https://dblp.org} +} + +@inproceedings{FreshStart, + Address = {Siena, Italy}, + Author = {Christoph Benzm{\"u}ller and Andreas Meier and Erica + Melis and Martin Pollet and Volker Sorge}, + Booktitle = {Proceedings of the {IJCAR} 2001 Workshop: Future + Directions in Automated Reasoning}, + Pages = {25-37}, + Title = {Proof Planning: A Fresh Start?}, + url_preprint = {http://christoph-benzmueller.de/papers/W12.pdf}, + Year = 2001, + note = {\href{https://www.researchgate.net/publication/319393675}{https://www.researchgate.net/publication/319393675}}, +} + +@inproceedings{LemmaDiscovery, + author = {Moa Johansson}, + editor = {Cezary Kaliszyk and Edwin C. Brady and Andrea + Kohlhase and Claudio Sacerdoti Coen}, + title = {Lemma Discovery for Induction - {A} Survey}, + booktitle = {Intelligent Computer Mathematics - 12th + International Conference, {CICM} 2019, Prague, Czech + Republic, July 8-12, 2019, Proceedings}, + optbooktitle = {{CICM} 2019}, + series = {Lecture Notes in Computer Science}, + volume = 11617, + pages = {125--139}, + publisher = {Springer}, + address = {Cham}, + year = 2019, + opturl = {https://doi.org/10.1007/978-3-030-23250-4_9}, + doi = {10.1007/978-3-030-23250-4_9}, + timestamp = {Sun, 21 Jun 2020 17:42:36 +0200}, + biburl = {https://dblp.org/rec/conf/mkm/Johansson19.bib}, + bibsource = {dblp computer science bibliography, + https://dblp.org} +} + +@article{Church40, + author = {Alonzo Church}, + title = {A Formulation of the Simple Theory of Types}, + journal = {Journal of Symbolic Logic}, + volume = 5, + number = 2, + pages = {56--68}, + year = 1940, + url = {https://doi.org/10.2307/2266170}, + doi = {10.2307/2266170}, + timestamp = {Wed, 14 Nov 2018 10:49:18 +0100}, + biburl = {https://dblp.org/rec/journals/jsyml/Church40.bib}, + bibsource = {dblp computer science bibliography, + https://dblp.org} +} + +@article{Leo2, + Author = {Christoph Benzm{\"u}ller and Nik Sultana and + Paulson, Lawrence C. and Frank Theiss}, + Doi = {10.1007/s10817-015-9348-y}, + Journal = {Journal of Automated Reasoning}, + publisher = {Springer Netherlands}, + Keywords = {own, Automated Reasoning, Interactive Proof, + Ontology Reasoning, LEO Prover, Higher Order Logic, + DFG-2501-Selected}, + Number = 4, + Pages = {389-404}, + Title = {The Higher-Order Prover {LEO-II}}, + url_preprint = {https://www.researchgate.net/publication/280986731}, + Volume = 55, + Year = 2015, +} + +@inproceedings{cvc4, + author = {Clark W. Barrett and + Christopher L. Conway and + Morgan Deters and + Liana Hadarean and + Dejan Jovanovic and + Tim King and + Andrew Reynolds and + Cesare Tinelli}, + editor = {Ganesh Gopalakrishnan and + Shaz Qadeer}, + title = {{CVC4}}, + booktitle = {Computer Aided Verification - 23rd International Conference, {CAV} + 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = {6806}, + pages = {171--177}, + publisher = {Springer}, + year = {2011}, + url = {https://doi.org/10.1007/978-3-642-22110-1\_14}, + doi = {10.1007/978-3-642-22110-1\_14}, + timestamp = {Tue, 27 Jul 2021 08:54:13 +0200}, + biburl = {https://dblp.org/rec/conf/cav/BarrettCDHJKRT11.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} diff --git a/thys/Boolos_Curious_Inference_Automated/document/root.tex b/thys/Boolos_Curious_Inference_Automated/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Boolos_Curious_Inference_Automated/document/root.tex @@ -0,0 +1,44 @@ +\documentclass[11pt,a4paper]{article} +\usepackage{isabelle,isabellesym} +\usepackage{amsmath,amssymb} +\usepackage{latexsym} + +% this should be the last package used +\usepackage{pdfsetup} +\usepackage{stmaryrd} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + + +\begin{document} + +\title{Automation of Boolos' Curious Inference in Isabelle/HOL} +\author{Christoph Benzmüller, David Fuenmayor, Alexander Steen and Geoff Sutcliffe} + +\maketitle + +\begin{abstract} + Boolos' Curious Inference is automated in Isabelle/HOL after interactive speculation of a suitable shorthand notation (one or two definitions). +\end{abstract} + +\tableofcontents + +% include generated text of all theories +\section{Introduction} +In his article \textit{A Curious Inference} \cite{BCI}, George Boolos discusses an example of the hyper-exponential speedup of proofs when moving from first-order logic to higher-order logic. The first-order proof problem he presents (hereafter called BCP, for Boolos' Curious Problem) has no short proof in first-order logic, but it has an elegant short proof in higher-order logic. + +The feasibility of interactive reconstructions of proofs of the BCP at the same level of proof granularity as exercised in Boolos' original paper was shown already one and half decades ago by Benzmüller and Brown~\cite{BoolosOmegaMizar}. Such an exercise has just recently been repeated in Isabelle/HOL by Ketland~\cite{KetlandAFP}. +However, as demonstrated in \cite{J63}, interactive proof for solving BCP is no longer needed, since proof automation in higher-order logic has progressed to the extent that short proofs for BCP can now be found by state-of-the-art higher-order automated theorem provers nearly fully automatically: the only extra human input is to provide one or two suitable shorthand notations. + +In this AFP paper, we provide Isabelle/HOL sources related to experiments performed in \cite{J63}, showing that interactive proof development for BCP (and related problems), as recently practiced by Ketland \cite{KetlandAFP}, can now be replaced by almost fully automated proofs. The availability of a powerful hammer tool, such as \textit{Sledgehammer} \cite{Sledgehammer}, is of course an essential prerequisite. + +In the formalisation presented below, we stick as closely as possible to the syntax of Boolos' original work; this is made easy in the user interface of Isabelle/HOL \cite{IsabelleJEDIT}. + +\input{session} + +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document} diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,721 +1,722 @@ ADS_Functor AI_Planning_Languages_Semantics AODV AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Ackermanns_not_PR Actuarial_Mathematics Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amicable_Numbers Amortized_Complexity AnselmGod Applicative_Lifting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS Attack_Trees Auto2_HOL Auto2_Imperative_HOL AutoFocus-Stream Automated_Stateful_Protocol_Verification Automatic_Refinement AxiomaticCategoryTheory Balog_Szemeredi_Gowers BDD BD_Security_Compositional BNF_CC BNF_Operations BTree Banach_Steinhaus Belief_Revision Bell_Numbers_Spivey BenOr_Kozen_Reif Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BirdKMP Birkhoff_Finite_Distributive_Lattices Blue_Eyes Bondy Boolean_Expression_Checkers Boolos_Curious_Inference +Boolos_Curious_Inference_Automated Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CISC-Kernel CRYSTALS-Kyber CRDT CSP_RefTK CYK CZH_Elementary_Categories CZH_Foundations CZH_Universal_Constructions CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Cauchy Cayley_Hamilton Certification_Monads Chandy_Lamport CHERI-C_Memory_Model Chord_Segments Circus Clean Clique_and_Monotone_Circuits ClockSynchInst Closest_Pair_Points CoCon CoSMeDis CoSMed CofGroups Coinductive Coinductive_Languages Collections Combinable_Wands Combinatorial_Enumeration_Algorithms Combinatorics_Words Combinatorics_Words_Graph_Lemma Combinatorics_Words_Lyndon Commuting_Hermitian Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Complete_Non_Orders Completeness Complex_Bounded_Operators Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Conditional_Simplification Conditional_Transfer_Rule Consensus_Refined Constructive_Cryptography Constructive_Cryptography_CM Constructor_Funs Containers CoreC++ Core_DOM Core_SC_DOM Correctness_Algebras Cotangent_PFD_Formula Count_Complex_Roots CryptHOL CryptoBasedCompositionalProperties Cubic_Quartic_Equations DFS_Framework DOM_Components DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Dedekind_Real Deep_Learning Delta_System_Lemma Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Design_Theory Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic Digit_Expansions Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation DiskPaxos Dominance_CHK DPRM_Theorem DynamicArchitectures Dynamic_Tables E_Transcendental Echelon_Form EdmondsKarp_Maxflow Efficient-Mergesort Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Equivalence_Relation_Enumeration Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Eval_FO Example-Submission Extended_Finite_State_Machine_Inference Extended_Finite_State_Machines FFT FLP FOL-Fitting FOL_Axiomatic FOL_Harrison FOL_Seq_Calc1 FOL_Seq_Calc2 FOL_Seq_Calc3 FSM_Tests Factor_Algebraic_Polynomial Factored_Transition_System_Bounding Falling_Factorial_Sum Farkas FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite-Map-Extras Finite_Automata_HF Finite_Fields Finitely_Generated_Abelian_Groups First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Fishers_Inequality Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing Formal_Puiseux_Series Formal_SSA Formula_Derivatives Foundation_of_geometry Fourier FO_Theory_Rewriting Free-Boolean-Algebra Free-Groups Frequency_Moments Fresh_Identifiers FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC GaleStewart_Games Gale_Shapley Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums Gaussian_Integers GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic GoedelGod Goedel_HFSet_Semantic Goedel_HFSet_Semanticless Goedel_Incompleteness Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Grothendieck_Schemes Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Hahn_Jordan_Decomposition Hales_Jewett Heard_Of Hello_World HereditarilyFinite Hermite Hermite_Lindemann Hidden_Markov_Models Higher_Order_Terms Hoare_Time Hood_Melville_Queue HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL Hyperdual IEEE_Floating_Point IFC_Tracking IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IMP_Compiler IMP_Compiler_Reuse IP_Addresses Imperative_Insertion_Sort Implicational_Logic Impossible_Geometry Incompleteness Incredible_Proof_Machine Independence_CH Inductive_Confidentiality Inductive_Inference InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interpolation_Polynomials_HOL_Algebra Interpreter_Optimizations Interval_Arithmetic_Word32 Intro_Dest_Elim Involutions2Squares Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl Irrationals_From_THEBOOK IsaGeoCoq Isabelle_C Isabelle_Marries_Dirac Isabelle_Meta_Model IsaNet Jacobson_Basic_Algebra Jinja JinjaDCI JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Khovanskii_Theorem Kleene_Algebra Kneser_Cauchy_Davenport Knights_Tour Knot_Theory Knuth_Bendix_Order Knuth_Morris_Pratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LTL LTL_Master_Theorem LTL_Normal_Form LTL_to_DRA LTL_to_GBA Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_EPO Lambda_Free_KBOs Lambda_Free_RPOs Lambert_W Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Launchbury Laws_of_Large_Numbers Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option Lifting_the_Exponent LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Logging_Independent_Anonymity Lowe_Ontological_Argument Lower_Semicontinuous Lp LP_Duality Lucas_Theorem MDP-Algorithms MDP-Rewards MFMC_Countable MFODL_Monitor_Optimized MFOTL_Monitor MSO_Regex_Equivalence Markov_Models Marriage Mason_Stothers Matrices_for_ODEs Matrix Matrix_Tensor Matroids Maximum_Segment_Sum Max-Card-Matching Median_Method Median_Of_Medians_Selection Menger Mereology Mersenne_Primes Metalogic_ProofChecker MiniML MiniSail Minimal_SSA Minkowskis_Theorem Minsky_Machines Modal_Logics_for_NTS Modular_Assembly_Kit_Security Modular_arithmetic_LLL_and_HNF_algorithms Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multiset_Ordering_NPC Multi_Party_Computation Multirelations Multitape_To_Singletape_TM Myhill-Nerode Name_Carrying_Type_Inference Nano_JSON Nash_Williams Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers Nominal2 Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Number_Theoretic_Transform Octonions OpSets Open_Induction Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinal_Partitions Ordinals_and_Cardinals Ordinary_Differential_Equations PAC_Checker Package_logic PAL PAPP_Impossibility PCF PLM POPLmark-deBruijn PSemigroupsConvolution Padic_Ints Padic_Field Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Pell Perfect-Number-Thm Perron_Frobenius Physical_Quantities Pi_Calculus Pi_Transcendental Planarity_Certificates Pluennecke_Ruzsa_Inequality Poincare_Bendixson Poincare_Disc Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Power_Sum_Polynomials Pratt_Certificate Prefix_Free_Code_Combinators Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Program-Conflict-Analysis Progress_Tracking Projective_Geometry Projective_Measurements Promela Proof_Strategy_Language PropResPI Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem Public_Announcement_Logic QHLProver QR_Decomposition Quantales Quantifier_Elimination_Hybrid Quasi_Borel_Spaces Quaternions Query_Optimization Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Random_Graph_Subgraph_Threshold Randomised_BSTs Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Real_Power Real_Time_Deque Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Registers Regression_Test_Selection Regular-Sets Regular_Algebras Regular_Tree_Relations Relation_Algebra Relational-Incorrectness-Logic Relational_Disjoint_Set_Forests Relational_Forests Relational_Method Relational_Minimum_Spanning_Trees Relational_Paths Rep_Fin_Groups ResiduatedTransitionSystem Residuated_Lattices Resolution_FOL Rewrite_Properties_Reduction Rewriting_Z Ribbon_Proofs Risk_Free_Lending Robbins-Conjecture Robinson_Arithmetic Root_Balanced_Tree Roth_Arithmetic_Progressions Routing Roy_Floyd_Warshall SATSolverVerification SC_DOM_Components SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 Safe_Distance Safe_OCL Safe_Range_RC Saturation_Framework Saturation_Framework_Extensions Sauer_Shelah_Lemma SCC_Bloemen_Sequential Schutz_Spacetime Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL Separation_Logic_Unbounded SequentInvertibility Shadow_DOM Shadow_SC_DOM Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Firewall Simplex Simplicial_complexes_and_boolean_functions SimplifiedOntologicalArgument Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds Sophomores_Dream Solidity Sort_Encodings Source_Coding_Theorem SpecCheck Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Stalnaker_Logic Statecharts Stateful_Protocol_Composition_and_Typing Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras SumSquares Sunflowers SuperCalc Surprise_Paradox Symmetric_Polynomials Syntax_Independent_Logic Synthetic_Completeness Szemeredi_Regularity Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Three_Circles Timed_Automata Topological_Semantics Topology TortoiseHare Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Transitive_Models Treaps Tree-Automata Tree_Decomposition Triangle Trie Turans_Graph_Theorem Twelvefold_Way Tycon Types_Tableaus_and_Goedels_God Types_To_Sets_Extension UPF UPF_Firewall UTP Undirected_Graph_Theory Universal_Hash_Families Universal_Turing_Machine UpDown_Scheme Valuation Van_Emde_Boas_Trees Van_der_Waerden VectorSpace VeriComp Verified-Prover Verified_SAT_Based_AI_Planning VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves Virtual_Substitution VolpanoSmith VYDRA_MDL WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weight_Balanced_Trees Weighted_Arithmetic_Geometric_Mean Weighted_Path_Order Well_Quasi_Orders Wetzels_Problem Winding_Number_Eval Word_Lib WorkerWrapper X86_Semantics XML Youngs_Inequality ZFC_in_HOL Zeta_3_Irrational Zeta_Function pGCL