Literal Projection and Circumscription

Christoph WernhardChristoph Wernhard

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

Details
Bibtex

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: WissensverarbeitungKnowledge Representation and Reasoning

@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}
}