Nachum Dershowitz Knihy

The purpose of this book is to present in a unified, completely algorithmic form, a description of thirteen calendars and how they relate to one another: the present civil calendar (Gregorian), the recent ISO commercial calendar, the old civil calendar (Julian), the Coptic and (virtually identical) Ethiopic calendars, the Islamic (Moslem) calendar, the Baha'i, the Hebrew (Jewish) calendar, the Mayan calendars, the French Revolutionary calendar, the Chinese calendar, and both the old (mean) and new (true) Hindu (Indian) calendars. Easy conversion among these calendars is a by-product of the approach, as is the determination of secular and religious holidays. Calendrical Calculations makes accurate calendrical algorithms readily available for computer use. This volume will be a valuable resource for working programmers, as well as a fount of useful algorithmic tools for computer scientists.

The book covers a range of topics in logic and computational theory, beginning with an exploration of Hilbert’s Program and its evolution into a logic toolbox. It discusses vacuous truth and the challenges in deductive question answering, alongside decidable fragments of many-sorted logic. The text delves into one-pass tableaux for computation tree logic and extends resolution provers to handle inequalities on elementary functions. It also examines model checking within the first-order fragment of higher-order fixpoint logic and the decidability of monadic fragments of Gödel logics. Key concepts include fixed points in linear logic, semantics of consistency and trust in peer data exchange, and completeness in sequence logic. The book introduces Zenon, an extensible automated theorem prover, and addresses matching in hybrid terminologies. It covers the verification of cryptographic protocols and knowledge in security protocols, as well as mechanized verification of CPS transformations. Further discussions include operational and epistemic approaches to protocol analysis, verification methods, and extensions of abstract categorial grammars. The content also touches on finite satisfiability in the guarded fragment, data complexity in description logics, and algorithms for propositional model counting. Lastly, it addresses the complexity of temporal logic and ATP cross-verification of Mizar MPTP challenge problems.

This festschrift volume constitutes a unique tribute to Zohar Manna on the occasion of his 64th birthday. Like the scientific work of Zohar Manna, the 32 research articles span the entire scope of the logical half of computer science. Also included is a paean to Zohar Manna by the volume editor. The articles presented are devoted to the theory of computing, program semantics, logics of programs, temporal logic, automated deduction, decision procedures, model checking, concurrent systems, reactive systems, hardware and software verification, testing, software engineering, requirements specification, and program synthesis.

This book presents throroughly revised full versions of the 21 papers accepted for the Fourth International Workshop on Conditional and Typed Rewriting Systems, CTRS-94, held in conjunction with ICALP '94 in Jerusalem, Israel, in July 1994. The volume reports the research advances in the area of rewriting in general achieved since the predecessor workshop held in July 1992. Among the topics addressed are conditional term rewriting, typed systems, higher-order rewriting, graph rewriting, combinator-based languages, and constrained rewriting.