Email Gateway (Aug 19 2022 at 11:44): Email Gateway (Aug 19 2022 at 11:44):From: Arthur Peters <amp@singingwizard.org>
Is there an existing theory of Kleene's Termary Logic written is Isabelle?
A search didn't show up anything.
I need it for representing that predicates that reference unbound variables
are neither true nor false.
Thanks.
-Arthur
Email Gateway (Aug 19 2022 at 11:45):From: "Jens-D. Doll" <jd@cococo.de>
Hello Arthur,
afaik you will have to distinguish these cases, independent of bound state,
a) a tautology, which is always true
b) the absurd, which is always false
c) there is an x s.th. p(x) is true, which really depends on the bound x
Jens
Is there an existing theory of Kleene's Termary Logic written is Isabelle?
A search didn't show up anything.
I need it for representing that predicates that reference unbound variables
are neither true nor false.
Thanks.
-Arthur
Email Gateway (Aug 19 2022 at 11:45):From: Lawrence Paulson <lp15@cam.ac.uk>
I have to agree. I've never seen a convincing application of a 3-valued logic. Even LCF, with its undefined values, didn't have undefined truth values.
Larry Paulson
Email Gateway (Aug 19 2022 at 11:45):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
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/
Email Gateway (Aug 19 2022 at 11:49):From: "Jens-D. Doll" <jd@cococo.de>
Hello Jasmin,
the reason and a justification of using 3-valued logic in praxi is the
incompleteness of formal systems, i.e. Goedel's sentence as of 1931. The
software for Abtract Interpretation is a formal system and there will
always be branches, which are unsolved/unproved or just
not-yet-thought-of. What they are doing in these unsolved cases is manual
investigation, which leads to a lot of work for highly trained engineers.
Jens
Last updated: Apr 19 2024 at 12:27 UTC