Nachum Dershowitz

Nachum Dershowitz is an Israeli computer scientist, known e.g. for the Dershowitz–Manna ordering used to prove termination of term rewrite systems.

He obtained his B.Sc. summa cum laude in 1974 in Computer Science–Applied Mathematics from Bar-Ilan University, and his Ph.D. in 1979 in Applied Mathematics from the Weizmann Institute of Science. Since 1978, he worked at Department of Computer Science of the University of Illinois at Urbana-Champaign, until he became 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]

Nachum Dershowitz
Known forDershowitz–Manna ordering
AwardsHerbrand Award 2011[1]
Scientific career
FieldsTerm rewriting
ThesisThe Evolution of Programs (1979)
Doctoral advisorZohar Manna
Websitehttp://www.cs.tau.ac.il/~nachumd/Homepage.html

Selected publications

  • Nachum Dershowitz & Zohar Manna (1977). "The Evolution of Programs: A System for Automatic Program Modification" (PDF). Proc. POPL. pp. 144–154.
  • Nachum Dershowitz and Zohar Manna (Aug 1979). "Proving Termination with Multiset Orderings" (PDF). Communications of the ACM. 22 (8): 465–476. CiteSeerX 10.1.1.1013.432. doi:10.1145/359138.359142.
  • N. Dershowitz (Oct 1979). "Orderings for Term Rewriting Systems". Proc. 20th Symposium on Foundations of Computer Science (FOCS). pp. 123–131.
  • N. Dershowitz (1981). "Termination of linear rewriting systems: Preliminary version". In Shimon Even; Oded Kariv (eds.). Proc. ICALP. LNCS. 115. Springer. pp. 448–458.
  • N. Dershowitz (1982). "Orderings for Term-Rewriting Systems" (PDF). Theoret. Comput. Sci. 17 (3): 279–301. doi:10.1016/0304-3975(82)90026-3.
  • Dershowitz, N. (1985). "Termination" (PDF). In Jean-Pierre Jouannaud (ed.). Rewriting Techniques and Applications, 1st Int. Conf., RTA-85. LNCS. 202. Springer. pp. 180–224.
  • Bachmair, L. and Dershowitz, N. and Hsiang, J. (Jun 1986). "Orderings for Equational Proofs". Proc. IEEE Symposium on Logic in Computer Science (LICS). Cambridge/MA. pp. 346–357.CS1 maint: Multiple names: authors list (link)
  • Bachmair, L. & Dershowitz, N. (1987). "Completion for Rewriting Modulo a Congruence". In Lescanne, Pierre (ed.). Rewriting Techniques and Applications, 2nd Int. Conf., RTA-87. LNCS. 256. Springer. pp. 192–203.
  • Nachum Dershowitz (1987). "Termination of Rewriting" (PDF). J. Symbolic Comput. 3 (1–2): 69–116. doi:10.1016/s0747-7171(87)80022-6.
  • N. Dershowitz & M. Okada (1988). "Proof-Theoretic Techniques for Term Rewriting Theory". Proc. 3rd IEEE Symp. on Logic in Computer Science (PDF). pp. 104–111.
  • N. Dershowitz & G. Sivakumar (1988). "Solving Goals in Equational Languages". Proc. 1st Int. Workshop on Conditional Term Rewriting Systems. LNCS. 308. Springer. pp. 45–55.
  • Dershowitz, Nachum, ed. (1989). Rewriting Techniques and Applications, 3rd Int. Conf., RTA-89. LNCS. 355. Springer.
  • N. Dershowitz & J.-P. Jouannaud (1990). "Rewrite Systems". In Jan van Leeuwen (ed.). Formal Models and Semantics. Handbook of Theoretical Computer Science. B. Elsevier. pp. 243–320.
  • N. Dershowitz & J.-P. Jouannaud (1990). "Notations for Rewriting".
  • Dershowitz, N. and Jouannaud, J.-P. and Jan Willem Klop (1991). "Open Problems in Rewriting". In Ronald V. Book (ed.). Rewriting Techniques and Applications, 4th Int. Conf., RTA-91. LNCS. 488. Springer. pp. 445–456.CS1 maint: Multiple names: authors list (link)
  • Dershowitz, N. and Jouannaud, J.-P. and Klop, J.W. (1993). "More Problems in Rewriting". In Kirchner, Claude (ed.). Rewriting Techniques and Applications, 5th Int. Conf., RTA-93. LNCS. 690. Springer. pp. 468–487.CS1 maint: Multiple names: authors list (link)
  • Nachum Dershowitz (Apr 1993). "Trees, Ordinals and Termination". Proc. CAAP/TAPSOFT (PDF). LNCS. 668. Springer. pp. 243–250.
  • Dershowitz, N. & Hoot, C. (1993). "Topics in Termination". In Kirchner, Claude (ed.). Rewriting Techniques and Applications, 5th Int. Conf., RTA-93. LNCS. 690. Springer. pp. 198–212.
  • Dershowitz, N. (1997). "Innocuous Constructor-Sharing Combinations". In Comon, Hubert (ed.). Rewriting Techniques and Applications, 8th Int. Conf., RTA-97. LNCS. 1232. Springer. pp. 202–216.
  • Dershowitz, Nachum and Reingold, Edward M., Calendrical Calculations, Cambridge University Press, ISBN 0521702380, 1997
  • Dershowitz, N. & Treinen, R. (1998). "An On-line Problem Database". In Tobias Nipkow (ed.). Rewriting Techniques and Applications, 9th Int. Conf., RTA-98. LNCS. 1379. Springer. pp. 332–342.
  • Dershowitz, N. & Mitra, S. (1999). "Jeopardy". In Narendran, Paliath & Rusinowitch, Michaël (eds.). Rewriting Techniques and Applications, 10th Int. Conf., RTA-99. LNCS. 1631. Springer. pp. 16–29.
  • Nachum Dershowitz and David A. Plaisted (2001). "Rewriting (Chapter 9)". In Alan Robinson; Andrei Voronkov (eds.). Handbook of Automated Reasoning. MIT Press + Elsevier. pp. 535–610.
  • Dershowitz, N. (2005). "Term Rewriting and Applications". In Giesl, J. (ed.). Term Rewriting and Applications, 16th Int. Conf., RTA-05. LNCS. 3467. Springer. pp. 376–393. ISBN 978-3-540-25596-3.
  • Dershowitz, N. & Castedo Ellerman, E. (2005). "Leanest Quasi-orderings". In Giesl, J. (ed.). Term Rewriting and Applications, 16th Int. Conf., RTA-05. LNCS. 3467. Springer. pp. 32–45. ISBN 978-3-540-25596-3.
  • 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.

References

  1. ^ Herbrand award address
  2. ^ Vita at Academia Europaea

External links

Calendrical calculation

A calendrical calculation is a calculation concerning calendar dates. Calendrical calculations can be considered an area of applied mathematics. Calendrical calculation is one of the five major Savant syndrome characteristics.

Some examples of calendrical calculations:

Converting a Julian or Gregorian calendar date to its Julian day number and vice versa (see the section on calculation in that article for details).

The number of days between two dates, which is simply the difference in their Julian day numbers.

The date of a religious holiday, like Easter (the calculation is known as Computus) or Passover, for a given year.

Converting a date between different calendars. For instance, dates in the Gregorian calendar can be converted to dates in the Islamic calendar with the Kuwaiti algorithm.

Calculating the day of the week.

Dershowitz

Dershowitz and Dershwitz is a surname. Notable people with the surname include:

Alan Dershowitz (born 1938), American lawyer, jurist, writer and political commentator

Eli Dershwitz (born 1995), American Olympic saber fencer, junior world champion

Nachum Dershowitz, Israeli computer scientist

Zecharia Dershowitz (1859-1921), founder of one of the first Yiddish communities in America

Zvi Dershowitz (born 1928), American rabbi, rabbi emeritus at Sinai Temple (Los Angeles).

Dershowitz–Manna ordering

In mathematics, the Dershowitz–Manna ordering is a well-founded ordering on multisets named after Nachum Dershowitz and Zohar Manna. It is often used in context of termination of programs or term rewriting systems.

Suppose that is a partial order, and let be the set of all finite multisets on . For multisets we define the Dershowitz–Manna ordering as follows:

whenever there exist two multisets with the following properties:

An equivalent definition was given by Huet and Oppen as follows:

if and only if

Dhanu (month)

Dhanu, Dhanus or Dhanurmas (धनुर्मास) is a month in the Hindu calendar, Malayalam calendar and others. It corresponds to the zodiacal sign of Sagittarius, and overlaps with approximately the second half of December and about the first half of January in the Gregorian calendar.

Edward Reingold

Edward M. Reingold (born 1945) is a computer scientist active in the fields of algorithms, data structures, graph drawing, and calendrical calculations.

In 1996 he was inducted as a Fellow of the Association for Computing Machinery.In 2000 he retired from University of Illinois at Urbana-Champaign and since then is a professor of computer science and applied mathematics at the Illinois Institute of Technology.

Handbook of Automated Reasoning

The Handbook of Automated Reasoning (ISBN 0444508139, 2128 pages) is a collection of survey articles on the field of automated reasoning. Published on June 2001 by MIT Press, it is edited by John Alan Robinson and Andrei Voronkov. Volume 1 describes methods for classical logic, first-order logic with equality and other theories, and induction. Volume 2 covers higher-order, non-classical and other kinds of logic.

Henk Barendregt

Hendrik Pieter (Henk) Barendregt (born 18 December 1947, Amsterdam) is a Dutch logician, known for his work in lambda calculus and type theory.

Herbrand Award

The Herbrand Award for Distinguished Contributions to Automated Reasoning is an award given by CADE Inc. (although it predates the formal incorporation of CADE) to honour persons or groups for important contributions to the field of automated deduction. The award is named after the French scientist Jacques Herbrand and given at most once per CADE or IJCAR conference. It comes with a prize of US$ 1000. Anyone can be nominated, the award is awarded after a vote among CADE trustees and former recipients, usually with input from the CADE/IJCAR programme committee.

Past recipients of the award are:

Larry Wos (1992)

Woody Bledsoe (1994)

John Alan Robinson (1996)

Wu Wenjun (1997)

Gérard Huet (1998)

Robert S. Boyer and J Strother Moore (1999)

William W. McCune (2000)

Donald W. Loveland (2001)

Mark E. Stickel (2002).

Peter B. Andrews (2003)

Harald Ganzinger (2004)

Martin Davis (2005)

Wolfgang Bibel (2006)

Alan Bundy (2007)

Edmund M. Clarke (2008)

Deepak Kapur (2009)

David Plaisted (2010)

Nachum Dershowitz (2011)

Melvin Fitting (2012)

C Greg Nelson (2013)

Robert L. Constable (2014)

Andrei Voronkov (2015)

Zohar Manna and Richard Waldinger (2016)

Lawrence C. Paulson (2017)

Bruno Buchberger (2018)

Kanyā

Kanyā is one of the twelve months in Indian solar calendar.Kanya corresponds to the zodiacal sign of Virgo, and overlaps with about the second half of September and about the first half of October in the Gregorian calendar. In Vedic texts, the Kanya month is called Nabhasya (IAST: Nabhasya), but in these ancient texts it has no zodiacal associations. The solar month of Kanya overlaps with its lunar month Ashvin, in Hindu lunisolar calendars. It marks the start of harvests and festival season across the Indian subcontinent. It is preceded by the solar month of Siṃha, and followed by the solar month of Tulā.The Kanya month is called Purattasi in the Tamil Hindu calendar. The ancient and medieval era Sanskrit texts of India vary in their calculations about the duration of Kanya, just like they do with other months. For example, the Surya Siddhanta, dated to c. 400 CE, calculates the duration of Kanya to be 30 days, 10 hours, 35 minutes and 36 seconds. In contrast, the Arya Siddhanta calculates the duration of the Kanya month to be 30 days, 10 hours, 57 minutes and 36 seconds.The Indian solar month names are significant in epigraphical studies of South Asia. For example, Kanya month, along with other solar months, are found inscribed in medieval era Hindu temples.Kanya is also an astrological sign in Indian horoscope systems, corresponding to Virgo (astrology).

Karkaṭa

Karkaṭa, also referred to as Karka or Karkatha, is a month in Indian solar calendar. It corresponds to the zodiacal sign of Cancer, and overlaps approximately with later half of July and early half of August in the Gregorian calendar.In Vedic texts, the Karka month is called Suchi (IAST: Śuchi), but in these ancient texts it has no zodiacal associations. The solar month of Karkata overlaps with its lunar month Shraavana, in Hindu lunisolar calendars. The Shraavana marks the middle of the monsoon season on the Indian subcontinent, and is preceded by the solar month of Mithuna, and followed by the solar month of Siṃha.The Karkata month is called Adi in the Tamil Hindu calendar. The ancient and medieval era Sanskrit texts of India vary in their calculations about the duration of Karkata, just like they do with other months. For example, the Surya Siddhanta calculates the duration of Karkata to be 31 days, 11 hours, 24 minutes and 24 seconds. In contrast, the Arya Siddhanta calculates the duration of the Karkata month to be 31 days, 11 hours, 13 minutes and 36 seconds.The Indian solar month names are significant in epigraphical studies of South Asia. For example, Karkaṭa month, along with other solar months are found inscribed in medieval era temples. The Karkaṭa month (spelled as Karkataka) is found inscribed in Chola Empire monument such as the Valisvara temple near Tamil Nadu–Andhra Pradesh border.Karka is also an astrological sign in Indian horoscope systems, corresponding to Cancer (astrology).

Kumbha (month)

Kumbha is a month in Indian solar calendar. It corresponds to the zodiacal sign of Aquarius, and overlaps with about the second half of February and about the first half of March in the Gregorian calendar.In Vedic texts, the Kumbha month is called Tapas (IAST: Tapas), but in these ancient texts it has no zodiacal associations. The solar month of Kumbha overlaps with its lunar month Phalguna, in Hindu lunisolar calendars. The Kumbha marks the end of winter for the Indian subcontinent. It is preceded by the solar month of Makara, and followed by the solar month of Mīna. The solar month is significant because it inspires the name of the 12-year cycled Kumbha Mela, where Hindu pilgrims gather by tens of millions to one of four pilgrimage sites, in the weeks before it starts.The Kumbha month is called Masi in the Tamil Hindu calendar. The ancient and medieval era Sanskrit texts of India vary in their calculations about the duration of Kumbha, just like they do with other months. For example, the Surya Siddhanta calculates the duration of Kumbha to be 29 days, 19 hours, 41 minutes and 12 seconds. In contrast, the Arya Siddhanta calculates the duration of the Kumbha month to be 29 days, 19 hours, 24 minutes and 0 seconds.Kumbha is also an astrological sign in Indian horoscope systems, corresponding to Aquarius (astrology).

Makara (month)

Makara is a month in Indian solar calendar. It corresponds to the zodiacal sign of Capricorn, and overlaps with about the later half of January and approximately early half of February in the Gregorian calendar.In Vedic texts, the Makara month is called Sahasya (IAST: Sahasya), but in these ancient texts it has no zodiacal associations. The solar month of Makara overlaps with its lunar month Magha, in Hindu lunisolar calendars. The Makara marks the month with lengthening day lengths on the Indian subcontinent. It is preceded by the solar month of Dhanu, and followed by the solar month of Kumbha. The start of this month is almost always January 14, the day of the Makara Sankranti festival, and periodically the Kumbh Mela.The Makara month is called Tai in the Tamil Hindu calendar. The ancient and medieval era Sanskrit texts of India vary in their calculations about the duration of Makara, just like they do with other months. For example, the Surya Siddhanta calculates the duration of Vrschika to be 29 days, 10 hours, 45 minutes and 12 seconds. In contrast, the Arya Siddhanta calculates the duration of the Vrschika month to be 29 days, 10 hours, 57 minutes and 35 seconds.Makara (crocodile or half animal-half fish being) is also an astrological sign in Indian horoscope systems, corresponding to Capricorn (astrology).

Meṣa

Meṣa, or Mesha (मेष), is a month in Indian solar calendar. It corresponds to the zodiacal sign of Aries, and overlaps with about the second half of April and about the first half of May in the Gregorian calendar.In Vedic texts, the Mesa month is called Madhu (IAST: Madhu), but in these ancient texts it has no zodiacal associations. The solar month of Mesha overlaps with its lunar month Vaisakha, in Hindu lunisolar calendars. The Mesha is preceded by the solar month of Mīna, and followed by the solar month of Vṛṣabha.The Mesha month is called Chittirai in the Tamil calendar, and is its first month. The ancient and medieval era Sanskrit texts of India vary in their calculations about the duration of Mesha, just like they do with other months. For example, the Surya Siddhanta calculates the duration of Mesha to be 30 days, 22 hours, 26 minutes and 48 seconds. In contrast, the Arya Siddhanta calculates the duration of Mesha to be 30 days 22 hours 12 minutes.Mesha is also an astrological sign in Indian horoscope systems, corresponding to Aries.

Mithuna (month)

Mithuna is a month in Indian solar calendar. It corresponds to the zodiacal sign of Gemini, and overlaps with about the second half of June and about the first half of July in the Gregorian calendar.In Vedic texts, the Mithuna month is called Shukra (IAST: Śukra), but in these ancient texts it has no zodiacal associations. The solar month of Mithuna overlaps with its lunar month Ashadha, in Hindu lunisolar calendars. The Mithuna marks the start of the monsoon season on the Indian subcontinent, and is preceded by the solar month of Vrsabha, and followed by the solar month of Karkaṭa.The Mithuna month is called Ani in the Tamil Hindu calendar. The ancient and medieval era Sanskrit texts of India vary in their calculations about the duration of Mithuna, just like they do with other months. For example, the Surya Siddhanta calculates the duration of Mithuna to be 31 days, 15 hours, 28 minutes and 24 seconds. In contrast, the Arya Siddhanta calculates the duration of the Mithuna month to be 31 days, 14 hours, 34 minutes and 24 seconds.Mithuna is also an astrological sign in Indian horoscope systems, corresponding to Gemini (astrology).

Mīna

Mīna, or Meena, is a month in Indian solar calendar. It corresponds to the zodiacal sign of Pisces, and overlaps with about the later half of March and about the early half of April in the Gregorian calendar.In Vedic texts, the Mina month is called Tapasya (IAST: Tapasya), but in these ancient texts it has no zodiacal associations. The solar month of Mina overlaps with its lunar month Chaitra, in Hindu lunisolar calendars. The Mina marks the spring season for the Indian subcontinent. It is preceded by the solar month of Kumbha, and followed by the solar month of Meṣa.The Mina month is called Panguni in the Tamil Hindu calendar, and is its last month in the traditional calendar. The ancient and medieval era Sanskrit texts of India vary in their calculations about the duration of Mina, just like they do with other months. For example, the Surya Siddhanta calculates the duration of Mina to be 30 days, 8 hours, 29 minutes and 1 second. In contrast, the Arya Siddhanta calculates the duration of the Mina month to be 30 days, 8 hours, 7 minutes and 42 seconds.The Indian solar month names are significant in epigraphical studies of South Asia. For example, the Mina month, along with other solar months are found inscribed in medieval era temples. The Mina month is found inscribed in Chola Empire monuments.Mina (literally, fish) is also an astrological sign in Indian horoscope systems, corresponding to Pisces (astrology).

Tobias Nipkow

Tobias Nipkow (born 1958) is a German computer scientist. He received his Diplom (MSc) in computer science from the Technische Hochschule Darmstadt in 1982, and his Ph.D. from the University of Manchester in 1987. He worked at MIT from 1987, changed to Cambridge University in 1989, and to Technical University Munich in 1992, where he was appointed professor for programming theory. He is chair of the Logic and Verification group since 2011.

He is known for his work in interactive and automatic theorem proving, in particular for the Isabelle proof assistant; he is the editor of the Journal of Automated Reasoning. Moreover, he focuses on programming language semantics, type systems and functional programming.

Vṛścik‌‌‌a

Vṛścik‌‌‌a, also referred to as Vrishchika or Vrschika, is a month in Indian solar calendar. It corresponds to the zodiacal sign of Scorpio, and approximately overlaps with later half of November and first half of December in the Gregorian calendar.In Vedic texts, the Vrscika month is called Urja (IAST: Ūrja), but in these ancient texts it has no zodiacal associations. The solar month of Vrschika overlaps with its lunar month Agahana or Mangsir, in Hindu lunisolar calendars. The Vrschika marks the end of the autumn season and the start of the winter on the Indian subcontinent, and is preceded by the solar month of Tulā, and followed by the solar month of Dhanu.The Vrschika month is called Kartigai in the Tamil Hindu calendar. The ancient and medieval era Sanskrit texts of India vary in their calculations about the duration of Vrschika, just like they do with other months. For example, the Surya Siddhanta calculates the duration of Vrschika to be 29 days, 11 hours, 46 minutes and 0 seconds. In contrast, the Arya Siddhanta calculates the duration of the Vrschika month to be 29 days, 12 hours, 12 minutes and 24 seconds.The Indian solar month names are significant in epigraphical studies of South Asia. For example, Vrischika month, along with other solar months are found inscribed in medieval era temples. The Vrischika month, along with the other months, is found inscribed in Chola Empire monuments.Vrschika is also an astrological sign in Indian horoscope systems, corresponding to Scorpio (astrology).

Vṛṣabha

Vṛṣabha, or Vrishabha, is a month in Indian solar calendar. It corresponds to the zodiacal sign of Taurus, and overlaps with about the second half of May and about the first half of June in the Gregorian calendar.In Vedic texts, the Vrsabha month is called Madhava (IAST: Mādhava), but in these ancient texts it has no zodiacal associations. The solar month of Vrsabha overlaps with its lunar month Jyeshtha, in Hindu lunisolar calendars. The Vrsabha is preceded by the solar month of Mesha, and followed by the solar month of Mithuna.The Vrsabha month is called Vaikasi in the Tamil Hindu calendar. The ancient and medieval era Sanskrit texts of India vary in their calculations about the duration of Vrsabha, just like they do with other months. For example, the Surya Siddhanta calculates the duration of Vrishabha to be 31 days, 10 hours, 5 minutes and 12 seconds. In contrast, the Arya Siddhanta calculates the duration of Vrsabha to be 31 days, 9 hours, 37 minutes and 36 seconds.The Indian solar month names are significant in epigraphical studies of South Asia. For example, Vrsabha month, along with other solar months, are found inscribed in medieval era Hindu temples, sometimes spelled as the Rishabha month.Vrsabha is also an astrological sign in Indian horoscope systems, corresponding to Taurus.

Wayne Snyder

Wayne Snyder is an associate professor at Boston University known for his work in E-unification theory.

He was raised in Yardley, Pennsylvania, worked in his father's aircraft shop, attended the Berklee School of Music, and obtained an MA in Augustan poetry at Tufts University.

He then studied computer science, and earned his Ph.D. at the University of Pennsylvania in 1988.

In 1987 he came to Boston University, teaching introductory computer science, and researching on automated reasoning, and, more particularly, E-unification.

This page is based on a Wikipedia article written by authors (here).
Text is available under the CC BY-SA 3.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.