Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Translation of TPTP to Isabelle/HOL?

Email Gateway (Aug 21 2020 at 07:44):

From: Alex Meyer <alex153@outlook.lv>
Hi!

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.

Thanks!

Alex

Last updated: Jan 04 2025 at 20:18 UTC