Nachum Dershowitz Explained
Nachum Dershowitz |
Fields: | Term rewriting |
Thesis Title: | The Evolution of Programs |
Thesis1 Url: | and |
Thesis2 Url: | )--> |
Thesis Year: | 1979 |
Doctoral Advisor: | Zohar Manna |
Known For: | Dershowitz–Manna ordering |
Awards: | Herbrand Award 2011[1] |
Website: | http://www.cs.tau.ac.il/~nachumd/Homepage.html |
Spouses: | )--> |
Partners: | )--> |
Nachum Dershowitz is an Israeli computer scientist, known e.g. for the Dershowitz–Manna ordering and the multiset path ordering used to prove termination of term rewrite systems.
Education and career
He obtained his B.Sc., summa cum laude, in 1974 in computer science and applied mathematics from Bar-Ilan University, and his Ph.D. in 1979 in Applied Mathematics from the Weizmann Institute of Science.From 1978, he worked at the Department of Computer Science of the University of Illinois at Urbana-Champaign, and was hired as a full professor of the Tel Aviv University (School of Computer Science) in 1998. He was a guest researcher at Weizmann Institute, INRIA, ENS Cachan, Microsoft Research, and the universities of Stanford, Paris, Jerusalem, Chicago, and Beijing.[2] He received the Herbrand Award for Distinguished Contributions to Automatic Reasoning in 2011.
He has co-authored the standard text on calendar algorithms, Calendrical Calculations, with Edward Reingold.[3] [4] [5] [6] An implementation of the algorithm in Common Lisp is in the public domain, and is also distributed with the book.
See also
Selected publications
- Book: Nachum Dershowitz . Zohar Manna . amp . The Evolution of Programs: A System for Automatic Program Modification . Proc. POPL . 144–154 . http://www.cs.tau.ac.il/~nachum/papers/Modification.pdf . 1977 . POPL .
- . Proving Termination with Multiset Orderings . . 22 . 8 . 465–476 . Aug 1979 . 10.1145/359138.359142. 10.1.1.1013.432 . 17906810 .
- Book: N. Dershowitz . Orderings for Term Rewriting Systems . Proc. 20th Symposium on Foundations of Computer Science (FOCS) . 123–131 . Oct 1979 . FOCS .
- Book: N. Dershowitz . Termination of linear rewriting systems: Preliminary version . Shimon Even . Oded Kariv . Proc. ICALP . Springer . . 115 . 448–458 . 1981 . ICALP .
- N. Dershowitz . Orderings for Term-Rewriting Systems . . 17 . 3 . 279–301 . 1982 . 10.1016/0304-3975(82)90026-3. 6070052 .
- Book: Dershowitz, N. . Termination . 180–224 . http://www.cs.tau.ac.il/~nachum/papers/LNCS/Termination.pdf . 1985 . Jean-Pierre Jouannaud . Jean-Pierre Jouannaud . Rewriting Techniques and Applications, 1st Int. Conf., RTA-85 . LNCS . 202 . Springer. Rewriting Techniques and Applications .
- Book: Bachmair, L. and Dershowitz, N. and Hsiang, J. . Orderings for Equational Proofs . Proc. IEEE Symposium on Logic in Computer Science (LICS). Cambridge/MA . 346–357 . Jun 1986 . LICS (symposium) .
- Book: Bachmair, L. . Dershowitz, N. . amp . Completion for Rewriting Modulo a Congruence . 192–203 . 1987 . Lescanne, Pierre . Rewriting Techniques and Applications, 2nd Int. Conf., RTA-87 . LNCS . 256 . Springer.
- Nachum Dershowitz . Termination of Rewriting . . 3 . 1–2 . 69–116 . 1987 . 10.1016/s0747-7171(87)80022-6. free .
- Book: N. Dershowitz . M. Okada . amp . Proof-Theoretic Techniques for Term Rewriting Theory . Proc. 3rd IEEE Symp. on Logic in Computer Science . 104–111 . 1988 .
- Book: N. Dershowitz . G. Sivakumar . amp . Solving Goals in Equational Languages . Proc. 1st Int. Workshop on Conditional Term Rewriting Systems . Springer . LNCS . 308 . 45–55 . 1988 .
- Book: 1989 . Dershowitz, Nachum . Rewriting Techniques and Applications, 3rd Int. Conf., RTA-89 . LNCS . 355 . Springer .
- Book: N. Dershowitz . J.-P. Jouannaud . amp . Rewrite Systems . 243–320 . Jan van Leeuwen . Jan van Leeuwen . Formal Models and Semantics . Elsevier . Handbook of Theoretical Computer Science . B . 1990.
- N. Dershowitz . J.-P. Jouannaud . amp . Notations for Rewriting . 1990 .
- Book: . Open Problems in Rewriting . 445–456 . 1991 . Ronald V. Book . Ronald V. Book . Rewriting Techniques and Applications, 4th Int. Conf., RTA-91 . LNCS . 488 . Springer.
- Book: Dershowitz, N. and Jouannaud, J.-P. and Klop, J.W. . More Problems in Rewriting . 468–487 . 1993 . Kirchner, Claude . Rewriting Techniques and Applications, 5th Int. Conf., RTA-93 . LNCS . 690 . Springer.
- Book: Nachum Dershowitz . Trees, Ordinals and Termination . Proc. CAAP/TAPSOFT . Springer . LNCS . 668 . 243–250 . Apr 1993 .
- Book: Dershowitz, N. . Hoot, C. . amp . Topics in Termination . 198–212 . 1993 . Kirchner, Claude . Rewriting Techniques and Applications, 5th Int. Conf., RTA-93 . LNCS . 690 . Springer.
- Book: Dershowitz, N. . Innocuous Constructor-Sharing Combinations . 202–216 . 1997 . Comon, Hubert . Rewriting Techniques and Applications, 8th Int. Conf., RTA-97 . LNCS . 1232 . Springer.
- Dershowitz, Nachum and Reingold, Edward M., Calendrical Calculations, Cambridge University Press,, 1997
- Book: Dershowitz, N. . Treinen, R. . amp . An On-line Problem Database . 332–342 . 1998 . Tobias Nipkow . Tobias Nipkow . Rewriting Techniques and Applications, 9th Int. Conf., RTA-98 . LNCS . 1379 . Springer.
- Book: Dershowitz, N. . Mitra, S. . amp . Jeopardy . 16–29 . 1999 . Narendran, Paliath . Rusinowitch, Michaël . Rewriting Techniques and Applications, 10th Int. Conf., RTA-99 . LNCS . 1631 . Springer.
- Book: . Rewriting (Chapter 9) . 535–610 . Handbook of Automated Reasoning . Alan Robinson . John Alan Robinson . Andrei Voronkov . Andrei Voronkov . MIT Press + Elsevier . 2001. Handbook of Automated Reasoning .
- Book: Dershowitz, N. . Term Rewriting and Applications . 376–393 . 2005 . Giesl, J. . Term Rewriting and Applications, 16th Int. Conf., RTA-05 . LNCS . 3467 . 978-3-540-25596-3 . Springer .
- Book: Dershowitz, N. . Castedo Ellerman, E. . amp . Leanest Quasi-orderings . 32–45 . 2005 . Giesl, J. . Term Rewriting and Applications, 16th Int. Conf., RTA-05 . LNCS . 3467 . 978-3-540-25596-3 . Springer .
- Dershowitz, Nachum 2005. The Four Sons of Penrose, in Proceedings of the Eleventh Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR; Jamaica), G. Sutcliffe and A. Voronkov, eds., Lecture Notes in Computer Science, vol. 3835, Springer-Verlag, Berlin, pp. 125–138.
External links
Notes and References
- http://www.cs.miami.edu/~geoff/Conferences/CADE/Data/HerbrandAwardSlidesDershowitz.pdf Herbrand award address
- http://www.ae-info.org/ae/User/Dershowitz_Nachum/CV Vita
- Edward M. Reingold and Nachum Dershowitz. Calendrical Calculations. Cambridge University Press; 4th edition (April 2018).
- Review of Calendrical Calculations by E. G. Richards (1998), Nature 391: 33–34, .
- Review of Calendrical Calculations by Robert Poole (1999), The British Journal for the History of Science 32 (1): 116–118, .
- Review of Calendrical Calculations by N. M. Swerdlow (1998), IEEE Annals of the History of Computing 20 (3): 78, .