search

leoprover / Leo-III

An Automated Theorem Prover for Classical Higher-Order Logic with Henkin Semantics
http://inf.fu-berlin.de/~lex/leo3
BSD 3-Clause "New" or "Revised" License
41 stars 10 forks source link

Isabelle/HOL #40

Closed jparsert closed 6 years ago

jparsert commented 7 years ago

Hi, I was wondering if Leo-III can already be used with Isabelle. If not, is there anyone currently working on an interface?

cbenzmueller commented 7 years ago

Hi,

no I don't think that somebody is currently working on an interface. So there seems room for contributions.

Best, C.

-- Priv.-Doz. Dr.-Ing. Christoph Benzmüller Faculté des Sciences, de la Technologie et de la Communication, Avenue de l'Université, L-4365 Esch-sur-Alzette, Luxembourg Further Affiliations: Freie Universität Berlin, Department of Mathematics and Computer Science Saarland University, Department of Computer Science http://christoph-benzmueller.de c.benzmueller@gmail.com | christoph.benzmueller@uni.lu | c.benzmueller@fu-berlin.de

On Mon, Aug 14, 2017 at 5:29 AM, Julian Parsert notifications@github.com wrote:

Hi, I was wondering if Leo-III can already be used with Isabelle. If not, is there anyone currently working on an interface?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/leoprover/Leo-III/issues/40, or mute the thread https://github.com/notifications/unsubscribe-auth/AEweRW6PBD73CtdEZmcIRHQlna5EMOGQks5sX78ogaJpZM4O16HM .

jparsert commented 7 years ago

I see, who was the person responsible for the Leo2 interface for isabelle?

cbenzmueller commented 7 years ago

Well, Jasmin Blanchette was involved, I guess, and Nik Sultana.

Best, C.

-- Priv.-Doz. Dr.-Ing. Christoph Benzmüller Faculté des Sciences, de la Technologie et de la Communication, Avenue de l'Université, L-4365 Esch-sur-Alzette, Luxembourg Further Affiliations: Freie Universität Berlin, Department of Mathematics and Computer Science Saarland University, Department of Computer Science http://christoph-benzmueller.de c.benzmueller@gmail.com | christoph.benzmueller@uni.lu | c.benzmueller@fu-berlin.de

On Mon, Aug 14, 2017 at 12:28 PM, Julian Parsert notifications@github.com wrote:

I see, who was the person responsible for the Leo2 interface for isabelle?

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/leoprover/Leo-III/issues/40#issuecomment-322155986, or mute the thread https://github.com/notifications/unsubscribe-auth/AEweRQQxqllWCeqf2CbBsKe7Np6AIeZ9ks5sYCFIgaJpZM4O16HM .

lex-lex commented 6 years ago

Leo-III is now integrated into the current development version of Isabelle (see http://isabelle.in.tum.de/repos/isabelle/rev/41f1f8c4259b). Note that, however, we will need to wait for the next Isabelle release to have this integration delivered with a current Isabelle version.