Definitions
-----------
+ Used effectively by THF systems, including Zipperp'n (Petar), Satallax, Leo-III (Chris).
+ Happy to leave used = and <=>, no need for := to indicate orientation (Alex, all).
+ Syntactic use is to expand all LHS symbols to the RHS definition (Geoff, all).
  Can be done as a preprocessing step. Therefore non-recursive.
+ Semantic use is to indicate origin (Cezary)
+ Semantic use can be useful, but might be used inconsistently (MartinS)
+ Plan will be to use the definition role for the syntactic case.
+ ACTION: Geoff and MartinS to write standards for what a syntactic definition can look like,
  for all the languages. See also below about $let expressions.
+ ACTION: Geoff to clean up all uses of the definition role for the syntactic case. Set the role
  for non-standard uses to axiom, and add a comment that the old role was prolly semantic.
+ Vampire fishes for syntactic definitions (MartinS)
+ Maybe provide meta-data to differentiate between the two uses (David).
+ Maybe use different connectives for syntactic and semantic uses?

Sequents
--------
+ Useful for non-classical logics (Claudia)
+ Tanels' intuitionistic prover can use sequents (Claudia)
+ Plan: Leave in

TXF and THF
-----------
+ Johannes Schoisswohl might be able to provide TXA problems (Ahmed, Petra)
Tuples:
+ Are tuples ever useful as terms? (Stephan (thinks not)). Adds complexity without added
  expressivity - can always be expanded using a new type and a new function with the tuple
  elements' types as arguments types and the new type as result.
+ Users might find them useful (Geoff, Adam)
+ There are no extractor functions (Alex asked)
+ Used in non-classical logic semantics specifcations, but that is not a logical term.
+ Used in sequents.
+ ACTION: Geoff to leave in, but comment out (or comment about) the use of tuples as terms.
$let expressions:
+ The rules for what the definitions in a $let, and in a definition formula, should be compatible.
  - Variables are free (not really variables) in $let, but quantified in definition formulae.
  - ACTION: Geoff to try use = or <=> in $let definitions, instead of := (but I failed before)
+ $let with tuples of types and definitions (parallel let) is more powerful than nested $let 
  (let*), as in Evgeny's thesis (Stephan)

Non-classical Logic
-------------------
+ Note to Alex, the long forms for altheic modal will be {$necessary} and {$possible} (not
  {$box} and {$dia} - for generic box and diamond use the short forms).
+ All long forms will be defined by the TPTP.
+ Currently a formula's properties are captured in the semantics specifcations by using the
  formula name - that's dirty. Maybe use meta-data instead (David).
+ Concern about writing parsers (Claudia). ACTION: Geoff to write exports using TPTP4X (which
  needs to be upgraded for non-classical logic)
+ ACTION: Geoff to release latest SyntaxBNF.

Github
------
+ Nice to be able to work from command line (Giles)
+ Use Active Pages to produce tagged releases with users' selections of problems (selected ala
  TPTP2T), which users can then clone (Giles)
+ Use Github to submit problems - SMT does that, but using a public repository and pull requests.
  Sadly that makes all submitted probvlem public (not the TPTP idiom for CASC). Need a better
  plan, but the idea is good.
+ ACTION: Geoff to write up senior UG project specification(s) for Stephan and Kostya.
+ ACTION: Kostya to give his deadline for the project specifications in the spring.

Other
-----
+ Use something like Jupyter notebooks to interact withe TPTP World (David). Look at kaggle.com
+ Create Docker images of systems, maybe directly from StarExec packages (Giles). What would
  such images be used for (maybe in Kaggle - ACTION: Geoff to look into that).