Stream: Mirror: Isabelle Users Mailing List

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


view this post on Zulip 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: Dec 05 2021 at 23:19 UTC