hol-info  

Messages by Thread

• • Re: [Hol-info] assumption matching in SPLIT_LT Konrad Slind
  • Re: [Hol-info] assumption matching in SPLIT_LT Waqar Ahmad via hol-info
  • Re: [Hol-info] assumption matching in SPLIT_LT Michael.Norrish
  • Re: [Hol-info] assumption matching in SPLIT_LT Waqar Ahmad via hol-info
  • Re: [Hol-info] assumption matching in SPLIT_LT Jeremy Dawson
• [Hol-info] Exception raised while using HOL in hol-mode Yassmeen Derhalli
  • [Hol-info] Exception raised while using HOL in hol-mode Yassmeen Derhalli
  • Re: [Hol-info] Exception raised while using HOL in hol-mode Thomas Tuerk
  • Re: [Hol-info] Exception raised while using HOL in hol-mode Yassmeen Derhalli
  • Re: [Hol-info] Exception raised while using HOL in hol-mode Michael.Norrish
• [Hol-info] LPAR-22 in Ethiopia - Call for Short Papers geoff
• [Hol-info] 13th International Workshop on the Implementation of Logics geoff
• [Hol-info] Final Call for Papers PADL-19 Moa Johansson
• [Hol-info] PhD positions in Programming Language Technology for Security and Privacy David Sands
• [Hol-info] LPNMR 2019 Call for Papers ** INVITED SPEAKERS TO BE ANNOUNCED ggelfond
• [Hol-info] NFM 2019 First Call For Papers- 11th Annual NASA Formal Methods Symposium Kristin Yvonne Rozier
• [Hol-info] Choosing an element in an increasing sequence of sets Chun Tian (binghe)
  • Re: [Hol-info] Choosing an element in an increasing sequence of sets Chun Tian (binghe)
  • Re: [Hol-info] Choosing an element in an increasing sequence of sets Ramana Kumar
  • Re: [Hol-info] Choosing an element in an increasing sequence of sets Chun Tian (binghe)
  • Re: [Hol-info] Choosing an element in an increasing sequence of sets Chun Tian (binghe)
  • Re: [Hol-info] Choosing an element in an increasing sequence of sets Thomas Tuerk
  • Re: [Hol-info] Choosing an element in an increasing sequence of sets Chun Tian (binghe)
  • Re: [Hol-info] Choosing an element in an increasing sequence of sets Chun Tian (binghe)
• [Hol-info] CPP 2019: Final Call for Papers Magnus Myreen
• [Hol-info] Prove BIGUNION (IMAGE f 𝕌(:num)) by induction on (count n)? Chun Tian (binghe)
  • Re: [Hol-info] Prove BIGUNION (IMAGE f 𝕌(:num)) by induction on (count n)? Waqar Ahmad via hol-info
  • Re: [Hol-info] Prove BIGUNION (IMAGE f 𝕌(:num)) by induction on (count n)? Chun Tian (binghe)
  • Re: [Hol-info] Prove BIGUNION (IMAGE f 𝕌(:num)) by induction on (count n)? Chun Tian (binghe)
  • Re: [Hol-info] Prove BIGUNION (IMAGE f 𝕌(:num)) by induction on (count n)? Chun Tian (binghe)
• [Hol-info] Uninterruptible PROVE_TAC [] Chun Tian (binghe)
• [Hol-info] The "limit" of a ``:'num->'a set`` function? Chun Tian (binghe)
  • Re: [Hol-info] The "limit" of a ``:'num->'a set`` function? Umair Siddique
  • Re: [Hol-info] The "limit" of a ``:'num->'a set`` function? Michael.Norrish
  • Re: [Hol-info] The "limit" of a ``:'num->'a set`` function? Chun Tian (binghe)
• [Hol-info] CfP: Postproceedings ThEdu'18 Walther Neuper
• [Hol-info] Two definitions of wellfoundedness Chun Tian (binghe)
  • Re: [Hol-info] Two definitions of wellfoundedness Lorenz Leutgeb via hol-info
  • Re: [Hol-info] Two definitions of wellfoundedness Chun Tian (binghe)
• [Hol-info] JELIA 2019 - Preliminary Call for Papers Simona Perri
• [Hol-info] Software Verification and Testing Track (SVT) @ ACM SAC 2019 (deadline extension) Matthias Güdemann
• [Hol-info] Partial Order for Set Supremum Waqar Ahmad via hol-info
  • Re: [Hol-info] Partial Order for Set Supremum Michael.Norrish
• [Hol-info] RAMiCS 2018 Call for Participation: Relational and Algebraic Methods in Computer Science Walter Guttmann
• [Hol-info] Reference cells in HOL4 Fabian Immler
  • Re: [Hol-info] Reference cells in HOL4 Michael.Norrish
  • Re: [Hol-info] Reference cells in HOL4 Fabian Immler
• [Hol-info] [ACL2-2018] Call for Participation --- Registration Open! Shilpi Goel
• [Hol-info] Lazy list: Stream in coinduction Waqar Ahmad via hol-info
  • Re: [Hol-info] Lazy list: Stream in coinduction Michael.Norrish
  • Re: [Hol-info] Lazy list: Stream in coinduction Waqar Ahmad via hol-info
• [Hol-info] Failure with REWRITE_TAC and UNDISCH on conjunctions Dylan Melville
  • Re: [Hol-info] Failure with REWRITE_TAC and UNDISCH on conjunctions Michael.Norrish
  • Re: [Hol-info] Failure with REWRITE_TAC and UNDISCH on conjunctions Dylan Melville
  • Re: [Hol-info] Failure with REWRITE_TAC and UNDISCH on conjunctions Michael.Norrish
  • Re: [Hol-info] Failure with REWRITE_TAC and UNDISCH on conjunctions Dylan Melville
• [Hol-info] QuoteFilter with precise positions Makarius
  • Re: [Hol-info] QuoteFilter with precise positions Michael.Norrish
  • Re: [Hol-info] QuoteFilter with precise positions Michael.Norrish
  • Re: [Hol-info] QuoteFilter with precise positions Makarius
  • Re: [Hol-info] QuoteFilter with precise positions Michael.Norrish
• [Hol-info] NFM 2019 Preliminary Call For Papers- 11th Annual NASA Formal Methods Symposium Kristin Yvonne Rozier
• [Hol-info] Call for Papers: Symposium on Practical Aspects of Declarative Languages (PADL 2019) Moa Johansson
• [Hol-info] Assumptions of goal usage Dylan Melville
  • Re: [Hol-info] Assumptions of goal usage Dylan Melville
  • Re: [Hol-info] Assumptions of goal usage Michael.Norrish
• [Hol-info] Using Assumptions Dylan Melville
  • Re: [Hol-info] Using Assumptions Chun Tian (binghe)
  • Re: [Hol-info] Using Assumptions Jeremy Dawson
  • Re: [Hol-info] Using Assumptions Mario Xerxes Castelán Castro
  • Re: [Hol-info] Using Assumptions Michael.Norrish
• [Hol-info] anecdote that the spec for sorting is output is sorted AND a permutation? Black, Paul E. (Fed)
• [Hol-info] PPDP | LOPSTR | WFLP 2018 Common Call for Participation David Sabel
• [Hol-info] PhD opportunities at the ANU Michael.Norrish
• [Hol-info] Applying a theorem to a specific subgoal Dylan Melville
  • Re: [Hol-info] Applying a theorem to a specific subgoal Jeremy Dawson
  • Re: [Hol-info] Applying a theorem to a specific subgoal Heiko Becker
  • Re: [Hol-info] Applying a theorem to a specific subgoal Dylan Melville
• [Hol-info] Partial Function on lazy list Waqar Ahmad via hol-info
  • Re: [Hol-info] Partial Function on lazy list Michael.Norrish
  • Re: [Hol-info] Partial Function on lazy list Waqar Ahmad via hol-info
  • Re: [Hol-info] Partial Function on lazy list Michael.Norrish
  • Re: [Hol-info] Partial Function on lazy list Waqar Ahmad via hol-info
• [Hol-info] [Publicity] Call for Participation: 11th Conference on Intelligent Computer Mathematics Tanja Gutenbrunner
• [Hol-info] iFM 2018: Registration Bursaries for PhD students and Early Stage Researchers HaoWu
• [Hol-info] conflicts auto-resolved by Define? binghe
  • Re: [Hol-info] conflicts auto-resolved by Define? Waqar Ahmad via hol-info
  • Re: [Hol-info] conflicts auto-resolved by Define? Thomas Tuerk
  • Re: [Hol-info] conflicts auto-resolved by Define? Chun Tian (binghe)
  • Re: [Hol-info] conflicts auto-resolved by Define? Chun Tian (binghe)
  • Re: [Hol-info] conflicts auto-resolved by Define? Chun Tian (binghe)
  • Re: [Hol-info] conflicts auto-resolved by Define? Waqar Ahmad via hol-info
  • Re: [Hol-info] conflicts auto-resolved by Define? Chun Tian (binghe)
  • Re: [Hol-info] conflicts auto-resolved by Define? Waqar Ahmad via hol-info
  • [Hol-info] New extrealTheory (was: Re: conflicts auto-resolved by Define?) Chun Tian (binghe)
  • Re: [Hol-info] New extrealTheory (was: Re: conflicts auto-resolved by Define?) Waqar Ahmad via hol-info
  • Re: [Hol-info] New extrealTheory (was: Re: conflicts auto-resolved by Define?) Chun Tian (binghe)
  • [Hol-info] measureTheory (was: Re: New extrealTheory) Chun Tian (binghe)
  • Re: [Hol-info] measureTheory (was: Re: New extrealTheory) Waqar Ahmad via hol-info
  • [Hol-info] HOL's new measure theory (in progress) Chun Tian (binghe)
  • Re: [Hol-info] HOL's new measure theory (in progress) Waqar Ahmad via hol-info
  • Re: [Hol-info] HOL's new measure theory (in progress) Chun Tian (binghe)
  • Re: [Hol-info] HOL's new measure theory (in progress) Michael.Norrish
  • Re: [Hol-info] HOL's new measure theory (in progress) Chun Tian (binghe)
  • Re: [Hol-info] HOL's new measure theory (in progress) Chun Tian (binghe)
  • Re: [Hol-info] HOL's new measure theory (in progress) Michael.Norrish
  • Re: [Hol-info] HOL's new measure theory (in progress) Waqar Ahmad via hol-info
  • Re: [Hol-info] HOL's new measure theory (in progress) Chun Tian (binghe)
• [Hol-info] How to (automatically) change the names of quantified variables in a theorem? Chun Tian (binghe)
  • Re: [Hol-info] How to (automatically) change the names of quantified variables in a theorem? Thomas Tuerk
  • Re: [Hol-info] How to (automatically) change the names of quantified variables in a theorem? Chun Tian (binghe)
  • Re: [Hol-info] How to (automatically) change the names of quantified variables in a theorem? Konrad Slind
• [Hol-info] Term Concatenation Dylan Melville
  • Re: [Hol-info] Term Concatenation Mario Xerxes Castelán Castro
• [Hol-info] Call for Papers Software Verification and Testing Track @ ACM SAC 2019 Matthias Güdemann
• [Hol-info] ACTIONS@KR: LAST CALL FOR CONTRIBUTIONS Fabio Patrizi
• [Hol-info] Undefined references building “description.pdf” Mario Xerxes Castelán Castro
  • Re: [Hol-info] Undefined references building “description.pdf” Michael.Norrish
  • Re: [Hol-info] Undefined references building “description.pdf” Mario Xerxes Castelán Castro
• [Hol-info] PhD Position on the formalization of automated reasoning in Isabelle/HOL Jasmin Blanchette
• [Hol-info] CPP 2019: Call for Papers Magnus Myreen
• [Hol-info] INST on a theorem Dylan Melville
  • Re: [Hol-info] INST on a theorem Thomas Tuerk
  • Re: [Hol-info] INST on a theorem Dylan Melville
  • Re: [Hol-info] INST on a theorem Chun Tian (binghe)
  • Re: [Hol-info] INST on a theorem Konrad Slind
• [Hol-info] PhD Position on ICT in Trento on "Quantum Annealing for SAT Solving" roberto . sebastiani
• [Hol-info] LPNMR 2019 Call for Papers ** INVITED SPEAKERS TO BE ANNOUNCED ** ggelfond
  • [Hol-info] LPNMR 2019 Call for Papers ** INVITED SPEAKERS TO BE ANNOUNCED ** Gregory Gelfond
• [Hol-info] MESON Dylan Melville
  • Re: [Hol-info] MESON Waqar Ahmad via hol-info
  • Re: [Hol-info] MESON Petros Papapanagiotou
• [Hol-info] Deadline Extension: Workshop in OCL and Textual Modeling (OCL 2018) Achim D. Brucker
• [Hol-info] ACTIONS@KR18: DEADLINE EXTENSION Fabio Patrizi
• [Hol-info] KR 2018 ** WORKSHOP DEADLINES EXTENDED ** Marcello Balduccini
• [Hol-info] LPAR-22 Ethiopia - Call for Papers geoff
• [Hol-info] 1st Call for Papers Software Verification and Testing Track @ ACM SAC 2019 Matthias Güdemann
• [Hol-info] Second Call for Papers: FSEN 2019 Maurice ter Beek
• [Hol-info] PPDP 2018: Call for Participation David Sabel
• [Hol-info] Keyboard layout with symbols used in HOL4 Mario Xerxes Castelán Castro
• [Hol-info] Call for paper: Only one *week* left to prepare your paper for the Workshop in OCL and Textual Modeling (OCL 2018) Achim D. Brucker
• [Hol-info] Mike Gordon bio Lawrence Paulson
  • [Hol-info] Type abstraction – Re: Mike Gordon bio Ken Kubota
  • Re: [Hol-info] Mike Gordon bio Mario Xerxes Castelán Castro
• [Hol-info] Adding abstraction to terms Dylan Melville
  • Re: [Hol-info] Adding abstraction to terms Mario Xerxes Castelán Castro
  • Re: [Hol-info] Adding abstraction to terms Dylan Melville
  • Re: [Hol-info] Adding abstraction to terms Thomas Tuerk
• [Hol-info] Taking universal quantification off an assumption Dylan Melville
  • Re: [Hol-info] Taking universal quantification off an assumption Mario Xerxes Castelán Castro
  • Re: [Hol-info] Taking universal quantification off an assumption Mario Xerxes Castelán Castro
  • Re: [Hol-info] Taking universal quantification off an assumption Dylan Melville
• [Hol-info] Strange tactic behavior HOL-k10 vs HOL-k12 Waqar Ahmad via hol-info
  • Re: [Hol-info] Strange tactic behavior HOL-k10 vs HOL-k12 Michael.Norrish
• [Hol-info] The Principle of Mathematical Induction – Re: [Coq-Club] I don't believe Coinduction; Please help me grok it :) Ken Kubota
• [Hol-info] String of term with type information? Yaqing Jiang
  • Re: [Hol-info] String of term with type information? Mark Adams
• [Hol-info] Tactic Dylan Melville
  • Re: [Hol-info] Tactic Mario Xerxes Castelán Castro
  • Re: [Hol-info] Tactic Dylan Melville
  • Re: [Hol-info] Tactic Heiko Becker
  • Re: [Hol-info] Tactic Konrad Slind
  • Re: [Hol-info] Tactic Freek Wiedijk
• [Hol-info] Deadline Extension for ACL2 2018 Matt Kaufmann
• [Hol-info] tacticoe Chun Tian (binghe)
  • Re: [Hol-info] tacticoe Ramana Kumar
• [Hol-info] Formalizing logical puzzles Dylan Melville
  • Re: [Hol-info] Formalizing logical puzzles Dylan Melville
  • Re: [Hol-info] Formalizing logical puzzles Jeremy Dawson
  • Re: [Hol-info] Formalizing logical puzzles Petros Papapanagiotou
  • Re: [Hol-info] Formalizing logical puzzles Mario Xerxes Castelán Castro
  • Re: [Hol-info] Formalizing logical puzzles Mario Xerxes Castelán Castro
  • Re: [Hol-info] Formalizing logical puzzles Mario Xerxes Castelán Castro
  • Re: [Hol-info] Formalizing logical puzzles Marco Maggesi
  • Re: [Hol-info] Formalizing logical puzzles Marco Maggesi
• [Hol-info] FLoC 2018 - Last Joint Call for Workshop Participation Andrzej Murawski
• [Hol-info] CICM 2018, Call for Contributions to doctoral programme, work-in-progress, posters, demos, tutorial Serge Autexier
• [Hol-info] FLoC 2018 - Last Call for Participation Andrzej Murawski
• [Hol-info] Kananaskis-12 release of HOL4 Michael.Norrish
• [Hol-info] CFP: One Month Until Left For Submitting to The Workshop in OCL and Textual Modeling (OCL 2018) Achim D. Brucker
• [Hol-info] [DEADLINE EXTENSION] Formal Verification of Physical Systems (FVPS 2018) Umair Siddique
• [Hol-info] WST 2018 - Call for Participation (July 18-19, 2018) Salvador Lucas
• [Hol-info] LPAR-22 in Ethiopia - Call for Papers and Workshops geoff
• [Hol-info] LOPSTR 2018: Second Round Final Call for Papers Fred Mesnard
• [Hol-info] ACL2 2018: Second Call for Papers Matt Kaufmann
• [Hol-info] 23rd International Conference on Engineering Complex Systems - Call for Papers geoff
• [Hol-info] Final CfP: FACS'18 (15th Int'l Conference on Formal Aspects of Component Software) Peter Csaba Ölveczky
• [Hol-info] VTSA 2018: call for applications Stephan Merz
  • Re: [Hol-info] VTSA 2018: call for applications Stephan Merz
• [Hol-info] The two characteristics of an antinomy: self-reference and negation Ken Kubota
• [Hol-info] big records Ramana Kumar
  • Re: [Hol-info] big records Michael.Norrish
• [Hol-info] Loops in HOL4 尚亚龙
  • Re: [Hol-info] Loops in HOL4 Waqar Ahmad via hol-info
  • Re: [Hol-info] Loops in HOL4 尚亚龙
  • Re: [Hol-info] Loops in HOL4 Thomas Tuerk
  • Re: [Hol-info] Loops in HOL4 尚亚龙
  • Re: [Hol-info] Loops in HOL4 Chun Tian
  • Re: [Hol-info] Loops in HOL4 尚亚龙
• [Hol-info] Type Theory vs. Set Theory (HOL, Isabelle/HOL, Q0, and R0 vs. ZFC) – Re: [Metamath] [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument) Ken Kubota

• Earlier messages
• Later messages