Founded Semantics and Constraint Semantics of Logic Rules

Abstract

Logic rules and inference are fundamental in computer science and have been studied extensively. However, prior semantics of logic languages can have subtle implications and can disagree significantly.

This paper describes a simple new semantics for logic rules, founded semantics, and its straightforward extension to another simple new semantics, constraint semantics, that unify the core of different prior semantics. The new semantics support unrestricted negation, as well as unrestricted existential and universal quantifications. They are uniquely expressive and intuitive by allowing assumptions about the predicates and rules to be specified explicitly. They are completely declarative and relate cleanly to prior semantics. In addition, founded semantics can be computed in linear time in the size of the ground program.

This work was supported in part by NSF under grants CCF-1414078, CNS-1421893, IIS-1447549, CCF-1248184, CCF-0964196, and CCF-0613913; and ONR under grants N000141512208 and N000140910651.

A Comparison of Semantics for Well-Known Small Examples and More

Table 2 shows well-known example rules and more for tricky boundary cases in the semantics, where all uncertain predicates that are in a conclusion are declared complete, but not closed, and shows different semantics for them.

Table 2. Different semantics for programs where all uncertain predicates that are in a conclusion are declared complete, but not closed. “uncertain” means all predicates in the program are declared uncertain. “certain” means all predicates in the program that can be declared certain are declared certain; “–” means no predicates can be declared certain, so the semantics is the same as “uncertain”. p, $\overline{\text{ p }}$ and p mean p is $T$, $F$, and $U$, respectively.

• Programs 1 and 2 contain only negative cycles. All three of Founded, WFS, and Fitting agree. All three of Constraint, SMS, and Supported agree.

• Programs 3 and 4 contain only positive cycles. Founded for certain agrees with WFS; Founded for uncertain agrees with Fitting. Constraint for certain agrees with SMS; Constraint for uncertain agrees with Supported.

• Programs 5 and 6 contain no cycles. Founded for certain agrees with WFS and Fitting; Founded for uncertain has more undefined. Constraint for certain agrees with SMS and Supported; Constraint for uncertain has more models.

• Programs 7 and 8 contain both negative and positive cycles. For program 7 where and q are disjunctive, all three of Founded, WFS, and Fitting agree; Constraint and Supported agree, but SMS has no model. For program 8 where and q are conjunctive, Founded and Fitting agree, but WFS has q being $F$; all three of Constraint, SMS, and Supported agree.

For all 8 programs, with default complete but not closed predicates, we have the following:

• If all predicates are the default certain or uncertain, then Founded agrees with WFS, and Constraint agrees with SMS, with one exception for each:

  • (1) Program 7 concludes q whether q is $F$ or $T$, so SMS having no model is an extreme outlier among all 6 semantics and is not consistent with common sense.

  • (2) Program 8 concludes q if q is $F$ and $T$, so Founded semantics with q being $U$ is imprecise, but Constraint has q being $F$. WFS has q being $F$ because it uses $F$ for ignorance.

• If predicates not in any conclusion are certain (not shown in Table 2 but only needed for q in programs 5 and 6), and other predicates are uncertain, then Founded equals Fitting, and Constraint equals Supported, as captured in Theorems 7 and 11, respectively.

• If all predicates are uncertain, then Founded has all values being $U$, capturing the well-known unclear situations in all these programs, and Constraint gives all different models except for programs 2 and 5, and programs 4 and 6, which are pair-wise equivalent under completion, capturing exactly the differences among all these programs.

Finally, if all predicates in these programs are not complete, then Founded and Constraint are the same as in Table 2 except that Constraint for uncertain becomes equivalent to truth values in first-order logic: programs 1 and 8 have an additional model, {q}, program 6 has an additional model, {$\overline{\text{ p }}$, q}, and programs 2 and 5 have an additional model, {p,q}.