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 <>

Is it possible to translate TPTP dialecs (e.g. higher order logic) into Isabelle/HOL or parts of it (e.g. as used in (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 but I am not sure whether I am on the right path.



Last updated: Jan 25 2022 at 01:11 UTC