Logic Programming and Inductive Definitions

Marc Denecker (KU Leuven)
12-05-2021, 16:00
Zoom Meeting ID: 527 800 0011, Passcode: 1NkkUz

There are two introductions in this talk. The first one is about a 45 years old but  unsolved problem: the problem of the declarative semantics of logic programming with negation as failure. We explain the nature of the problem and see the three main ideas for informal semantics of Logic : logic programs (LP) as sets of material implications augmented with Closed World Assumption, logic programs as default theories, and logic programs as definitions. We then focus on the third proposal.

The second introduction is about the concept of definition in general, and inductive definitions more specifically. It is a short (and incomplete) overview of existing work on this fundamental topic, with focus on what is relevant for this talk: syntax and semantics (rather than expressivity and definability).

We discuss the view of logic programs as inductive definitions, the merits of this view, and how and where it was (not) presented in the literature on LP semantics. It will be argued that the least (Herbrand) model semantics for definite programs, and the well-founded model semantics for general programs formalizes the informal semantics of logic programs as generalized forms of inductive definitions.

In the last part of the talk, we point to some unacceptable practical expressivity limitations of pure logic programming from a Knowledge Representation point of view, and discuss some easy and obvious extensions to alleviate them. This results in a natural and expressive language construct for defining relations, that can be integrated in classical logic resulting in an alternative for Answer Set Programming.  This work is based on "Extending Classical Logic with Inductive Definitions, International Conference on  Computational Logic' (CL 2000)https://arxiv.org/pdf/cs/0003019, which received last year's   "The John Alan Robinson 20 Year Test of Time Award" at ICLP 2020.