"Kleene Logics and their application to the Semantics of Logic Programs"

João Barbosa has a Bachelor degree in Physics, with minor in Informatics, a Master Degree in Computer Science, and a Doctorate in Computer Science, all in the Faculty of Science of the University of Porto. He started his research trying to describe a type discipline for logic programming, which is typically untyped. His Master thesis was based on the concept of regular types and a subset of those, called Closed Types. In his PhD thesis, he described a three-valued declarative semantics for logic programming, a type system and a type inference algorithm which inferred Closed Types. He also described a typed operational semantics for logic programming that was based on the same three-valued logic and described how it can be extended from the traditional operational semantics (SLD-resolution) and used to detect type errors in programs/queries.
Recently he is expanding his research into automated theorem proving, and program verification.

Title

"Kleene Logics and their application to the Semantics of Logic Programs"

Abstract

Logic programming represents programs and queries using Horn clauses. Then, one computes (using resolution) if the querry is a consequence of the program. The paradigm is attrative for its declarative semantics and easy way to assign meaning to programs. Traditionally, the declarative semantics for a logic program is a model, a set of literals with truth value true, such that if the body of a clause evaluates to true, then the head of the clause also evaluates to true, for every possible instance of the clause. However, in some contexts, it may not be easy nor possible to assign the value true or false to a literal, or the operational semantics reaches a state not contemplated by the declarative semantics (type error, non-termination, etc.). This difficults program analysis, debugging, and creates a gap between the declarative semantics and the operational semantics that were supposed to be equivalent.
As a means to solve this problem, several three-valued semantics for logic programming have ben proposed, where the third value corresponds to different behaviours from returning true or false. In order to make sense of having a third value in the semantics, a three-valued logic is used and the definition of model is adapted.
Here I present the main three-valued logics as well as their application to logic programming semantics in different contexts.