ACM DL

Computational Logic (TOCL)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Computational Logic (TOCL), Volume 6 Issue 2, April 2005

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...