00:41:45 Jasmin Blanchette: Not yet decided. 00:42:48 Jasmin Blanchette: Where CASC 00:46:53 Alexander Steen: grep ",definition," . -r | wc -l 68935 00:52:21 Petar Vukmirovic: so far I have sseen it in HO only 00:52:29 Alexander Steen: RNG105+2 00:52:36 Alexander Steen: fof(mDefMod,definition 00:54:08 Jasmin Blanchette: We don't want recursive defs in HOL. 00:55:13 Alexander Steen: grep ",definition," . -r --include="*+*.p" | wc -l 4037 01:03:33 David Fuenmayor: what about adding custom metadata to formulas? 01:04:41 Michael Rawson: There are kind of two "formula roles" in general, not just for "definition" - roles that gives background information (like the Mizar export) and roles that systems have to do something (like "unfold this definition" or "prove this conjecture"). 01:05:28 Christoph Benzmüller: axiom[abbreviation] and axiom[definition] 01:05:51 Petar Vukmirovic: E as well :) 01:06:57 Alexander Steen: i like the idea that provers need to know what to do with special formulas, this should not be the burden of the user (to some extent), i think. 01:09:38 Pierre Grenon: You may have equivalence statements that could look like equivalence for the same sentence on the left hand side, but as a user you may want one to be used as syntactic sugar and the other to be used only as an equivalence. I have no view on the prover's behaviour but writing theories, it is sometimes useful to encode the intended role of a formula as a definition 01:10:19 Pierre Grenon: Yes, apologies, FOL obsessed here 01:11:46 David Fuenmayor: I am totally pro sequents! 01:12:39 Ahmed Bhayat: Vampire cannot parse HOL sequence (not sure about the fog ones) 01:12:41 David Fuenmayor: proof theorists developping ATPs may someday find an use for them (hopefully!) 01:12:49 Ahmed Bhayat: *sequents 01:22:11 Alexander Steen: are there extractor functions for tuples? 01:39:15 Michael Rawson: Could tuples be an extension of the current "product" type "(t * s)", rather than a separate type/thing? Just a thought. 01:39:38 Michael Rawson: (sorry for text-only, somebody is drilling outside my window) 01:41:48 David Fuenmayor: btw, the hypothetical sequents' user might also have an use for tuples (just speculating ;) 01:42:44 David Fuenmayor: just speculating ;) 01:43:19 Michael Rawson: Then "f(foo, bar)" is merely "f applied to (foo, bar)". ;-) 01:43:58 Michael Rawson: Correct! 01:50:39 Michael Rawson: Willing, not necessarily able. 01:55:31 Michael Rawson: Johannes Schoisswohl, no? 02:17:10 Geoff Sutcliffe: Got you Ahmed, when he finishes 02:17:48 Geoff Sutcliffe: Got you Claudia 02:22:55 Geoff Sutcliffe: Got you David 02:26:10 Cláudia Nalon: Me! 02:37:29 Pascal Fontaine: We are using a local server using gitlab 02:37:33 Pascal Fontaine: for SMT 02:38:17 Giles Reger: SMT split things up into multiple repositories. It has the advantage that you can just grab one kind of benchmarks instead of everything. Disadvantage is that it’s harder to get everything! 02:43:57 Adam Pease: FGV and IBM 02:46:15 David Fuenmayor: are there any thoughts on integrating things like Jupyter notebooks in the TPTP world? Notebooks are used e.g. in machine learning to run competitions (www.kaggle.com) 02:48:59 Giles Reger: Other idea - dockerized theorem provers on DockerHub to supplement the great work on maintaining provers on StarExec. 02:50:06 Giles Reger: One advantage is that once you have a Dockerized theorem prover the steps to run it on AWS in a massive experiment there are much shorter. 02:50:21 Stephan Schulz: Last year the official deadline for offering student theses was September 17th....this year it will be something similar. 02:50:29 Adam Pease: (1) Is there an official ANTLR grammar for the TPTP family of languages ? (is it the one from Alexander Steen and Tobias Gleißner) (2) has the Java tptp_parser package (that your students provided to me around 2008) been brought up to date with ANTLR4 and the latest grammar? 02:57:10 Michael Rawson: Afraid so, but that's written as parser combinators so no ANTLR for you nice people. :-( 03:01:49 Pierre Grenon: Thank you! 03:01:52 Giles Reger: Thanks! 03:02:08 Cláudia Nalon: Nice to see you all! Thanks Geoff for organising this! 03:02:21 Christian Franck: Thank you!