×

zbMATH — the first resource for mathematics

A near-optimal method for reasoning about action. (English) Zbl 0424.03010

MSC:
03B45 Modal logic (including the logic of norms)
68Q60 Specification and verification (program logics, model checking, etc.)
03D15 Complexity of computation (including implicit computational complexity)
68Q65 Abstract data types; algebraic specification
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Basu, S.K.; Yeh, R.T., Strong verification of programs, IEEE trans. software engrg., SE-1, No. 3, 339-345, (1975)
[2] Beth, E.W., The foundations of mathematics, (1959), North-Holland Amsterdam · Zbl 0154.00203
[3] Chandra, A.E.; Stockmeyer, L.J., Alternation, (), 98-108
[4] Cook, S.A., Characterization of pushdown machines in terms of time bounded computers, J. assoc. comput. Mach., 18, 4-18, (1971) · Zbl 0222.02035
[5] Dijkstra, E.W., A discipline of programming, (1976), Prentice-Hall Englewood Cliffs, N. J · Zbl 0286.00013
[6] Fischer, M.J.; Ladner, R.E., Propositional modal logic of programs, (), 286-294, Boulder, Colo.
[7] Fischer, M.J.; Ladner, R.E., Propositional dynamic logic of regular programs, manuscript, (1977), Dept. of Computor Science, University of Washington
[8] Gabbay, D., Axiomatizations of logics of programs, (November 1977), manuscript
[9] Gentzen, G.; Gentzen, G., Investigations into logical deduction, (), 39, 69-131, (1934-1935), English tr.
[10] Hintieica, K.J.J., Form and content in quantification theory, Acta philos. fenn., 8, 7-55, (1955)
[11] Hoare, C.A.R., An axiomatic basis for computer programming, Comm. ACM, 12, 576-580, (1969) · Zbl 0179.23105
[12] Jazayeri, M.; Ogden, W.F.; Rounds, W.C., The intrinsically exponential complexity problem for attribute grammars, Comm. ACM, 18, 697-706, (1975) · Zbl 0318.68051
[13] Kozen, D., On parallelism in Turing machines, (), 89-97
[14] Lewis, H., Complexity of solvable cases of the decision problem for the predicate calculus, ()
[15] Meyer, A.R., Equivalence of DL, DL + and ADL for regular programs with array assignments, ()
[16] Misra, J., Prospects and limitations of automatic assertion generation for loop programs, SIAM J. comput., 6, 718-729, (1977) · Zbl 0366.68003
[17] Parikh, R., A completeness result for PDL, () · Zbl 0188.02102
[18] Pratt, V.R., Semantical considerations on floyd-Hoare logic, (), 109-121
[19] Pratt, V.R., A practical decision method for propositional dynamic logic, (), 326-337, San Diego, Calif. · Zbl 1283.03066
[20] Pratt, V.R., Models of program logics, () · Zbl 0469.94017
[21] Segerberg, K., A completeness theorem in the modal logic of programs, preliminary report, Notices amer. math. soc., 24, A-552, (1977)
[22] Smullyan, R.M., First-order logic, (1968), Springer-Verlag Berlin · Zbl 0172.28901
[23] Smullyan, R.M., Trees and nest structures, J. symbolic logic, 31, 303-321, (1966) · Zbl 0149.00501
[24] Wegbreit, B., The synthesis of loop predicates, Comm. ACM, 17, 102-112, (1974) · Zbl 0273.68014
[25] Winklmann, K., Equivalence of DL and DL+ for regular programs, ()
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.