Re: [isabelle] folding and linking in jEdit; curry/split



> On 18.02.2016, at 16:54, Makarius <makarius at sketis.net> wrote:
> 
> The situation in Isabelle is very complex, but by mixing up names, it becomes just one big bog that nobody understands anymore.

I would like to add my grain of salt. At first, I thought the distinction between jEdit and Isabelle/jEdit was somewhat pedantic, but after years of being at the receiving end of bug reports and other comments about "metis" and "smt", and as an originator of material about it, I found that many misunderstandings are just waiting to happen.

To give one example: Metis (Joe Hurd's Metis ATP) is an automatic theorem prover for FOL that is designed to be sound and complete for that logic. "metis" is an Isabelle proof method that (1) translates HOL to FOL; (2) invokes Metis; (3) replays Metis inferences in Isabelle's kernel. Without appropriate context, statements like "metis is first-order" or "metis is higher-order" or "metis is buggy" are close to meaningless.

This having been said, I notice that nobody ever confused Nitpick and its backend Kodkod. I'm grateful I didn't call the tool Isabelle/Kodkod. ;)

Jasmin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.