ºÝºÝߣshows by User: lawrencepaulson / http://www.slideshare.net/images/logo.gif ºÝºÝߣshows by User: lawrencepaulson / Wed, 19 Nov 2014 09:56:15 GMT ºÝºÝߣShare feed for ºÝºÝߣshows by User: lawrencepaulson Proving Security Protocols Correct /slideshow/proving-security-protocols-correct/41759848 lics-slides-141119095615-conversion-gate01
Keynote lecture for the IEEE Symposium on Logic in Computer Science (LICS). Trento, Italy (1999).]]>
Keynote lecture for the IEEE Symposium on Logic in Computer Science (LICS). Trento, Italy (1999).]]> Wed, 19 Nov 2014 09:56:15 GMT /slideshow/proving-security-protocols-correct/41759848 lawrencepaulson@slideshare.net(lawrencepaulson) Proving Security Protocols Correct lawrencepaulson Keynote lecture for the IEEE Symposium on Logic in Computer Science (LICS). Trento, Italy (1999). <img style="border:1px solid #C3E6D8;float:right;" alt="" src="https://cdn.slidesharecdn.com/ss_thumbnails/lics-slides-141119095615-conversion-gate01-thumbnail.jpg?width=120&amp;height=120&amp;fit=bounds" /><br> Keynote lecture for the IEEE Symposium on Logic in Computer Science (LICS). Trento, Italy (1999).
Proving Security Protocols Correct from Lawrence Paulson
]]> 454 2 https://cdn.slidesharecdn.com/ss_thumbnails/lics-slides-141119095615-conversion-gate01-thumbnail.jpg?width=120&height=120&fit=bounds presentation Black http://activitystrea.ms/schema/1.0/post http://activitystrea.ms/schema/1.0/posted 0 MetiTarski's menagerie of cooperating systems /slideshow/fro-cos-presentation/41152254 frocos-presentation-141105062813-conversion-gate01
Plenary Lecture for the FroCoS and Tableaux conferences. Nancy, France, September 2013.]]>
Plenary Lecture for the FroCoS and Tableaux conferences. Nancy, France, September 2013.]]> Wed, 05 Nov 2014 06:28:12 GMT /slideshow/fro-cos-presentation/41152254 lawrencepaulson@slideshare.net(lawrencepaulson) MetiTarski's menagerie of cooperating systems lawrencepaulson Plenary Lecture for the FroCoS and Tableaux conferences. Nancy, France, September 2013. <img style="border:1px solid #C3E6D8;float:right;" alt="" src="https://cdn.slidesharecdn.com/ss_thumbnails/frocos-presentation-141105062813-conversion-gate01-thumbnail.jpg?width=120&amp;height=120&amp;fit=bounds" /><br> Plenary Lecture for the FroCoS and Tableaux conferences. Nancy, France, September 2013.
MetiTarski's menagerie of cooperating systems from Lawrence Paulson
]]> 378 6 https://cdn.slidesharecdn.com/ss_thumbnails/frocos-presentation-141105062813-conversion-gate01-thumbnail.jpg?width=120&height=120&fit=bounds presentation Black http://activitystrea.ms/schema/1.0/post http://activitystrea.ms/schema/1.0/posted 0 Automated theorem proving for special functions: the next phase /slideshow/snc2014-slides/41152172 snc2014-slides-141105062617-conversion-gate01
Keynote Lecture for the conference SNC 2014 (Symbolic-Numeric Computation). Shanghai, China, July 2014.]]>
Keynote Lecture for the conference SNC 2014 (Symbolic-Numeric Computation). Shanghai, China, July 2014.]]> Wed, 05 Nov 2014 06:26:16 GMT /slideshow/snc2014-slides/41152172 lawrencepaulson@slideshare.net(lawrencepaulson) Automated theorem proving for special functions: the next phase lawrencepaulson Keynote Lecture for the conference SNC 2014 (Symbolic-Numeric Computation). Shanghai, China, July 2014. <img style="border:1px solid #C3E6D8;float:right;" alt="" src="https://cdn.slidesharecdn.com/ss_thumbnails/snc2014-slides-141105062617-conversion-gate01-thumbnail.jpg?width=120&amp;height=120&amp;fit=bounds" /><br> Keynote Lecture for the conference SNC 2014 (Symbolic-Numeric Computation). Shanghai, China, July 2014.
Automated theorem proving for special functions: the next phase from Lawrence Paulson
]]> 578 3 https://cdn.slidesharecdn.com/ss_thumbnails/snc2014-slides-141105062617-conversion-gate01-thumbnail.jpg?width=120&height=120&fit=bounds presentation Black http://activitystrea.ms/schema/1.0/post http://activitystrea.ms/schema/1.0/posted 0 Theorem proving and the real numbers: overview and challenges /slideshow/nfm-2014/41152088 nfm2014-141105062419-conversion-gate02
Keynote Lecture for the conference NASA Formal Methods. Houston, Texas, April 2014.]]>
Keynote Lecture for the conference NASA Formal Methods. Houston, Texas, April 2014.]]> Wed, 05 Nov 2014 06:24:18 GMT /slideshow/nfm-2014/41152088 lawrencepaulson@slideshare.net(lawrencepaulson) Theorem proving and the real numbers: overview and challenges lawrencepaulson Keynote Lecture for the conference NASA Formal Methods. Houston, Texas, April 2014. <img style="border:1px solid #C3E6D8;float:right;" alt="" src="https://cdn.slidesharecdn.com/ss_thumbnails/nfm2014-141105062419-conversion-gate02-thumbnail.jpg?width=120&amp;height=120&amp;fit=bounds" /><br> Keynote Lecture for the conference NASA Formal Methods. Houston, Texas, April 2014.
Theorem proving and the real numbers: overview and challenges from Lawrence Paulson
]]> 594 2 https://cdn.slidesharecdn.com/ss_thumbnails/nfm2014-141105062419-conversion-gate02-thumbnail.jpg?width=120&height=120&fit=bounds presentation Black http://activitystrea.ms/schema/1.0/post http://activitystrea.ms/schema/1.0/posted 0 Source-Level Proof Reconstruction for Interactive Proving /slideshow/reconstruction-slides/33033278 reconstruction-slides-140402075546-phpapp01
Interactive proof assistants should verify the proofs they re- ceive from automatic theorem provers. Normally this proof reconstruc- tion takes place internally, forming part of the integration between the two tools. We have implemented source-level proof reconstruction: reso- lution proofs are automatically translated to Isabelle proof scripts. Users can insert this text into their proof development or (if they wish) exam- ine it manually. Each step of a proof is justified by calling Hurd’s Metis prover, which we have ported to Isabelle. A recurrent issue in this project is the treatment of Isabelle’s axiomatic type classes. Theorem Proving in Higher Order Logics (Springer LNCS 4732, 2007), 232–245. ]]>
Interactive proof assistants should verify the proofs they re- ceive from automatic theorem provers. Normally this proof reconstruc- tion takes place internally, forming part of the integration between the two tools. We have implemented source-level proof reconstruction: reso- lution proofs are automatically translated to Isabelle proof scripts. Users can insert this text into their proof development or (if they wish) exam- ine it manually. Each step of a proof is justified by calling Hurd’s Metis prover, which we have ported to Isabelle. A recurrent issue in this project is the treatment of Isabelle’s axiomatic type classes. Theorem Proving in Higher Order Logics (Springer LNCS 4732, 2007), 232–245. ]]> Wed, 02 Apr 2014 07:55:46 GMT /slideshow/reconstruction-slides/33033278 lawrencepaulson@slideshare.net(lawrencepaulson) Source-Level Proof Reconstruction for Interactive Proving lawrencepaulson Interactive proof assistants should verify the proofs they re- ceive from automatic theorem provers. Normally this proof reconstruc- tion takes place internally, forming part of the integration between the two tools. We have implemented source-level proof reconstruction: reso- lution proofs are automatically translated to Isabelle proof scripts. Users can insert this text into their proof development or (if they wish) exam- ine it manually. Each step of a proof is justified by calling Hurd’s Metis prover, which we have ported to Isabelle. A recurrent issue in this project is the treatment of Isabelle’s axiomatic type classes. Theorem Proving in Higher Order Logics (Springer LNCS 4732, 2007), 232–245. <img style="border:1px solid #C3E6D8;float:right;" alt="" src="https://cdn.slidesharecdn.com/ss_thumbnails/reconstruction-slides-140402075546-phpapp01-thumbnail.jpg?width=120&amp;height=120&amp;fit=bounds" /><br> Interactive proof assistants should verify the proofs they re- ceive from automatic theorem provers. Normally this proof reconstruc- tion takes place internally, forming part of the integration between the two tools. We have implemented source-level proof reconstruction: reso- lution proofs are automatically translated to Isabelle proof scripts. Users can insert this text into their proof development or (if they wish) exam- ine it manually. Each step of a proof is justified by calling Hurd’s Metis prover, which we have ported to Isabelle. A recurrent issue in this project is the treatment of Isabelle’s axiomatic type classes. Theorem Proving in Higher Order Logics (Springer LNCS 4732, 2007), 232–245.
Source-Level Proof Reconstruction for Interactive Proving from Lawrence Paulson
]]> 287 2 https://cdn.slidesharecdn.com/ss_thumbnails/reconstruction-slides-140402075546-phpapp01-thumbnail.jpg?width=120&height=120&fit=bounds presentation Black http://activitystrea.ms/schema/1.0/post http://activitystrea.ms/schema/1.0/posted 0 Defining Functions on Equivalence Classes /slideshow/equivclasses-slides/33033138 equivclasses-slides-140402075208-phpapp02
A quotient construction defines an abstract type from a concrete type, using an equivalence relation to identify elements of the concrete type that are to be regarded as indistinguishable. The elements of a quotient type are equivalence classes: sets of equivalent concrete values. Simple techniques are presented for defining and reasoning about quotient constructions, based on a general lemma library concerning functions that operate on equivalence classes. The techniques are applied to a definition of the integers from the natural numbers, and then to the definition of a recursive datatype satisfying equational constraints. Published in ACM Trans. on Computational Logic 7 4 (2006), 658–675.]]>
A quotient construction defines an abstract type from a concrete type, using an equivalence relation to identify elements of the concrete type that are to be regarded as indistinguishable. The elements of a quotient type are equivalence classes: sets of equivalent concrete values. Simple techniques are presented for defining and reasoning about quotient constructions, based on a general lemma library concerning functions that operate on equivalence classes. The techniques are applied to a definition of the integers from the natural numbers, and then to the definition of a recursive datatype satisfying equational constraints. Published in ACM Trans. on Computational Logic 7 4 (2006), 658–675.]]> Wed, 02 Apr 2014 07:52:08 GMT /slideshow/equivclasses-slides/33033138 lawrencepaulson@slideshare.net(lawrencepaulson) Defining Functions on Equivalence Classes lawrencepaulson A quotient construction defines an abstract type from a concrete type, using an equivalence relation to identify elements of the concrete type that are to be regarded as indistinguishable. The elements of a quotient type are equivalence classes: sets of equivalent concrete values. Simple techniques are presented for defining and reasoning about quotient constructions, based on a general lemma library concerning functions that operate on equivalence classes. The techniques are applied to a definition of the integers from the natural numbers, and then to the definition of a recursive datatype satisfying equational constraints. Published in ACM Trans. on Computational Logic 7 4 (2006), 658–675. <img style="border:1px solid #C3E6D8;float:right;" alt="" src="https://cdn.slidesharecdn.com/ss_thumbnails/equivclasses-slides-140402075208-phpapp02-thumbnail.jpg?width=120&amp;height=120&amp;fit=bounds" /><br> A quotient construction defines an abstract type from a concrete type, using an equivalence relation to identify elements of the concrete type that are to be regarded as indistinguishable. The elements of a quotient type are equivalence classes: sets of equivalent concrete values. Simple techniques are presented for defining and reasoning about quotient constructions, based on a general lemma library concerning functions that operate on equivalence classes. The techniques are applied to a definition of the integers from the natural numbers, and then to the definition of a recursive datatype satisfying equational constraints. Published in ACM Trans. on Computational Logic 7 4 (2006), 658–675.
Defining Functions on Equivalence Classes from Lawrence Paulson
]]> 1305 7 https://cdn.slidesharecdn.com/ss_thumbnails/equivclasses-slides-140402075208-phpapp02-thumbnail.jpg?width=120&height=120&fit=bounds presentation Black http://activitystrea.ms/schema/1.0/post http://activitystrea.ms/schema/1.0/posted 0 Organizing Numerical Theories using Axiomatic Type Classes /slideshow/type-classes-slides/32765875 typeclasses-slides-140326102901-phpapp01
Published in the J. Automated Reasoning 33 1 (2004), 29–49. Describes the use of axiomatic type classes in Isabelle eliminate duplication in the presence of many different numeric types, from the natural numbers to the complexes and beyond.]]>
Published in the J. Automated Reasoning 33 1 (2004), 29–49. Describes the use of axiomatic type classes in Isabelle eliminate duplication in the presence of many different numeric types, from the natural numbers to the complexes and beyond.]]> Wed, 26 Mar 2014 10:29:01 GMT /slideshow/type-classes-slides/32765875 lawrencepaulson@slideshare.net(lawrencepaulson) Organizing Numerical Theories using Axiomatic Type Classes lawrencepaulson Published in the J. Automated Reasoning 33 1 (2004), 29–49. Describes the use of axiomatic type classes in Isabelle eliminate duplication in the presence of many different numeric types, from the natural numbers to the complexes and beyond. <img style="border:1px solid #C3E6D8;float:right;" alt="" src="https://cdn.slidesharecdn.com/ss_thumbnails/typeclasses-slides-140326102901-phpapp01-thumbnail.jpg?width=120&amp;height=120&amp;fit=bounds" /><br> Published in the J. Automated Reasoning 33 1 (2004), 29–49. Describes the use of axiomatic type classes in Isabelle eliminate duplication in the presence of many different numeric types, from the natural numbers to the complexes and beyond.
Organizing Numerical Theories using Axiomatic Type Classes from Lawrence Paulson
]]> 335 2 https://cdn.slidesharecdn.com/ss_thumbnails/typeclasses-slides-140326102901-phpapp01-thumbnail.jpg?width=120&height=120&fit=bounds presentation Black http://activitystrea.ms/schema/1.0/post http://activitystrea.ms/schema/1.0/posted 0 A Generic Tableau Prover and Its Integration with Isabelle /slideshow/blast-slides/32765585 blast-slides-140326102405-phpapp02
Published in the CADE-15 Workshop on Integration of Deductive Systems (1998). Describes the automatic theorem proving technology used in the Isabelle system.]]>
Published in the CADE-15 Workshop on Integration of Deductive Systems (1998). Describes the automatic theorem proving technology used in the Isabelle system.]]> Wed, 26 Mar 2014 10:24:05 GMT /slideshow/blast-slides/32765585 lawrencepaulson@slideshare.net(lawrencepaulson) A Generic Tableau Prover and Its Integration with Isabelle lawrencepaulson Published in the CADE-15 Workshop on Integration of Deductive Systems (1998). Describes the automatic theorem proving technology used in the Isabelle system. <img style="border:1px solid #C3E6D8;float:right;" alt="" src="https://cdn.slidesharecdn.com/ss_thumbnails/blast-slides-140326102405-phpapp02-thumbnail.jpg?width=120&amp;height=120&amp;fit=bounds" /><br> Published in the CADE-15 Workshop on Integration of Deductive Systems (1998). Describes the automatic theorem proving technology used in the Isabelle system.
A Generic Tableau Prover and Its Integration with Isabelle from Lawrence Paulson
]]> 381 3 https://cdn.slidesharecdn.com/ss_thumbnails/blast-slides-140326102405-phpapp02-thumbnail.jpg?width=120&height=120&fit=bounds presentation Black http://activitystrea.ms/schema/1.0/post http://activitystrea.ms/schema/1.0/posted 0 Mechanized Proofs for a Recursive Authentication Protocol /slideshow/recur-slides/32765323 recur-slides-140326101900-phpapp02
Presented at the 10th Computer Security Foundations Workshop, 1997. One of the first papers concerning the inductive approach to verifying cryptographic protocols, demonstrated on a variable-length multi-party protocol.]]>
Presented at the 10th Computer Security Foundations Workshop, 1997. One of the first papers concerning the inductive approach to verifying cryptographic protocols, demonstrated on a variable-length multi-party protocol.]]> Wed, 26 Mar 2014 10:19:00 GMT /slideshow/recur-slides/32765323 lawrencepaulson@slideshare.net(lawrencepaulson) Mechanized Proofs for a Recursive Authentication Protocol lawrencepaulson Presented at the 10th Computer Security Foundations Workshop, 1997. One of the first papers concerning the inductive approach to verifying cryptographic protocols, demonstrated on a variable-length multi-party protocol. <img style="border:1px solid #C3E6D8;float:right;" alt="" src="https://cdn.slidesharecdn.com/ss_thumbnails/recur-slides-140326101900-phpapp02-thumbnail.jpg?width=120&amp;height=120&amp;fit=bounds" /><br> Presented at the 10th Computer Security Foundations Workshop, 1997. One of the first papers concerning the inductive approach to verifying cryptographic protocols, demonstrated on a variable-length multi-party protocol.
Mechanized Proofs for a Recursive Authentication Protocol from Lawrence Paulson
]]> 274 2 https://cdn.slidesharecdn.com/ss_thumbnails/recur-slides-140326101900-phpapp02-thumbnail.jpg?width=120&height=120&fit=bounds presentation White http://activitystrea.ms/schema/1.0/post http://activitystrea.ms/schema/1.0/posted 0 Mechanizing set theory: cardinal arithmetic and the axiom of choice /slideshow/ac-slides/32493228 ac-slides-140319095754-phpapp01
This 1996 paper on formalising axiomatic set theory using Isabelle/ZF was published in the Journal of Automated Reasoning 17 (1996), 291–32]]>
This 1996 paper on formalising axiomatic set theory using Isabelle/ZF was published in the Journal of Automated Reasoning 17 (1996), 291–32]]> Wed, 19 Mar 2014 09:57:54 GMT /slideshow/ac-slides/32493228 lawrencepaulson@slideshare.net(lawrencepaulson) Mechanizing set theory: cardinal arithmetic and the axiom of choice lawrencepaulson This 1996 paper on formalising axiomatic set theory using Isabelle/ZF was published in the Journal of Automated Reasoning 17 (1996), 291–32 <img style="border:1px solid #C3E6D8;float:right;" alt="" src="https://cdn.slidesharecdn.com/ss_thumbnails/ac-slides-140319095754-phpapp01-thumbnail.jpg?width=120&amp;height=120&amp;fit=bounds" /><br> This 1996 paper on formalising axiomatic set theory using Isabelle/ZF was published in the Journal of Automated Reasoning 17 (1996), 291–32
Mechanizing set theory: cardinal arithmetic and the axiom of choice from Lawrence Paulson
]]> 584 2 https://cdn.slidesharecdn.com/ss_thumbnails/ac-slides-140319095754-phpapp01-thumbnail.jpg?width=120&height=120&fit=bounds presentation Black http://activitystrea.ms/schema/1.0/post http://activitystrea.ms/schema/1.0/posted 0 MetiTarski: An Automatic Prover for Real-Valued Special Functions /slideshow/metit-slides/29505616 metit-slides-131226092124-phpapp01
]]>
]]> Thu, 26 Dec 2013 09:21:24 GMT /slideshow/metit-slides/29505616 lawrencepaulson@slideshare.net(lawrencepaulson) MetiTarski: An Automatic Prover for Real-Valued Special Functions lawrencepaulson <img style="border:1px solid #C3E6D8;float:right;" alt="" src="https://cdn.slidesharecdn.com/ss_thumbnails/metit-slides-131226092124-phpapp01-thumbnail.jpg?width=120&amp;height=120&amp;fit=bounds" /><br>
MetiTarski: An Automatic Prover for Real-Valued Special Functions from Lawrence Paulson
]]> 354 4 https://cdn.slidesharecdn.com/ss_thumbnails/metit-slides-131226092124-phpapp01-thumbnail.jpg?width=120&height=120&fit=bounds presentation White http://activitystrea.ms/schema/1.0/post http://activitystrea.ms/schema/1.0/posted 0 The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF /slideshow/constructible-slides/29505574 constructible-slides-131226091830-phpapp01
]]>
]]> Thu, 26 Dec 2013 09:18:30 GMT /slideshow/constructible-slides/29505574 lawrencepaulson@slideshare.net(lawrencepaulson) The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF lawrencepaulson <img style="border:1px solid #C3E6D8;float:right;" alt="" src="https://cdn.slidesharecdn.com/ss_thumbnails/constructible-slides-131226091830-phpapp01-thumbnail.jpg?width=120&amp;height=120&amp;fit=bounds" /><br>
The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF from Lawrence Paulson
]]> 561 2 https://cdn.slidesharecdn.com/ss_thumbnails/constructible-slides-131226091830-phpapp01-thumbnail.jpg?width=120&height=120&fit=bounds presentation White http://activitystrea.ms/schema/1.0/post http://activitystrea.ms/schema/1.0/posted 0 The Reflection Theorem: Formalizing Meta-Theoretic Reasoning /slideshow/the-reflection-theorem-formalizing-metatheoretic-reasoning/29503750 reflection-slides-131226070330-phpapp02
]]>
]]> Thu, 26 Dec 2013 07:03:30 GMT /slideshow/the-reflection-theorem-formalizing-metatheoretic-reasoning/29503750 lawrencepaulson@slideshare.net(lawrencepaulson) The Reflection Theorem: Formalizing Meta-Theoretic Reasoning lawrencepaulson <img style="border:1px solid #C3E6D8;float:right;" alt="" src="https://cdn.slidesharecdn.com/ss_thumbnails/reflection-slides-131226070330-phpapp02-thumbnail.jpg?width=120&amp;height=120&amp;fit=bounds" /><br>
The Reflection Theorem: Formalizing Meta-Theoretic Reasoning from Lawrence Paulson
]]> 486 3 https://cdn.slidesharecdn.com/ss_thumbnails/reflection-slides-131226070330-phpapp02-thumbnail.jpg?width=120&height=120&fit=bounds presentation Black http://activitystrea.ms/schema/1.0/post http://activitystrea.ms/schema/1.0/posted 0 Proving Properties of Security Protocols by Induction /slideshow/proving-properties-of-security-protocols-by-induction/29503716 auth-slides-131226070146-phpapp02
]]>
]]> Thu, 26 Dec 2013 07:01:46 GMT /slideshow/proving-properties-of-security-protocols-by-induction/29503716 lawrencepaulson@slideshare.net(lawrencepaulson) Proving Properties of Security Protocols by Induction lawrencepaulson <img style="border:1px solid #C3E6D8;float:right;" alt="" src="https://cdn.slidesharecdn.com/ss_thumbnails/auth-slides-131226070146-phpapp02-thumbnail.jpg?width=120&amp;height=120&amp;fit=bounds" /><br>
Proving Properties of Security Protocols by Induction from Lawrence Paulson
]]> 562 2 https://cdn.slidesharecdn.com/ss_thumbnails/auth-slides-131226070146-phpapp02-thumbnail.jpg?width=120&height=120&fit=bounds presentation Black http://activitystrea.ms/schema/1.0/post http://activitystrea.ms/schema/1.0/posted 0 A Machine-Assisted Proof of Gödel's Incompleteness Theorems /slideshow/godel-slides/29503633 godel-slides-131226065705-phpapp01
]]>
]]> Thu, 26 Dec 2013 06:57:05 GMT /slideshow/godel-slides/29503633 lawrencepaulson@slideshare.net(lawrencepaulson) A Machine-Assisted Proof of Gödel's Incompleteness Theorems lawrencepaulson <img style="border:1px solid #C3E6D8;float:right;" alt="" src="https://cdn.slidesharecdn.com/ss_thumbnails/godel-slides-131226065705-phpapp01-thumbnail.jpg?width=120&amp;height=120&amp;fit=bounds" /><br>
A Machine-Assisted Proof of Gæ—¦del's Incompleteness Theorems from Lawrence Paulson
]]> 2134 7 https://cdn.slidesharecdn.com/ss_thumbnails/godel-slides-131226065705-phpapp01-thumbnail.jpg?width=120&height=120&fit=bounds presentation White http://activitystrea.ms/schema/1.0/post http://activitystrea.ms/schema/1.0/posted 0 https://cdn.slidesharecdn.com/profile-photo-lawrencepaulson-48x48.jpg?cb=1523521740 https://cdn.slidesharecdn.com/ss_thumbnails/lics-slides-141119095615-conversion-gate01-thumbnail.jpg?width=320&height=320&fit=bounds slideshow/proving-security-protocols-correct/41759848 Proving Security Proto... https://cdn.slidesharecdn.com/ss_thumbnails/frocos-presentation-141105062813-conversion-gate01-thumbnail.jpg?width=320&height=320&fit=bounds slideshow/fro-cos-presentation/41152254 MetiTarski&#39;s menagerie... https://cdn.slidesharecdn.com/ss_thumbnails/snc2014-slides-141105062617-conversion-gate01-thumbnail.jpg?width=320&height=320&fit=bounds slideshow/snc2014-slides/41152172 Automated theorem prov...