Legality concepts for three-valued logic programs (Q689286)

The authors consider three-valued propositional logic and interpret the third truth degree (besides 0 and 1) as ``illegal'' or ``unacceptable''. With reference to a background in computer science they get (unusual) truth tables for an implication and -- noncommutative (!) -- conjunction and disjunction connectives. And they add a ``legality'' connective indicating that some formula has a ``legal'' truth degree, i.e. one of the degrees 0,1. For this logic they study Horn clauses and logic programs, introduce Herbrand models and fixpoint semantics. For the class of ``legal'' three- valued logic programs the use of the SLD resolution algorithm is proven to be sound, and it is shown that this algorithm too can be used for a legality check.