First-Order Modular Logic Programs and their Conservative Extensions (Extended Abstract)

1 Introduction

Answer set programming is a prominent knowledge representation paradigm with roots in logic programming [Leake, 2016]. It is especially useful for addressing combinatorial search problems. In answer set programming, a given computational problem is represented by a declarative program that describes the properties of a solution to the problem. Then, an answer set solver is used to generate answer sets, also called stable models, for the program. These models correspond to solutions to the original problem.

In this paper we show how some logic programs under the answer set semantics can be viewed as consisting of various "modules", and how stable models of these programs can be computed by composing the stable models of the modules. We call collections of such modules first-order modular programs. To illustrate this approach consider the following two rules

Intuitively, these rules encode that the relation r is the transitive closure of the relation in. The empty set is the only answer set of the program composed of these rules alone. Thus, in some sense the meaning of these two rules in isolation is the same as the meaning of any program that has a single answer set that is empty. (The empty program is an example of another program with a single empty answer set.) We show

Yuliya Lierler

University of Nebraska Omaha ylierler@unomaha.edu

how to view rules (1) and (2) as a module and use the operator SM introduced by Ferraris et al. (2011) to define a semantics that corresponds more accurately to the intuitive meaning of these rules. The operator SM provides a definition of the stable model semantics for first-order logic programs that does not refer to grounding or fixpoints as does the original definition [Gelfond and Lifschitz, 1988]. The operator SM has proved an effective tool for studying properties of logic programs with variables, which are the focus of this paper.

Modularity is essential for modeling large-scale practical applications. Here we propose first-order modular programs and argue their utility for reasoning about answer set programs. We use the Hamiltonian Cycle problem as a running example to illustrate that a "modular" view of a program gives us

• a more intuitive reading of the parts of the program;
• the ability to incrementally develop modules or parts of a program that have stand-alone meaning and that interface with other modules via a common signature;
• a theory for reasoning about modular rewritings of individual components with a clear picture of the overall impact of such changes.

First-order modular programs can be viewed as a generalization of propositional modular logic programs [Lierler and Truszczy´nski, 2013]. In turn, propositional modular logic programs generalize the concept of modules introduced by Oikarinen and Janhunen 2008. ASP-FO logic [Denecker et al., 2012] is another related formalism. It is a modular formalization of generate-define-test answer set programming [Lifschitz, 2002] that allows for unrestricted interpretations as models, non-Herbrand functions, and first-order formulas in the bodies of rules. An ASP-FO theory is a set consisting of modules of three types: G-modules (G for generate), D-modules (D for define), and T-modules (T for test). In contrast, there is no notion of type among modules in the modular programs introduced here.

We also define conservative extensions for first-order modular programs. This concept is related to strong equivalence for logic programs [Lifschitz et al., 2001]. If two rules are strongly equivalent, we can replace one with the other within the context of any program and the answer sets of the resulting program coincide with those of the original one. Conservative extensions allow us to reason about rewritings even when the rules in question have different signatures. The theorem stated at the end of this paper, for instance, shows that conservative extensions can be used to justify the projection rewriting [Faber et al., 1999], which is commonly employed to improve program performance. Consider the rule

which says that every vertex must be reachable from every other vertex. This rule can be replaced with the following three rules without affecting the stable models in an "essential way"

Furthermore, this replacement is valid in the context of any program, as long as that program does not already contain either of the predicates v1 and v2. Currently, these performance-enhancing rewritings are done manually. We expect the theory about conservative extensions developed here to provide a platform for automating such rewritings in the future. We note that conservative extensions are related to the notion of knowledge forgetting in [Wang et al., 2014]. However, that work applies only to propositional programs.

2 Review: Traditional Programs

A (traditional logic) program is a finite set of rules of the form

(0 ≤ k ≤ l ≤ m ≤ n), where each ai is an atomic formula, possibly containing function symbols, variables, or the equality symbol with the restriction that atomic formulas a1, . . . , ak and am+1, . . . ,an may not contain the equality symbol. The expression containing atomic formulas ak+1 through an is called the body of the rule. A rule with an empty body is called a fact. An instance of a rule R in a program P is a rule that can be formed by replacing all variables in R with ground terms formed from function symbols and object constants occurring in P. The process of grounding a traditional logic program consists of the following steps:

1. each rule is replaced with all of its instances by substituting ground terms for variables;
2. in each instance, every atomic formula of the formt1 =t2 is replaced by ⊤ if t1 is the same as t2 and by ⊥ otherwise.

It is easy to see that the resulting ground program does not have equality symbols and can be viewed as a propositional program. The answer sets of a traditional program P are stable models of the result of grounding P, where stable models are defined using the fixpoint operation introduced in [Ferraris, 2005].

Traditional programs do not include some constructs available in ASP input languages. (For example, aggregate expressions and arithmetic are not covered.) Even so, they do cover a substantial practical fragment. In particular, according to [Ferraris and Lifschitz, 2005] and [Ferraris, 2005], rules of the form (4) are sufficient to capture the meaning of the commonly used choice rule construct. For instance, the choice rule {p(X)}←q(X) is understood as the rule

Consider the Hamiltonian Cycle problem on an undirected graph. A Hamiltonian Cycle is a subset of the set of edges in a graph that forms a cycle going though each vertex exactly once. A sample program for finding such a cycle can be constructed by adding rules (1), (2), and (3) to the following:

Each answer set of the Hamiltonian Cycle program above corresponds to a Hamiltonian cycle of the given graph, specified by facts (5), so that the predicate in encodes these cycles. If an atom in(a,b) appears in an answer set it says that the edge between a and b is part of the subset forming the Hamiltonian cycle. Intuitively,

• the facts in (5) define a graph instance by listing its edges, and rule (6) ensures that this edge relation is symmetric (since we are dealing with an undirected graph); the vertices of the graph are implicit-they are objects that occur in the edge relation; 1
• rule (7) says that any edge may belong to a Hamiltonian cycle;
• rules (8) and (9) impose the restriction that no two edges in a Hamiltonian cycle may start or end at the same vertex, and rule (10) requires that each edge appears at most once in a Hamiltonian cycle (recall that in(a,b) and in(b,a) both encode the information that the edge between a and b is included in a Hamiltonian cycle);
• rules (1) and (2) define a relation r (reachable) that is the transitive closure of relation in;
• rule (3) ensures that every vertex in a Hamiltonian cycle must be reachable from every other vertex.

Clearly, rules in the program can be grouped according to intuitive meaning. Yet, considering these groups separately will not produce "meaningful" logic programs under the answer set semantics as discussed in the introduction. In this paper, we show how we can view each of these groups of rules as a separate module, and then use the SM operator [Ferraris et al., 2011; 2009], along with a judicious choice of "intensional" and "extensional" predicates to achieve a more accurate correspondence between the intuitive reading of the groups of rules and their model-theoretic semantics.

3 Operator SM

The SM operator was introduced by Ferraris et al. (2011; 2009). There are a few key differences between the original stable model semantics and the semantics provided by the SM operator that make the latter a convenient formalism for facilitating a view of groups of rules in a program as separate units or "modules". First, the SM operator does not rely on grounding, but instead operates on first-order sentence representations of logic programs. Secondly, the semantics as defined by SM allows for a distinction between "extensional" and "intensional" predicates. Intuitively, "extensional" predicates correspond to the input of the program, or module, and "intensional" predicates correspond to output or auxiliary concepts. Finally, unlike the original stable model semantics, the SM operator does not involve a fixpoint calculation, but instead defines stable models as models of a second-order formula. The result of applying the SM operator to a first-order sentence F with intensional predicates p is a second-order formula, denoted SMp[F].

1 This precludes graphs that include isolated vertices.

The SM operator applies to first-order sentences, rather than to logic programs. Yet, traditional logic programs can be identified with the first-order sentences of a particular form. For example, we understand the Hamiltonian Cycle program presented in Section 2 as an abbreviation for the conjunction of the following formulas

where a,a′ , . . .c,c′ are object constants and x,y,z,z′ are variables.

The answer sets of any traditional program P that contains at least one object constant coincide with Herbrand models of SMp[P], where p is the list of all predicates occurring in P.

4 Modular Logic Programs

A first-order modular logic program is a collection of logic programs, where the SM operator is used to compute models of each individual logic program in the collection.

We call a formula of the form SMp[F], where p is a tuple of predicate symbols and F is a traditional program, a defining module (of p in F) or a def-module. We can view any traditional program P as a def-module SMp[P], where p is the list of all predicates occurring in P. A first-order modular logic program (or, modular program) P is a finite set of def-modules

By s(P) we denote the set of all function and predicate symbols occurring in a modular program P, also called the signature of P. A stable model of a modular program P is any interpretation over s(P) that is a model of the conjunction of all def-modules in P.

We now illustrate how modular programs capture the encoding (11) of the Hamiltonian Cycle so that each of its modules carries its intuitive meaning. The modular program Phcconsists of five def-modules:

∀xy((in(x, y) ∧ in(y, x)) → ⊥)]

The def-modules shown above correspond to the intuitive groupings of rules of the Hamiltonian Cycle encoding discussed in Section 2.

• A model of def-module (12) is any interpretation I over s(Phc) such that the extension 2 of the edge predicate in I corresponds to the symmetric closure of the facts in (5).
• A model of def-module (13) is any interpretation I over s(Phc) such that the extension of the predicate in in I is a subset of the extension of the predicate edge in I.
• A model of def-module (14) is any interpretation I over s(Phc) that satisfies the conjunction in (14).
• A model of def-module (15) is any interpretation I over s(Phc), where relation r is the transitive closure of relation in.
• A model of def-module (16) is any interpretation I over s(Phc) that satisfies the implication in (16).

Any interpretation over s(Phc) that satisfies the conditions imposed by every module is a stable model of Phc.

5 RelatingModular Programs and Traditional Programs

We view a traditional logic program as an abbreviation for a first-order sentence formed as a conjunction of formulas of

which corresponds to rule (4). The symbol ˜∀ denotes universal closure. We call the disjunction in the consequent of a rule (17) its head, and the conjunction in the antecedent its body. The conjunction ak+1 ∧· · ·∧al constitutes the positive part of the body. A modular program is called simple if for every def-module SMp[F], every predicate symbol p occurring in the head of a rule in F occurs also in the tuple p. For instance, Phc is a simple modular program.

The dependency graph [Ferraris et al., 2009] of a simple modular program P, denoted DG[P], is a directed graph that

• has all intensional predicates in P as vertices, and

2 The extension of a predicate in an interpretation is the set of tuples that satisfy the predicate in that interpretation.

• has an edge from p to q if there is a def-module SMp[F] ∈ P containing a rule with p occurring in the head and q occurring in the positive part of the body.

We call a simple modular program P coherent if

• (i) no two def-modules in P have overlapping intensional predicates, and
• (ii) every strongly connected component in the dependency graph of P is contained within p for some def-module SMp[F] in P.

From the symmetric splitting result from [Ferraris et al., 2009] it follows that the Herbrand stable models of a coherent modular program P that (i) contains at least one object constant and (ii) has each predicate symbol in P occurring in p for some def-module SMp[F], coincide with the answer sets of the traditional program constructed as the conjunction of all first order sentences occurring in this modular program.

The strongly connected components of the dependency graph of Phc each consist of a single vertex. It is easy to check that the Hamiltonian Cycle program Phc is coherent and that all of its predicate symbols are intensional in some defmodule. Therefore, the Herbrand models of Phc coincide with the answer sets of (11) so that answer set solvers can be used to find these models.

Arguably, when answer set practitioners develop their applications they intuitively associate meaning with components of their programs. We believe that modular programs as introduced here provide us with a suitable model for understanding the meaning of these components.

6 Conservative Extensions

In this section, we study the question of how to formalize common rewriting techniques used in answer set programming, such as projection, and argue their correctness.

For an interpretation I over signature s and a function symbol (or, predicate symbol) t from s by t I we denote a function (or, relation) assigned to t by I. Let s and S be signatures so that s ⊂S. For interpretation I over S, by I|s we denote the interpretation over s such that for every function or predicate symbol t in s, t I = t I|s . Let P and P′ be modular logic programs such that the set of all predicates occurring in P is a subset of the set of all predicates in P′ and both programs share the same function symbols. We say that P′ is a conservative extension of P if M ↦→M|s(P) is a 1-1 correspondence between the models of P′ and the models of P. It turns out that we can replace def-modules in a modular program with their conservative extensions and are guaranteed to obtain a conservative extension of the original modular program. Thus, conservative extensions of def-modules allow us to establish something similar to strong equivalence accounting for the possibility of different signatures.

For example, consider the choice rule {p}, a shorthand for the rule p←not not p. In some answer set programming dialects double negation is not allowed in the body of a rule. It is then common to simulate a choice rule as above by introducing an auxiliary atom ˆp and using the rules p←¬ ˆp and ˆp←¬p. It is easy to check that SMp, ˆp[(¬ ˆp→ p)∧(¬p→ ˆp)] is a conservative extension of SMp[¬¬p→ p]. It follows that we can replace the latter with the former within the context of any modular program not containing the predicate symbol ˆp, and get a conservative extension of the original program.

Similarly, replacing def-module (16) in the Phc by

results in a conservative extension of the original program. This follows from a more general fact about the projection rewriting stated below.

Let R be a rule (17) occurring in a traditional logic program F, and let x be a non-empty tuple of variables occurring only in the body of R. By a(x,y) we denote the conjunction of all conjunctive terms in the body of R that contain at least one variable from x, where y denotes all the variables occurring in these conjunctive terms but not occurring in x. By b we denote the set of all conjunctive terms in the body of R that do not contain any variables in x. By g we denote the head of R. Let t be a predicate symbol that does not occur in F. Then the result of projecting variables x out of R using predicate symbol t is the conjunction

We can project variables out of a traditional logic program by successively projecting variables out of rules. For example, first projecting z out of the traditional logic program in (16) and then projecting z′ out of the first rule of the resulting program yields program (18).

Theorem Let SMp1,...,pk [F] be a def-module and R be a rule in F. Let x denote a non-empty tuple of variables occurring in the body of R, but not in the head. If G is constructed from F by replacing R in F with the result of projecting variables x out of R using a predicate symbol pk+1 that is not in the signature of F, then SMp1,...,pk+1 [G] is a conservative extension of SMp1,...,pk [F].

This theorem can be restated in terms of traditional logic programs using the fact that any traditional program can be viewed as a def-module.

7 Conclusion

In this paper, we introduced first-order modular logic programs as a way of viewing logic programs as consisting of many independent, meaningful modules. We also defined conservative extensions, which like strong equivalence for traditional programs, can be useful for reasoning about traditional programs and modular programs. We showed how these concepts justify the common projection rewriting.

Acknowledgments

Many thanks to Joshua Irvin, Vladimir Lifschitz, and Miroslaw Truszczynski for useful discussions regarding ideas in this paper. Thanks as well to the anonymous referees for helpful comments. Amelia Harrison was partially supported by the National Science Foundation under Grant IIS1422455. Yuliya Lierler was partially supported by University Committee on Research and Creative Activity from the University of Nebraska at Omaha in Summer 2016.