User loginNavigation 
Do Logic Languages Need Negation?I have been working on an interpreter for a minisubset of Prolog as I find it interesting how logic languages hold a central place in proofassistants, theoremprovers and typesystems. What I am interested in is a minimal and sound dialect of prolog to server as a starting point for further investigation. There are obviously several design points to discuss, but negation appears to be the most fundamental. Obviously as I am interested in soundness I want to operate in a Herbrand universe, which means unification with an occurs check. The problem with negation seems to stem from the Prolog programming model. It appears to me that at some point "failure/unsat" and "falseness" (and "success/sat" and "truthfulness") have become confused with each other. This leads to negation as failure, the unsoundness of which is easily shown: : not (not (X = 0)), not (not (X = 1)). yes. Various solutions to this have been proposed, threevalued (Kleene) logic, four valued (Belnap) logic, negation as inconsistency, negation as refutation etc. All of those complicate the resolution process, but do solve the problem. Strong negation seems interesting because it is local and not fragile like some of these methods. I particularly liked the combination of a fourvalued logic (because the bilattice structure is nice) and strong negation, and started to look at implementing it. What interested me is that the logic values are seen as success values, so that a functor can be 'true' or 'false' without failing. In which case, why make them special 'values' in the language at all, surely they can be treated as normal atoms? Taking list membership as an example, we might want to define: member(Key, cons(def(Key, _), _), true). member(Key, nil, false). member(Key, cons(_, Tail), X) : member(Key, Tail, X). We can even define 'not' as a predicate (fail if arg is true): not(false). not_member(Key, List) : member(Key, List, X), not(X). or a binary operator not(true, false). not(false, true). not_member(Key, List, X) : member(Key, List, Y), not(Y, X). Without any of the logical unsoundness of negation as failure. There is obviously a parallel with dependent type systems (curryhoward), which I don't think have negation. I have put the source code for my simple logic language "Clors" on GitHub https://github.com/keean/Clors. Its a still experimental, and is suffering form many changes and false starts, so needs a little tidying up (I have just removed metainterpreters because they turn out to be unsound), and needs updating to use my parser combinator library. So the question is, do logic languages need builtin negation? By Keean Schupke at 20140715 09:07  LtU Forum  previous forum topic  next forum topic  other blogs  9204 reads

Browse archivesActive forum topicsNew forum topics 
Recent comments
15 hours 50 min ago
21 hours 38 min ago
1 day 8 hours ago
1 day 8 hours ago
4 days 16 hours ago
4 days 18 hours ago
4 days 22 hours ago
5 days 15 hours ago
6 days 1 hour ago
1 week 15 hours ago