From: Alex Meyer <email@example.com>
Is it possible to translate TPTP dialecs (e.g. higher order logic) into Isabelle/HOL or parts of it (e.g. as used in https://www.isa-afp.org/entries/GoedelGod.html) (with all the reservations that Isabelle has no single language, it is expanding languge with sugar introduced with each additional theory)? TPTP seems to be so far removed from how the actual classical logic or lambda calculus looks.
I am reading https://smolka.st/papers/isar_jar.pdf but I am not sure whether I am on the right path.
Last updated: Dec 05 2021 at 23:19 UTC