2020-05-12 12:16:6 (GMT)
Petar noticed that even the TH1 problems in the LTB category contain encodings of connectives. For example this definition of a new "not" symbol:
thf(logicdef_2E_7E,axiom,(
! [V0: $o] :
( ( c_2Ebool_2E_7E @ V0 )
<=> ( (~) @ V0 ) ) )).
The GRUNGE paper also mentions this in the section "Translating to TH1":
The TPTP logical connectives ∧, ∨, ⇒, ¬, =, ∀, ∃ are used at the top-level of
the translated formula whenever possible, but the corresponding HOL4 constants
are used when necessary. Equivalences relating HOL4 logical constants to TPTP
connectives are included.
Why can't the native connectives be used throughout in TH1?
2020-05-12 12:50:34 (GMT)
Alex, indeed this is ridiculous.