LEGALITY CONCEPTS FOR 3-VALUED LOGIC PROGRAMS

In several application fields, sentences can assume, besides the usual values true and false, a third value that signals their unacceptabili ty. This may happen when a query to a database violates the database c onstraints or in typed logic programming, where a goal which does not satisfy the type constraints can be considered unacceptable. Here a th ree-valued Horn logic is presented, where the third value has the mean ing of ''illegal'', i.e. unacceptable. The extension of the convention al logic operators is considered, and a model-theoretic semantics for three-valued Horn programs is provided, which allows a formal definiti on of legality (i.e. acceptability) of logic Formulas and programs. Fo r the class of legal three-valued logic programs the use of the tradit ional SLD resolution algorithm is proven to be sound. Finally, it is s hown that the legality check of a three-valued logic program can be al so carried out through SLD resolution.