TXF and THF

with Evgeny, Martin, others

• TXF extends TFF with

  Boolean terms, tuples, $ite, and $let
  • This web page provides examples
  • TX0 and TX1 are the extensions of TF0 and TF1

• THF will have (updated)

  tuples, $ite, and $let
  • This web page provides examples

• TPTP v8.0.0 with TXF

  will be released in the first half of 2022

• CASC

  • CASC-J11 in 2022 will have LTB with TXF problem versions, and THF problem versions with $ite and $let
  • CASC-J11 in 2022 will (hopefully) have SLH using THF with $ite and $let
  • CASC-29 in 2023 will have a TXA division - TXF with arithmetic