Skip to main content
SpringerLink
Log in

Guarded Quantification in Least Fixed Point Logic

  • Published:
Journal of Logic, Language and Information Aims and scope Submit manuscript

Abstract

We develop a variant of Least Fixed Point logic based on First Orderlogic with a relaxed version of guarded quantification. We develop aGame Theoretic Semantics of this logic, and find that under reasonableconditions, guarding quantification does not reduce the expressibilityof Least Fixed Point logic. But we also find that the guarded version ofa least fixed point algorithm may have a greater time complexity thanthe unguarded version, by a linear factor.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  • Abadi, M., Lamport, L., and Wolper, P., 1989, “Realizable and unrealizable specifications of reactive systems, ” pp. 1-17 in Proceedings of 16th ICALP, Stresa, Italy, G. Ausiello et al., eds., Berlin: Springer-Verlag.

    Google Scholar 

  • Abiteboul, S., Hull, R., and Vianu, V., 1995, Foundations of Databases, Reading, MA: Addison-Wesley.

    Google Scholar 

  • Aczel, P., 1975, “Quantifiers, games and inductive definitions, ” pp. 1-14 in Proceedings of the 3rd Scandinavian Logic Symposium, S. Kanger, ed., Amsterdam: North-Holland.

    Google Scholar 

  • Aho, A. and Ullman, J., 1979, “Universality of data retrieval languages, ” pp. 110-117 in Proceedings of the 6th ACM Symposium on Principles of Programming Languages, Association for Computing Machinery.

  • Andréka, H., van Benthem, J., and Németi, I., 1996, “Modal Languages and Bounded Fragments of Predicate Logic, ” ILLC Research Repport and Technical Notes Series.

  • Back, R.-J. and von Wright, J., 1998, Refinement Calculus: A Systematics Introduction, Berlin: Springer-Verlag.

    Google Scholar 

  • Barwise, J., 1977, “On Moschovakis Closure Ordinals, ” Journal of Symbolic Logic 42, 292-296.

    Google Scholar 

  • Barwise, J. and Moss, L., 1996, Vicious Circles: On the Mathematics of Non-Wellfounded Phenomena, Stanford, CA: CSLI.

    Google Scholar 

  • Berlekamp, E.R., Conway, J.H., and Guy, R.K., 2001, Winning Ways for your Mathematical Plays, London, New York: A.K. Peters.

    Google Scholar 

  • Blass, A. and Gurevich, Y., 1987, “Existential fixed-point logic, ” pp. 20-36 in Computation Theory and Logic, E. Börger, ed., Berlin: Springer-Verlag.

    Google Scholar 

  • Chandra, A. and Harel, D., 1982, “Structure and complexity of relational queries, ” Journal of Computer and System Sciences 25, 99-128.

    Google Scholar 

  • Clark, K., 1978, “Negation as Failure, ” pp. 293-322 in Logic and Databases, H. Gallaire and J. Minke, eds., New York: Plenum Press.

    Google Scholar 

  • Codd, E. F., 1970, “A relational model of data for larged shared data banks, ” Communications of the ACM 13, 377-387.

    Google Scholar 

  • Compton, K., 1983, “Some useful preservation theorems, ” Journal of Symbolic Logic 48, 427-440.

    Google Scholar 

  • Conway, J.H., 2001, On Numbers and Games, London, New York: A.K. Peters.

    Google Scholar 

  • Dahlhaus, E., 1987, “Skolem normal forms concerning the least fixed point, ” pp. 101-106 in Computation Theory and Logic, E. Börger, ed., Berlin: Springer-Verlag.

    Google Scholar 

  • Date, C.J., 1990, An Introduction to Database Systems, 5th edition, Reading, MA: Addison-Wesley.

    Google Scholar 

  • Ebbinghaus, H.-D. and Flum, J., 1995, Finite Model Theory, Berlin: Springer-Verlag.

    Google Scholar 

  • Ehrenfeucht, A., 1961, “An application of games to the completeness problem for formalized theories, ” Fundamenta Mathematicae 49, 129-141.

    Google Scholar 

  • Fagin, R., 1974, “Generalized first-order spectra and polynomial time recognizable sets, ” pp. 43-73 in Complexity of Computations, R. Karp, ed., SIAM-AMS Proceedings, Vol. 7, Philadelphia, PA: SIAM.

    Google Scholar 

  • Fagin, R., Halpern, J., Moses, Y., and Vardi, M., 1995, Reasoning about Knowledge, Cambridge, MA: MIT Press.

    Google Scholar 

  • Gale, D. and Stewart, F.M., 1953, “Infinite games with perfect information, ” Annals of Mathematics Studies 28, 245-266.

    Google Scholar 

  • Grädel, E., 1992, “On transitive closure logic, ” pp. 149-163 in '91), Berlin: Springer-Verlag.

    Google Scholar 

  • Grädel, E. and McColm, G., 1996, “Hierarchies in transitive closure logic, stratified datalog and infinitary logic, ” Annals of Pure and Applied Logic 77, 169-199.

    Google Scholar 

  • Grädel, E. and Wakiewicz, I., 1999, “Guarded fixed point logic, ” pp. 45-54 in Proceedings 14th IEEE Symposium on Logic in Computer Science, New York: IEEE.

    Google Scholar 

  • Grohe, M., 1996, “Arity hierarchies, ” Annals of Pure and Applied Logic 82, 103-163.

    Google Scholar 

  • Guy, R.K., ed., 1991, Combinatorial Games, Providence, RI: American Mathematical Society.

    Google Scholar 

  • Harel, D. and Kozen, D., 1984, “A programming language for the inductive sets, and applications, ” Information and Control 63, 118-139.

    Google Scholar 

  • Hesselink, W.H., 1994, “Nondeterminism and recursion via games and stacks, ” Theoretical Computer Science 124, 273-295.

    Google Scholar 

  • Hilpenen, R., 1982, “On C. S. Peirce's theory of the proposition: Peirce as a precursor of gametheoretic semantics, ” The Monist 62, 182-189.

    Google Scholar 

  • Hintikka, J., 1972, Language Games and Information, Oxford: Clarendon.

    Google Scholar 

  • Hintikka, J. and Kulas, J., 1983, The Game of Language: Studies in Game-Theoretical Semantics and its Applications, Dordrecht: Reidel.

    Google Scholar 

  • Hintikka, J. and Sandu, G., 1997, “Game-theoretic semantics, ” pp. 361-410 in Handbook of Logic and Language, J. van Benthem and A. ter Meulen, eds., Cambridge, MA: MIT Press and Amsterdam: North-Holland.

    Google Scholar 

  • Hirsch, R. and Hodkinson, I., 2002, Relation Algebras by Games, Amsterdam: Elsevier.

    Google Scholar 

  • Immerman, N., 1981, “Number of quantifiers is better than number of tape cells, ” Journal of Computer and System Sciences 22, 384-406.

    Google Scholar 

  • Immerman, N., 1982, “Upper and lower bounds for first order expressibility, ” Journal of Computer and System Sciences 25, 76-98.

    Google Scholar 

  • Immerman, N., 1986, “Relational queries computable in polynomial time, ” Information and Control 68, 86-104.

    Google Scholar 

  • Immerman, N., 1987, “Languages that capture complexity classes, ” SIAM Journal of Computing 16, 760-778.

    Google Scholar 

  • Immerman, N., 1999, Descriptive Complexity, Berlin: Springer-Verlag.

    Google Scholar 

  • Kanellakis, P., 1991, “Elements of relational database theory, ” pp. 1074-1156 in Handbook of Theoretical Computer Science, J. van Leeuwen, ed., Amsterdam: Elsevier.

    Google Scholar 

  • Kolaitis, P., 1985, “Game quantification, ” pp. 365-421 in Model-Theoretic Logics, J. Barwise and S. Feferman, eds., Berlin: Springer-Verlag.

    Google Scholar 

  • Kolaitis, P., 1991, “The expressive power of stratified logic programs, ” Information and Computation 90, 50-66.

    Google Scholar 

  • McColm, G., 1989, “Some restrictions on simple fixed points of the integers, ” Journal of Symbolic Logic 54, 1324-1345.

    Google Scholar 

  • McColm, G., 1990a, “Parametrization over inductive relations of a bounded number of variables, ” Annals of Pure and Applied Logic 48, 103-134.

    Google Scholar 

  • McColm, G., 1990b, “When is arithmetic possible?, ” Annals of Pure and Applied Logic 50, 29-51.

    Google Scholar 

  • McColm, G., 1995a, “Pebble games and subroutines in least fixed point logic, ” Information and Computation 122, 201-220.

    Google Scholar 

  • McColm, G., 1995b, “Dimension versus number of variables, and connectivity, too, ” Mathematical Logic Quarterly 41, 111-134.

    Google Scholar 

  • Milner, R., 1999, Communicating and Mobile Systems: The π-Calculus, Cambridge: Cambridge University Press.

    Google Scholar 

  • Moschovakis, Y., 1972, “The game quantifier, ” Proceedings of the American Mathematical Society 31, 245-250.

    Google Scholar 

  • Moschovakis, Y., 1974, Elementary Induction on Abstract Structures, Amsterdam: North-Holland.

    Google Scholar 

  • Moschovakis, Y., 1980, Descriptive Set Theory, Amsterdam: North-Holland.

    Google Scholar 

  • Moschovakis, Y., 1983, “Abstract recursion as a foundation for the theory of algorithms, ” pp. 289-364 in Computation and Proof Theory, M.M. Richter et al., eds., Berlin: Springer-Verlag.

    Google Scholar 

  • Moschovakis, Y., 1991, “A model of concurrency with fair merge and full recursion, ” Information and Computation 93, 114-171.

    Google Scholar 

  • Nowakowski, R.J., ed., 2002, More Games of No Chance, Cambridge: Cambridge University Press.

    Google Scholar 

  • Parikh, R., 1985, “The logic of games and its applications, ” Annals of Discrete Mathematics 24, 111-140.

    Google Scholar 

  • Plotkin, G., 1981, A Structural Approach to Operational Semantics, Aarhus: Computer Science Department, Aarhus University.

    Google Scholar 

  • Rogers, Jr., H., 1967, Theory of Recursive Functions and Effective Computability, New York: McGraw-Hill.

    Google Scholar 

  • Ullman, J.D., 1988, 1989, Principles of Database Systems and Knowledge Base Systems I and II, Rockville, MD: Computer Science Press.

    Google Scholar 

  • van Benthem, J.F.A.K., 1996, Exploring Logical Dynamics, Stanford, CA: CSLI.

    Google Scholar 

  • van Benthem, J.F.A.K., 2002, “Extensive games as process models, ” Journal of Logic, Language and Information 11, 289-313.

    Google Scholar 

  • Vardi, M., 1982, “Complexity of relational database systems, ” pp. 137-146 in Proceedings 14th ACM Symposium on the Theory of Computing, Association for Computing Machinery (ACM).

Download references

Author information

Authors and Affiliations

  1. Department of Mathematics, University of South Florida, Tampa, FL, 33620, U.S.A.

    Gregory McColm

Authors
  1. Gregory McColm
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

McColm, G. Guarded Quantification in Least Fixed Point Logic. Journal of Logic, Language and Information 13, 61–110 (2004). https://doi.org/10.1023/A:1026107209351

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1023/A:1026107209351

Search

Navigation