Re: [isabelle] Kleene's Ternary Logic



Am 28.08.2013 um 11:55 schrieb Lawrence Paulson <lp15 at cam.ac.uk>:

> I have to agree. I've never seen a convincing application of a 3-valued logic.

I presume you mean in specification languages like LCF and HOL. Abstract interpretation naturally leads to 3-valued logics [1], and tools like Refute and Nitpick, which need to approximate infinite domains, make ample use of them. Ultimately, Nitpick translates 3-valued logic formulas into 2-valued logic ones, because the user is interested in a binary outcome (a genuine countermodel was found or not) and the underlying engine is 2-valued, but as an intermediate step it is useful to be able to talk about things like an unknown (e.g. too big) "nat" and use Kleene rules to remain precise and sound.

Jasmin

[1] http://www.cs.tau.ac.il/~tvla/



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