[Hol-info] IJCAR 2016 Workshop - Call for Position Statements

IJCAR 2016 Workshop on “Paths not taken: thinking about the process of proof’’ (https://pathsnottakenblog.wordpress.com) 2nd July 2016 in Coimbra, Portugal. In association with IJCAR 2016. Keynote speaker: J Strother Moore, Admiral B.R. Inman Centennial Chair Emeritus in Computing Theory,

[Hol-info] [cfp] 14th IEEE International Conference on Embedded and Ubiquitous Computing (EUC 2016)

14th IEEE International Conference on Embedded and Ubiquitous Computing (EUC 2016) August 24-26, Paris, Francehttp://euc2016.conferences-events.org Introduction Embedded and ubiquitous computing is an exciting paradigm that promises to provide computing and communication services to the end

Re: [Hol-info] Instantiating existentials under existentials

Hi, there is "GEN_EXISTS_TAC "y" `5`" from bossLib. It is more general than what was asked for here originally. It also knows about the usual boolean connectives. For example, it can instantiate also ?x. P x /\ ?z y. ... y ... or with negation ?x. (P x /\ (!z y. ... y ...)) ==> Q x