Legality concepts for three-valued logic programs

In several application fields, sentences can assume, besides the usual values true and false, a third value that signals their unacceptability. This may happen when a query to a database violates the database constraints or in typed logic programming, where a goal which does not satisfy the type constraints can be considered unacceptable. Here a three-valued Horn logic is presented, where the third value has the meaning of “illegal”, i.e. unacceptable. The extension of the conventional logic operators is considered, and a model-theoretic semantics for three-valued Horn programs is provided, which allows a formal definition of legality (i.e. acceptability) of logic formulas and programs. For the class of legal three-valued logic programs the use of the traditional SLD resolution algorithm is proven to be sound. Finally, it is shown that the legality check of a three-valued logic program can be also carried out through SLD resolution.