Search ACM DL

Search Issue

enter search term and/or author name

**Induction from answer sets in nonmonotonic logic programs**

Chiaki Sakama

Pages: 203-231

DOI: 10.1145/1055686.1055687

*Inductive logic programming* (ILP) realizes inductive machine learning in computational logic. However, the present ILP mostly handles classical clausal programs, especially Horn logic programs, and has limited applications to learning...

**Complexity of propositional nested circumscription and nested abnormality theories**

Marco Cadoli, Thomas Eiter, Georg Gottlob

Pages: 232-272

DOI: 10.1145/1055686.1055688

Circumscription has been recognized as an important principle for knowledge representation and common-sense reasoning. The need for a circumscriptive formalism that allows for simple yet elegant modular problem representation has led Lifschitz (AIJ,...

**From linear time to branching time**

Orna Kupferman, Moshe Y. Vardi

Pages: 273-294

DOI: 10.1145/1055686.1055689

Model checking is a method for the verification of systems with respect to their specifications. Symbolic model-checking, which enables the verification of large systems, proceeds by calculating fixed-point expressions over the system's set of...

**Comparisons and computation of well-founded semantics for disjunctive logic programs**

Kewen Wang, Lizhu Zhou

Pages: 295-327

DOI: 10.1145/1055686.1055690

Much work has been done on extending the well-founded semantics to general disjunctive logic programs and various approaches have been proposed. However, these semantics are different from each other and no consensus is reached about which semantics...

**Equivalences among aggregate queries with negation**

Sara Cohen, Yehoshua Sagiv, Werner Nutt

Pages: 328-360

DOI: 10.1145/1055686.1055691

Query equivalence is investigated for disjunctive aggregate queries with negated subgoals, constants and comparisons. A full characterization of equivalence is given for the aggregation functions *count, max, sum, prod, top2* and *parity*....

**Knuth--bendix constraint solving is NP-complete**

Konstantin Korovin, Andrei Voronkov

Pages: 361-388

DOI: 10.1145/1055686.1055692

We show the NP-completeness of the existential theory of term algebras with the Knuth--Bendix order by giving a nondeterministic polynomial-time algorithm for solving Knuth--Bendix ordering constraints.

**Reasoning about evolving nonmonotonic knowledge bases**

Thomas Eiter, Michael Fink, Giuliana Sabbatini, Hans Tompits

Pages: 389-440

DOI: 10.1145/1055686.1055693

Recently, several approaches to updating knowledge bases modeled as extended logic programs have been introduced, ranging from basic methods to incorporate (sequences of) sets of rules into a logic program, to more elaborate methods which use an...

**Minimum model semantics for logic programs with negation-as-failure**

Panos Rondogiannis, William W. Wadge

Pages: 441-467

DOI: 10.1145/1055686.1055694

We give a purely model-theoretic characterization of the semantics of logic programs with negation-as-failure allowed in clause bodies. In our semantics, the meaning of a program is, as in the classical case, the unique *minimum* model in a...

**An elementary fragment of second-order lambda calculus**

Klaus Aehlig, Jan Johannsen

Pages: 468-480

DOI: 10.1145/1055686.1055695

A fragment of second-order lambda calculus (System *F*) is defined that characterizes the elementary recursive functions. Type quantification is restricted to be noninterleaved and stratified, that is, the types are assigned levels, and a...