Literal Projection and Circumscription

From International Center for Computational Logic

Toggle side column

Literal Projection and Circumscription

Christoph WernhardChristoph Wernhard
Literal Projection and Circumscription


Christoph Wernhard
Literal Projection and Circumscription
In Nicolas Peltier and Viorica Sofronie-Stokkermans, eds., Proceedings of the 7th International Workshop on First-Order Theorem Proving, FTP'09, volume 556 of CEUR Workshop Proceedings, 2010
  • KurzfassungAbstract
    We develop a formal framework intended as a preliminary step for a single knowledge representation system that provides different representation techniques in a unified way. In particular we consider first-order logic extended by techniques for second-order quantifier elimination and non-monotonic reasoning. In this paper two independent results are developed. The background for the first result is literal projection, a generalization of second-order quantification which permits, so to speak, to quantify upon an arbitrary sets of ground literals, instead of just (all ground literals with) a given predicate symbol. We introduce an operator raise that is only slightly different from literal projection and can be used to define a generalization of predicate circumscription in a straightforward and compact way. We call this variant of circumscription scope-determined. Some properties of raise and scope-determined circumscription, also in combination with literal projection, are then shown. A previously known characterization of consequences of circumscribed formulas in terms of literal projection is generalized from propositional to first-order logic and proven on the basis of the introduced concepts. The second result developed in this paper is a characterization stable models in terms of circumscription. Unlike traditional characterizations, it does not recur onto syntactic notions like reduct and fixed-point construction. It essentially renders a recently proposed ``circumscription-like characterization in a compact way, without involvement of a non-classically interpreted connective.
  • Bemerkung: Note: (Extended version: http://cs.christophwernhard.com/papers/projection-circumscription.pdf)
  • Forschungsgruppe:Research Group: Wissensverarbeitung
@inproceedings{W2010,
  author    = {Christoph Wernhard},
  title     = {Literal Projection and Circumscription},
  editor    = {Nicolas Peltier and Viorica Sofronie-Stokkermans},
  booktitle = {Proceedings of the 7th International Workshop on First-Order
               Theorem Proving, {FTP'09}},
  series    = {CEUR Workshop Proceedings},
  volume    = {556},
  year      = {2010}
}