Logic Journal of IGPL Advance Access originally published online on September 26, 2007
Logic Journal of IGPL 2007 15(5-6):503-526; doi:10.1093/jigpal/jzm037
On Minimal Models
Departamento de Computação, Universidade Federal do Ceará, CP 12.166, Fortaleza-CE, Brasil, CEP 60455-760. E-mail: fran{at}lia.ufc.br
Departamento de Computaçãao, Universidade Federal do Ceará, CP 12.166, Fortaleza-CE, Brasil, CEP 60455-760. E-mail: ana{at}lia.ufc.br
We investigate some logics which use the concept of minimal models in their definition. Minimal objects are widely used in Logic and Computer Science. They are applied in the context of Inductive Definitions, Logic Programming and Artificial Intelligence. An example of logic which uses this concept is the MIN(FO) logic due to van Benthem [20]. He shows that MIN(FO) is equivalent to the Least Fixed Point logic (LFP) in expressive power. In [6], we extended MIN(FO) to the MIN Logic and proved it is equivalent to second-order logic in expressive power. Here, we exhibit a fragment of MIN, the MIN
logic, which is more expressive than LFP, less expressive than MIN and closed under boolean connectives and first-order quantification. In order to do this, in the Section 2, we prove that the Downward Löwenheim-Skolem Theorem holds for arbitrary countable sets of LFP-formulas by showing that every infinite structure has a countable LFP-substructure. The method may be used to generalize this theorem to any set of LFP-formulas. We also analyse the expressive power of the Nested Abnormality Theories (NATs) of Lifschitz, another formalism based on minimal models used in Artificial Intelligence, and we demonstrate that for each second-order theory
there is a NAT which is a conservative extension of
. We give a translation from second-order sentences into such NATs which is linear in the size of the sentence in prenex normal form. Finally, we establish a hierarchy of expressiveness of these logics that deal with the concept of minimal models.
Key Words: minimal models fixed points expressiveness.
Received for publication 13 September 2006.
This research is partially supported by CNPq and FUNCAP.
This research is partially supported by PADCT/CNPq, PRONEX/FUNCAP-CNPq, CNPq and FUNCAP.
References
- Aczel P. An Introduction to Inductive Definitions. In: Handbook of Mathematical Logic—Barwise J, ed. (1977) North-Holland: Amsterdam. 739–782.
- Cadoli M, Eiter T, Gottlob G. Complexity of propositional nested circumscription and nested abnormality theories. ACM Trans. Comput. Logic ((Apr. 2005)) 6(2):232–272.[CrossRef]
- Dawar A, Gurevich Y. Fixed-point Logics. Bulletin of Symbolic Logic (2002) 8(1):65–88.
- Ebbinghaus H-D, Flum J, Thomas W. (NY) New York, NY: Mathematical Logic. Springer-Verlag.
- Ebbinghaus H-D, Flum J. Finite Model Theory. (1995) Springer-Verlag.
- Ferreira Francicleber M, Martins Ana Teresa. The Predicate-Minimizing logic MIN. In: IBERAMIA/SBIA 2006 International Joint Conference, 2006. In: 2006. Ribeiro Preto. Lecture Notes in Artificial Intelligence: Proceedings of IBERAMIA/SBIA 2006: Berlin : Springer-Verlag. 1–10.
- Caicedo X, Montenegro C. On the (Infinite) Model Theory of Fixed-Point Logics, in Models, algebras and proofs. In: no 2003 in Lecture Notes in Pure and Applied Mathematics Series (1999) Marcel Dekker. 67–75.
- Grädel E. Guarded fixed point logics and the monadic theory of countable trees. Theoretical Computer Science (2002) 288(1):129–152.
- Hrbacek K, Jech T. . Introduction to Set Theory, 3rd. edition (1999) New York: Marcel Dekker.
- Kreutzer S. Pure and Applied Fixed-Point Logics. In: PhD Thesis (2002) Fakultät für Mathematik, Informatik und Naturwissenschaften der Rheinisch-Westflischen Technischen Hochschule Aachen.
- Kreutzer S. Expressive Equivalence of Least and Inflationary Fixed-Point Logic. In: Annals of Pure and Applied Logic, LICS 2002 Selected Paper Issue (2004) Volume 130(Issues 1–3):61–78.
- Libkin L. Elements of Finite Model Theory (2004) Berlin: Springer.
- Gabbay DM, Hogger CJ, Robinson JA. Circumscription. Handbook of Logic in Artificial Intelligence and Logic Programming-Nonmonotonic Reasoning and Uncertain Reasoning (Volume 3). (1994) Oxford: Clarendon Press. 297–352.
- Lifschitz V. Nested Abnormality Theories. Artif. Intell. (1995) 74(2):351–365.
- McCarthy J. Circumscription – A Form of Non-Monotonic Reasoning. Artif. Intell. (1980) 13(1–2):27–39.
- McCarthy J. Applications of circumscription to formalizing common-sense knowledge. Artif. Intell. (1986) 28(1).
- Moschovakis YN. Elementary induction on abstract structures. (1974) North Holland.
- Scott D. Domains for Denotational Semantics. (1982) LNCS 140: Proc. 9th ICALP. Berlin: Springer. 577–613.
- Tarski A. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics (1955) 5:285–309.
- van Benthem J. Minimal Predicates, Fixed-Points, and Definability. J. Symbolic Logic (2005) 70(3):696–712.
| ||||||||||||||||||||||||||||||||||||||||||||||||||