Predicate Answer Set Programming via coinductive Logic Programming

Answer Set Programming (ASP) is a powerful paradigm based on logic programming for non-monotonic reasoning. Current ASP implementations are restricted to "grounded range-restricted function-free normal programs" and use an evaluation strategy that is "bottom-up" (i.e., not goal-driven). Recent introduction of coinductive Logic Programming (co-LP) with coinductive SLDNF resolution (co-SLDNF) has allowed the development of top-down query-driven goal-directed evaluation strategies for ASP. In this paper we present co-LP with co-SLDNF and its application to the implementation of a predicate ASP solver. Our novel method eliminates the need for grounding and allows functions, to overcome current restriction of current ASP solver, toward the development of a truly predicate ASP solver. The resulting coinductive ASP solver (co-ASP Solver) provides a powerful, practical and efficient predicate ASP solver to handle effectively a large class of predicate answer set programs including possibly infinite ones. We apply our solution strategy to answer programs (e.g., move-win and Schur number problem) to demonstrate our co-ASP Solver with performance result.