Zohar Manna
Amir Pnueli
ABSTRACT
This paper is concerned with the relationship between the convergence, correctness and equivalence of recursively defined functions and the satisfiability (or unsatisfiability) of certain first-order formulas.
- 1.Church, A. Introduction to Mathematical Logic. Volume 1, Princeton University Press, Princeton (1956).Google Scholar
- 2.Cooper, D. C. The equivalence of certain computations. The Computer Journal 9, 1 (1966), 45-52.Google ScholarCross Ref
- 3.Cooper, D. C. Program scheme equivalences and second order logic. Presented at Fourth Annual Machine Intelligence Workshop, University of Edinburgh (August 1968).Google Scholar
- 4.Floyd, R. W. Assigning Meaning to Programs. Proceedings of Symposia in Applied Mathematics, American Mathematical Society, Vol. 19 (1967), 19-32.Google ScholarCross Ref
- 5.Manna, Z. Termination of algorithms. Ph.D. Thesis, Computer Science Department, Carnegie-Mellon University (April 1968). Google ScholarDigital Library
- 6.Manna, Z. Formalization of properties of programs. Stnaford Artificial Intelligence Report, Memo No. AI-64 (July 1968).Google Scholar
- 7.Manna, Z., and Pnueli, A. The validity problem of the 91-function. Stanford Artificial Intelligence Report, Memo No. AI-68 (Aug. 1968).Google Scholar
- 8.McCarthy, J. Towards a Mathematical Science of Computation. Proc. ICIP Congress 62, North-Holland, Amsterdam (1962), 21-28.Google Scholar
- 9.McCarthy, J. A basis for a mathematical theory of computation. In Braffort,P., and Hirschberg, D. (Eds.), Computer Programming and Formal Systems. North-Holland, Amsterdam (1963).Google Scholar
- 10.Mendelson, E. Introduction to Mathematical Logic. D. Van Nostrand Company, Princeton (1964). Google ScholarDigital Library
Index Terms
- Formalization of properties of recursively defined functions
Recommendations
Shifted plateaued functions and their differential properties
AbstractA bent4 function is a Boolean function with a flat spectrum with respect to a certain unitary transform . It was shown previously that a Boolean function f in an even number of variables is bent4 if and only if f + σ is bent, where σ is a certain ...
Some general properties of modified bent functions through addition of indicator functions
AbstractProperties of a secondary bent function construction that adds the indicator of an affine subspace of arbitrary dimension to a given bent function in n variables are obtained. Some results regarding normal and weakly normal bent functions are ...
Generalized Plateaued Functions and Admissible (Plateaued) Functions
Plateaued functions are very important crypto- graphic functions due to their various desirable cryptographic characteristics. We point out that plateaued functions are more general than bent functions (that is, functions with maximum nonlinearity). Some ...
Comments