Advertisement

Abstract

The impossibility of semantically complete deductive calculi for logics for imperative programs has led to the study of two alternative approaches to completeness: “local” semantic completeness on the one hand (Cook’s relative completeness, Harel’s Arithmetical completeness), and completeness with respect to other forms of reasoning about programs, on the other. However, local semantic completeness is problematic on several counts, whereas proof theoretic completeness results often involve ad hoc ingredients, such as formal theories for the natural numbers.

The notion of inductive completeness, introduced in [18], provides a generic proof theoretic framework which dispenses with extraneous ingredients, and yields local semantic completeness as a corollary.

Here we prove that (first-order) Dynamic Logic for regular programs (DL) is inductively complete: a DL-formula ϕ is provable in (the first-order variant of) Pratt-Segerberg deductive calculus DL iff ϕ, is provable in first-order logic from the inductive theory for program semantics. The method can be adapted to yield the schematic relative completeness of DL: if \(\mathcal{S}\) is an expressive structure, then every formula true in \(\mathcal{S}\) is provable from the axiom-schemas that are valid in \(\mathcal{S}\). Harel’s Completeness Theorem falls out then as a special case.

Keywords

Dynamic logic inductive completeness relative completeness arithmetical completeness 

References

  1. 1.
    Andreka, H., Nemeti, I., Sain, I.: A complete logic for reasoning about programs via nonstandard model theory, Parts I and II. Theoretical Computer Science 17, 193–212, 259–278 (1982)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Beckert, B., Platzer, A.: Dynamic logic with non-rigid functions. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS, vol. 4130, pp. 266–280. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  3. 3.
    Blass, A., Gurevich, Y.: The underlying logic of Hoare logic. Current Trends in Theoretical Computer Science, 409–436 (2001)Google Scholar
  4. 4.
    Clarke, E.: Programming language constructs for which it is impossible to obtain good Hoare-like axioms. J. ACM 26, 129–147 (1979)CrossRefzbMATHGoogle Scholar
  5. 5.
    Cook, S.A.: Soundness and completeness of an axiom system for program verification. SIAM J. Computing 7(1), 70–90 (1978)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Csirmaz, L.: Programs and program verification in a general setting. Theoretical Computer Science 16, 199–210 (1981)CrossRefzbMATHGoogle Scholar
  7. 7.
    Feferman, S.: Formal theories for transfinite iterations of generalized inductive definitions and some subsystems of analysis. In: Intuitionism and Proof Theory, pp. 303–326. North-Holland, Amsterdam (1970)Google Scholar
  8. 8.
    Feferman, S., Sieg, W.: Iterated inductive definitions and subsystems of analysis. In: Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoreitc Studies. LNM, vol. 897, pp. 16–77. Springer, Berlin (1981)CrossRefGoogle Scholar
  9. 9.
    Harel, D., Meyer, A., Pratt, V.: Computability and completeness in logics of programs. In: Proceedings of the ninth symposium on the Theory of Computing, Providence, pp. 261–268. ACM, New York (1977)Google Scholar
  10. 10.
    Harel, D.: First-Order Dynamic Logic. LNCS, vol. 68. Springer, Heidelberg (1979)zbMATHGoogle Scholar
  11. 11.
    Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)zbMATHGoogle Scholar
  12. 12.
    Honsell, F., Miculan, M.: A natural deduction approach to dynamic logics. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol. 1158, pp. 165–182. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  13. 13.
    Kreisel, G.: Generalized inductive definitions. Reports for the seminar on foundations of analysis, Stanford, vol. 1 §3 (1963)Google Scholar
  14. 14.
    Kreisel, G.: Mathematical logic. In: Saaty, T. (ed.) Lectures on Modern Mathematics, vol. III, pp. 95–195. John Wiley, New York (1965)Google Scholar
  15. 15.
    Leivant, D.: Logical and mathematical reasoning about imperative programs. In: Conference Record of the Twelfth Annual Symposium on Principles of Programming Languages, pp. 132–140. ACM, New York (1985)Google Scholar
  16. 16.
    Leivant, D.: Partial correctness assertions provable in dynamic logics. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 304–317. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  17. 17.
    Leivant, D.: Matching explicit and modal reasoning about programs: A proof theoretic delineation of dynamic logic. In: Twenty-first Symposium on Logic in Computer Science (LiCS 2006), Washington, pp. 157–166. IEEE Computer Society Press, Los Alamitos (2006)CrossRefGoogle Scholar
  18. 18.
    Leivant, D.: Inductive completeness of logics of programs. In: Proceedings of the Workshop on Logical Frameworks and Meta-Languages (to appear, 2008)Google Scholar
  19. 19.
    Martin-Löf, P.: Hauptsatz for the intuitionistic theory of iterated inductive definitions. In: Fenstad, J.E. (ed.) Proceedings of the Second Scandinavian Logic Symposium, pp. 63–92. North-Holland, Amsterdam (1971)Google Scholar
  20. 20.
    Mirkowska, G.: On formalized systems of algorithmic logic. Bull. Acad. Polon. Sci. 19, 421–428 (1971)MathSciNetzbMATHGoogle Scholar
  21. 21.
    Nishimura, H.: Arithmetical completeness in first-order dynamic logic for concurrent programs. Publ. Res. Inst. Math. Sci. 17, 297–309 (1981)MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Pratt, V.: Semantical considerations on Floyd-Hoare logic. In: Proceedings of the seventeenth symposium on Foundations of Computer Science, Washington, pp. 109–121. IEEE Computer Society, Los Alamitos (1976)Google Scholar
  23. 23.
    Sain, I.: An elementary proof for some semantic characterizations of nondeterministic Floyd-Hoare logic. Notre Dame Journal of Formal Logic 30, 563–573 (1989)MathSciNetCrossRefzbMATHGoogle Scholar
  24. 24.
    Segerberg, K.: A completeness theorem in the modal logic of programs (preliminary report). Notics of the American Mathematical Society 24(6), A–552 (1977)Google Scholar
  25. 25.
    Szalas, A.: On strictly arithmetical completeness in logics of programs. Theoretical Computer Science 79(2), 341–355 (1991)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Daniel Leivant
    • 1
  1. 1.Computer Science DepartmentIndiana UniversityBloomingtonUSA

Personalised recommendations