A NATURAL AXIOMATIZATION OF COMPUTABILITY AND PROOF OF CHURCH’S THESIS (2009)
Nachum Dershowitz, Yuri Gurevich
Abstract. Church’s Thesis asserts that the only numeric functions that can be calculated by effective means are the recursive ones, which are the same, extensionally, as the Turingcomputable...
A CRITICAL PAIR CRITERION FOR COMPLETION MODULO A CONGRUENCE 1 (2009)
Leo Bachmair, Nachum Dershowitz
Rewrite systems axe collections of directed equations (rules) used to compute by repeatedly replacing subterms in a given formula until a simplest form possible (normal form) is obtained. Many...
The Influence of Domain Interpretations on Computational Models ⋆ (2009)
Computational models are usually defined over specific domains. For example, Turing machines are defined over strings, and the recursive functions over the natural numbers. Nevertheless, one often...
Infinite Normal Forms (Preliminary Version) (2009)
Nachum Dershowitz, Strphane Kaplan, David A. Plalsted
We continue here a study of properties of rewrite systems that are not necessarily terminating, but allow for infinite derivations that have a limit. In particular, we give algebraic semantics for...
The Church-Turing Thesis over Arbitrary Domains, in A. Avron et al (2009)
For Boaz, pillar of a new discipline. Abstract. The Church-Turing Thesis has been the subject of many variations and interpretations over the years. Specifically, there are versions that refer only...
Abstract. Bit vectors and bit operations are proposed for efficient propositional inference. Bit arithmetic has efficient software and hardware implementations, which can be put to advantage in...
Indian Calendrical Calculations ∗ (2009)
Nachum Dershowitz, Edward M. Reingold
Summary. We analyse various Indian calendars. We discuss the Indian day count, a generic solar calendar that generalizes various calendars including the mean Indian solar calendar, the true and...
Matching Phrases for Arabic-to-English Example-Based Translation (2008)
Kfir Bar, Yaacov Choueka, Nachum Dershowitz
An implementation of a non-structural Example-Based Machine Translation system that translates sentences from Arabic to English, using a parallel corpus aligned at the paragraph level, is described....
Endless Commuting: Finite Rearrangement (2008)
Abstract. We investigate a combinatorial commutation property for reordering a sequence of two kinds of steps, and for separating wellfoundedness of unions of binary relations. We show how this...
Abstract DCM 2005 Preliminary Version Abstract Effective Models (2008)
We modify Gurevich’s notion of abstract machine so as to encompass computational models, that is, sets of machines that share the same domain. We also add an effectiveness requirement. The...
From Backtracking to Chaff (2008)
Abstract. Modern Chaff-like SAT solvers enhance plain backtracking (DLL) by Conflict-Driven Learning (CDL), including 1UIP-based Conflict-Directed Backjumping (CDB), Non-Chronological Backtracking...
SPREADSPACES: Mathematically-Intelligent Graphical Spreadsheets (2008)
Nachum Dershowitz, Claude Kirchner, Ugo Montanari, Francesca Rossi
Abstract. Starting from existing spreadsheet software, like Lotus 1-2-3 R ○ , Excel R ○ , or Spreadsheet 2000 R ○ , we propose a sequence of enhancements to fully integrate constraint-based...
When are two algorithms the same? (2008)
Blass, Andreas, Dershowitz, Nachum, Gurevich, Yuri
People usually regard algorithms as more abstract than the programs that implement them. The natural way to formalize this idea is that algorithms are equivalence classes of programs with respect to...
Intersection-Based Methods for Satisfiability Using Boolean Rings (2008)
Nachum Dershowitz, Jieh Hsiang, Guan-shieng Huang, Daher Kaiss
Abstract. A potential advantage of using a Boolean-ring formalism for propositional formulæ is the large measure of simplification it facilitates. We propose a combined linear and binomial...
The Church-Turing Thesis over Arbitrary Domains ⋆ (2008)
For Boaz, pillar of a new discipline. Abstract. The Church-Turing Thesis has been the subject of many variations and interpretations over the years. Specifically, there are versions that refer only...
WHEN ARE TWO ALGORITHMS THE SAME? (2008)
Andreas Blass, Nachum Dershowitz, Yuri Gurevich
than the programs that implement them. The natural way to formalize this idea is that algorithms are equivalence classes of programs with respect to a suitable equivalence relation. We argue that no...
The RTA list of open problems (2008)
Nachum Dershowitz, Ralf Treinen
The RTA list of open problems 1 The RTA list of open problems summarizes open problems in the field of the International Conference on Rewriting Techniques and Applications (RTA). For the RTA 2002...
A Formalization of the Church-Turing Thesis for State-Transition Models (2008)
Abstract. Our goal is to formalize the Church-Turing Thesis for a very large class of computational models. Specifically, the notion of an “effective model of computation ” over an arbitrary...
Complexity of Propositional Proofs Under a Promise ⋆ (2008)
Nachum Dershowitz, Iddo Tzameret
Abstract. We study – within the framework of propositional proof complexity – the problem of certifying unsatisfiability of CNF formulas under the promise that any satisfiable formula has many...
Abstract A Hypercomputational Alien (2008)
Is there a physical constant with the value of the halting function? An answer to this question, as holds true for other discussions of hypercomputation, assumes a fixed interpretation of nature by...
Abstract Abstract Canonical Presentations ⋆ (2008)
Nachum Dershowitz, Claude Kirchner, Loria Inria
Solving goals—like proving properties, deciding word problems or resolving constraints—is much easier with some presentations of the underlying theory than with others. What have been called...
Canonical Ground Horn Theories (2008)
Maria Paola Bonacina, Nachum Dershowitz, Harald Ganzinger
Dedicated to the memory of
Cambridge University Press 978-0-521-88540-9- Calendrical Calculations, Third Edition (2008)
Nachum Dershowitz, Edward M. Reingold, More Information
This new edition of the popular calendar book expands the treatment of the previous edition to new calendar variants: generic cyclical calendars and astronomical lunar calendars, as well as the...
The Hydra Battle Revisited ⋆ (2008)
Nachum Dershowitz, Georg Moser
To Jean-Pierre on this momentous occasion. Abstract. Showing termination of the Battle of Hercules and Hydra is a challenge. We present the battle both as a rewrite system and as an arithmetic while...
A Gap Tree Theorem for Quasi-Ordered Labels 1 (2008)
Nachum Dershowitz, Iddo Tzameret
Given a quasi-ordering of labels, a labelled ordered tree s is embedded with gaps in another tree t if there is an injection from the nodes of s into those of t that maps each edge in s to a unique...
Matching with a Hierarchical Ontology (2008)
Yaacov Choueka, Nachum Dershowitz, Liad Tal
Abstract. We describe how hierarchical ontologies are used for classifying products, as well as for answering queries. For classifying and scoring product descriptions and queries in an...
Electronic Notes in Theoretical Computer Science (2008)
We modify Gurevich’s notion of abstract machine so as to encompass computational models, that is, sets of machines that share the same domain. We also add an effectiveness requirement. The...
The Four Sons of Penrose (2008)
Abstract. We distill Penrose’s argument against the “artificial intelligence premiss”, and analyze its logical alternatives. We then clarify the different positions one can take in answer to...
AUTOMATIC PROGRAM ANNOTATION (2008)
Techniques were developed by which an Algol-like program, given together with its specifications, may be documented automatically. This documentation expresses invariant relationships that hold...
Abstract Effective Models (2008)
We modify Gurevich’s notion of abstract machine so as to encompass computational models, that is, sets of machines that share the same domain. We also add an effectiveness requirement. The...
Boolean Rings for Intersection-Based Satisfiability (2008)
Nachum Dershowitz, Guan-shieng Huang, Daher Kaiss
There is not a person in this courtroom who has never told a lie, who has never done an immoral thing, and there is no man living who has never looked upon a woman without desire. 1 —Harper Lee: To...
Abstract ASSOCIATIVE-COMMUTATIVE REWRITING* (2008)
Nachum Dershowitz, N. Alan Josephson
We are currently extending the rewrite system laboratory REVE to handle associative-commutative operators. In particular, we are incorporating a set of rules for Boolean algebra that provides a...
The RTA list of open problems (2008)
Nachum Dershowitz, Ralf Treinen
The RTA list of open problems 1 The RTA list of open problems summarizes open problems in the field of the International Conference on Rewriting Techniques and Applications (RTA). For the RTA 2002...
Nachum Dershowitz, Naomi Lindenstrauss, Yehoshua Sagiv, Alexander Serebrenik
Abstract This paper describes a general framework for automatic termination analysis of logic programs, where we understand by \termination" the niteness of the LD-tree constructed for the...
Abstract Abstract Canonical Presentations ⋆ (2008)
Nachum Dershowitz, Claude Kirchner, Inria Loria
Solving goals—like proving properties, deciding word problems or resolving constraints—is much easier with some presentations of the underlying theory than with others. Typically, what have been...
Abstract A Hypercomputational Alien ⋆ (2008)
Is there a physical constant with the value of the halting function? An answer to this question, as in other discussions of hypercomputation, assumes a fixed interpretation of nature by mathematical...
COMPLEXITY OF PROPOSITIONAL PROOFS UNDER A PROMISE (2008)
Nachum Dershowitz, Iddo Tzameret
Abstract. We study – within the framework of propositional proof complexity – the problem of certifying unsatisfiability of CNF formulas under the promise that any satisfiable formula has many...
���� � ��� � ��� � Open closed open. ���� � � � � � That is Man. (2008)
Nachum Dershowitz, Yehudah Amichai (israel
Abstract. As a window into the subject, we recount some of the history (and geography) of two mature, challenging, partially open, partially closed problems in the theory of rewriting (numbers 13 and...
The Hydra Battle Revisited ⋆ (2008)
Nachum Dershowitz, Georg Moser
To Jean-Pierre on this momentous occasion. Abstract. Showing termination of the Battle of Hercules and Hydra is a challenge. We present the battle both as a rewrite system and as an arithmetic while...
Abstract Leanest Quasi-Orderings (2008)
Nachum Dershowitz, E. Castedo Ellerman
A convenient method for defining a quasi-ordering, such as those used for proving termination of rewriting, is to choose the minimum of a set of quasi-orderings satisfying some desired traits....
Automatic Inductive Synthesis of Functional Programs ⋆ (2008)
Nachum Dershowitz, Ely Pinchover
Abstract. An automated system for the synthesis of functional programs, expressed as a convergent set of rewrite rules, is presented. Deductive and inductive rewriting techniques are combined to...
Termination Dependencies (2008)
The innovative dependency-pair termination method of [1, 2] relies on two important observations: – If a rewrite system is nonterminating, then there is an infinite derivation with at least one...
MORE PATTERNS IN TREES: UP AND DOWN, YOUNG AND OLD, ODD AND EVEN (2008)
Nachum Dershowitz, Shmuel Zaks
Abstract. We apply the tree-pattern enumeration formulæ of [7], and a new extension thereof, to some recent enumerations of distributions of leaves in ordered trees [4] and in bicolored ordered...
Boosting Satisfiability Testing Using Boolean Rings (2008)
Daher Kaiss, Nachum Dershowitz
Given a Boolean formula A, the satisfiability problem is concerned with finding an assignment of truth values (0 and 1) to the propositional variables in A that gives the formula the value 1 (true),...
Chapter 6 of Handbook of Theoretical Computer Science Volume B: Formal Methods and Semantics (2008)
Nachum Dershowitz, Jean-pierre Jouannaud
J. van Leeuwen, ed.
Quasi-Ordered Gap Embedding ⋆ —Extended Abstract— (2008)
Nachum Dershowitz, Iddo Tzameret
Kruskal’s Tree Theorem [3], stating that finite trees are well-quasi-ordered under homeomorphic embedding, and its extensions, have played an important rôle in both logic and computer science. In...
The Church-Turing Thesis over Arbitrary Domains ⋆ (2008)
Abstract. The Church-Turing Thesis has been the subject of many variations and interpretations over the years. Specifically, there are versions that refer only to functions over the natural numbers...
Enumerating the Propositions Equivalent to a (2008)
Boolean Function Nachum, Nachum Dershowitz, Mitchell A. Harris
A general method is presented for counting the propositional formulas of a given size that are equal to an arbitrary boolean function.
Canonical Inference for Implicational Systems (2008)
Maria Paola Bonacina, Nachum Dershowitz
Abstract. Completion is a general paradigm for applying inferences to generate a canonical presentation of a logical theory, or to semi-decide the validity of theorems, or to answer queries. We...
Trees, ordinals and termination (2007)
Know that one is the secret and sourceofallthecardinals.--- Abraham ibn Ezra #1153# Trees are a natural representation for countable ordinals. In particular, #nite trees provide a convenient notation...
ATaste of Rewrite Systems (2007)
Abstract. This survey of the theory and applications of rewriting with equations discusses the existence and uniqueness of normal forms, the Knuth-Bendix completion procedure and its variations, as...
When are Two Rewrite Systems More than None?? (2007)
Abstract. It is important for programs to have modular correctness properties. We look at non-deterministic programs expressed as termrewriting systems (which compute normal forms of input terms) and...
1 Background Canonical Sets of Horn Clauses (2007)
Rewrite rules are oriented equations used to replace equals-by-equals in the speci ed direction. Input terms are repeatedly rewritten according to the rules. When and if no rule applies, the...
Matching and Uni cation in Rewrite Theories (2007)
Subrata Mitra, Nachum Dershowitz
\Semantic uni cation " is the process of generating a basis set of substitutions (of terms for variables) that makes two given terms equal in a speci ed theory. Semantic uni cation is an...
Semigroups Satisfying x m+n = x n (2007)
We summarize recent results on semigroups satisfying the identity x m+n = x n, for n 0andm 1, and some rewrite techniques that have contributed to their investigation. 1
Subrata Mitra, Nachum Dershowitz
\Semantic matching " is the process of generating a basis set of substitutions (of terms for variables) that makes one term equal to another in a speci ed theory. We restrict ourselves here...
Nachum Dershowitz, Hon-wai Leong
We present three variations of the following new sorting theme: Throughout the sort, the array ismaintained in piles of sorted elements. At each step, the piles are split into two parts, so that the...
Communicated by Received Revised (2007)
Nachum Dershowitz, Charles Hoot
Abstract. Twotechniques are examined for showing termination of rewrite systems when simpli cation ordering are insu cient. The rst approach generalizes the various path orderings and the conditions...
Nachum Dershowitz, Subrata Mitra, G. Sivakumar
We describe decision procedures for certain classes of semantic matching problems, where the equational theory with respect to which the semantic matching is performed has a convergent rewrite...
Primitive and Partial Rewriting--- DRAFT--- (2007)
Indeed, if general recursive function is the formal equivalent of effective calculability, its formulation may play a role in the history of combinatory mathematics second only to that of the...
Nachum Dershowitz, Claude Kirchner
Abstract. We consider the problem of inversion, for functions dened by ground-convergent rewrite systems. That is, we are looking for an algorithm for nding most general solutions to problems of the...
COMPLETION WITHOUT FAILURE 1 (2007)
Leo Bachmair, Nachum Dershowitz, David A. Plaisted
Abstract. We present an \unfailing " extension of the standard Knuth-Bendix completion procedure that is guaranteed to produce a desired canonical system, provided certain conditions are...
Nachum Dershowitz, Subrata Mitra
An algorithm is given for inverting functions de#ned by left-linear ground convergent rewrite systems, with left sides restricted in depth and right sides not having de#ned symbols at the top. 1...
Automatic Termination Analysis of Programs Containing Arithmetic Predicates (2007)
Nachum Dershowitz, Naomi Lindenstrauss, Yehoshua Sagiv, Alexander Serebrenik
For logic programs with arithmetic predicates, showing termination is not easy, since the usual order for the integers is not well-founded. A new method, easily incorporated in the TermiLog system...
Semigroups Satisfying x m+n = x n (2007)
We summarize recent results on semigroups satisfying the identity x m+n = x n , for n 0 and m 1, and some rewrite techniques that have contributed to their investigation. 1 Introduction Ninety years...
When are Two Rewrite Systems More than None? (2007)
. It is important for programs to have modular correctness properties. We look at non-deterministic programs expressed as termrewriting systems (which compute normal forms of input terms) and...
Nachum Dershowitz, Subrata Mitra
An algorithm is given for inverting functions defined by left-linear ground convergent rewrite systems, with left sides restricted in depth and right sides not having defined symbols at the top. 1...
Trees, Ordinals and Termination (2007)
Trees are a natural representation for countable ordinals. In particular, finite trees provide a convenient notation for the predicative ones. Processes that transform trees or terms can often be...
Ordered Construction Of Combinatorial Objects (2007)
Mitch Harris, Nachum Dershowitz
. The generating function method for counting species of combinatorial objects is applied to the construction of the objects in order. The species considered are those described using context-free...
Matching and Unification in Rewrite Theories (2007)
Subrata Mitra, Nachum Dershowitz
"Semantic unification" is the process of generating a basis set of substitutions (of terms for variables) that makes two given terms equal in a specified theory. Semantic unification is an...
Nachum Dershowitz, Hon-wai Leong
We present three variations of the following new sorting theme: Throughout the sort, the array is maintained in piles of sorted elements. At each step, the piles are split into two parts, so that the...
Edward M. Reingold, Nachum Dershowitz, Stewart M. Clamen, French Revolutionary, Old Hindu
Algorithmic presentations are given for three calendars of historical interest, the Mayan,
KEY WORDS Calendar Holidays Gregorian calendar Hebrew calendar Islamic calendar ISO calendar (2007)
Nachum Dershowitz, M. Reingold, Julian Calendar
A unified, algorithmic presentation is given for the Gregorian (current civil), ISO, Julian (old civil), Islamic (Moslem), and Hebrew (Jewish) calendars. Easy conversion among these calendars is a...
Automatic Termination Analysis of Programs Containing Arithmetic Predicates (2007)
Nachum Dershowitz, Naomi Lindenstrauss, Yehoshua Sagiv, Alexander Serebrenik
For logic programs with arithmetic predicates, showing termination is not easy, since the usual order for the integers is not well-founded. A new method, easily incorporated in the TermiLog system...
Nachum Dershowitz, Naomi Lindenstrauss, Yehoshua Sagiv, Alexander Serebrenik
The date of receipt and acceptance will be inserted by the editor Abstract This paper describes a general framework for automatic termination analysis of logic programs, where we understand by...
WoLLIC 2003 Preliminary Version (2007)
Gap Embedding For, Nachum Dershowitz, Iddo Tzameret
Given a quasi-ordering of labels, a labelled ordered tree s is embedded with gaps in another tree t if there is an injection from the nodes of s into those of t that maps each edge in s to a unique...
The Four Sons Of Penrose (2007)
We analyze Penrose's argument against the "strong artificial intelligence" premiss, as well as its logical alternatives. We then clarify the different positions one can take in answer...
Complexity of Propositional Proofs under a Promise (2007)
Dershowitz, Nachum, Tzameret, Iddo
We study -- within the framework of propositional proof complexity -- the problem of certifying unsatisfiability of CNF formulas under the promise that any satisfiable formula has many satisfying...
A natural axiomatization of Church’s thesis (2007)
Nachum Dershowitz, Yuri Gurevich
The Abstract State Machine Thesis asserts that every classical algorithm is behaviorally equivalent to an abstract state machine. This thesis has been shown to follow from three natural postulates...
Towards a better understanding of the functionality of a conflict-driven SAT solver (2007)
Nachum Dershowitz, Ziyad Hanna, Er Nadel
Abstract. We show that modern conflict-driven SAT solvers implicitly build and prune a decision tree whose nodes are associated with flipped variables. Practical usefulness of conflict-driven...
Comparing Computational Power (2006)
Boker, Udi, Dershowitz, Nachum
It is common practice to compare the computational power of different models of computation. For example, the recursive functions are strictly more powerful than the primitive recursive functions,...
Enumeration Problems Related to Ground Horn Theories (2006)
Dershowitz, Nachum, Harris, Mitchell A., Huang, Guan-Shieng
We investigate the enumeration of varieties of boolean theories related to Horn clauses. We describe a number of combinatorial equivalences among different characterizations and calculate the number...
A Scalable Algorithm for Minimal Unsatisfiable Core Extraction (2006)
Dershowitz, Nachum, Hanna, Ziyad, Nadel, Alexander
We propose a new algorithm for minimal unsatisfiable core extraction, based on a deeper exploration of resolution-refutation properties. We provide experimental results on formal verification...
A scalable algorithm for minimal unsatisfiable core extraction (2006)
Nachum Dershowitz, Ziyad Hanna, Er Nadel
Abstract. The task of extracting an unsatisfiable core for a given Boolean formula has been finding more and more applications in recent years. The only existing approach that scales well for large...
A scalable algorithm for minimal unsatisfiable core extraction (2006)
Nachum Dershowitz, Ziyad Hanna, Er Nadel
Abstract. We propose a new algorithm for minimal unsatisfiable core extraction, based on a deeper exploration of resolution-refutation properties. We provide experimental results on formal...
Comparing Computational Power (2006)
Boker, Udi, Dershowitz, Nachum
It is common practice to compare the computational power of different models of computation. For example, the recursive functions are strictly more powerful than the primitive recursive functions,...
Comparing Computational Power (2005)
Boker, Udi, Dershowitz, Nachum
It is common practice to compare the computational power of different models of computation. For example, the recursive functions are strictly more powerful than the primitive recursive functions,...
Space-Efficient Bounded Model Checking (2005)
Katz, Jacob, Hanna, Ziyad, Dershowitz, Nachum
Current algorithms for bounded model checking use SAT methods for checking satisfiability of Boolean formulae. These methods suffer from the potential memory explosion problem. Methods based on the...
Space-Efficient Bounded Model Checking (2005)
Katz, Jacob, Hanna, Ziyad, Dershowitz, Nachum
Current algorithms for bounded model checking use SAT methods for checking satisfiability of Boolean formulae. These methods suffer from the potential memory explosion problem. Methods based on the...
Parallel Multithreaded Satisfiability Solver: Design and Implementation (2005)
Yulik Feldman, Nachum Dershowitz, Ziyad Hanna
We describe the design and implementation of a highly optimized, multithreaded algorithm for the propositional satisfiability problem. The algorithm is based on the Davis-Putnam-LogemannLoveland...
Well-Quasi-Orderings on Binary Trees (2005)
Nachum Dershowitz, E. Castedo Ellerman, Edward M. Reingold
We provide a set of “natural ” requirements for quasi-orderings of finite and infinite binary trees. We show that any ordering satisfying these requirements must be well-ordered and that there is...
Undecidability results in rewriting have usually been proved by reduction from undecidable problems of Turing machines or, more recently, from Post’s Correspondence Problem. Another natural...
A clause-based heuristic for SAT solvers (2005)
Nachum Dershowitz, Ziyad Hanna, Er Nadel
Abstract. We propose a new decision heuristic for DPLL-based propositional SAT solvers. Its essence is that both the initial and the conflict clauses are arranged in a list and the next decision...
How to compare the power of computational models (2005)
Abstract. We argue that there is currently no satisfactory general framework for comparing the extensional computational power of arbitrary computational models operating over arbitrary domains. We...
How to compare the power of computational models (2005)
Abstract. We argue that there is currently no satisfactory general framework for comparing the extensional computational power of arbitrary computational models operating over arbitrary domains. We...
Abstract Canonical Inference (2004)
Bonacina, Maria Paola, Dershowitz, Nachum
An abstract framework of canonical inference is used to explore how different proof orderings induce different variants of saturation and completeness. Notions like completion, paramodulation,...
Termination by abstraction (2004)
Abstract. Abstraction can be used very effectively to decompose and simplify termination arguments. If a symbolic computation is nonterminating, then there is an infinite computation with a top...
Boolean Ring Satisfiability (2004)
Nachum Dershowitz, Jieh Hsiang, Guan-shieng Huang, Daher Kaiss
Abstract. We propose a method for testing satisfiability based on Boolean rings. It makes heavy use of simplification, but avoids the potential size increase associated with application of the...
We explore how different proof orderings induce different notions of saturation. We relate completion, paramodulation, saturation, redundancy elimination, and rewrite system reduction to proof...
Abstract saturation-based inference (2003)
Nachum Dershowitz, Claude Kirchner
Solving goals — like deciding word problems or resolving constraints — is much easier in some theory presentations than in others. What have been called “completion processes”, in particular...
Inference Rules for Program Annotation. (2002)
Dershowitz,Nachum, Manna,Zohar
Methods are presented whereby an ALGOL-like program, given together with its specifications, may be documented automatically. This documentation expresses invariant relationships that hold between...
Proving Termination with Multiset Orderings. (2002)
Dershowitz,Nachum, Manna,Zohar
A common tool for proving the termination of programs is the well-founded set, a set ordered in such a way as to admit no infinite descending sequences. The basic approach is to find a termination...
The Evolution of Programs: A System for Automatic Program Modification. (2002)
Dershowitz,Nachum, Manna,Zohar
An attempt is made to formulate techniques of program modification, whereby a program that achieves one result can be transformed into a new program that uses the same principles to achieve a...
Nachum Dershowitz, Farhad Arbab, Cristina Borralleras, Albert Rubio
path ordering......................... 8
Nachum Dershowitz, Farhad Arbab, Cristina Borralleras, Albert Rubio
path ordering......................... 8
A General Framework for Automatic Termination Analysis of Logic Programs (2000)
Dershowitz, Nachum, Lindenstrauss, Naomi, Sagiv, Yehoshua, Serebrenik, Alexander
This paper describes a general framework for automatic termination analysis of logic programs, where we understand by ``termination'' the finitenes s of the LD-tree constructed for the program and a...
Automatic Termination Analysis of Programs Containing Arithmetic Predicates (2000)
Dershowitz, Nachum, Lindenstrauss, Naomi, Sagiv, Yehoshua, Serebrenik, Alexander
For logic programs with arithmetic predicates, showing termination is not easy, since the usual order for the integers is not well-founded. A new method, easily incorporated in the TermiLog system...
Automatic Termination Analysis of Programs Containing Arithmetic Predicates (2000)
Nachum Dershowitz, Naomi Lindenstrauss, Yehoshua Sagiv, Alexander Serebrenik C
For logic programs with arithmetic predicates, showing termination is not easy, since the usual order for the integers is not well-founded. A new method, easily incorporated in the TermiLog system...
Automatic Termination Analysis of Programs Containing Arithmetic Predicates (1999)
Nachum Dershowitz, Naomii Lindenstrauss, Yehoshua Sagiv, Alexander Serebrenik
For logic programs with arithmetic predicates, showing termination is not easy, since the usual order for the integers is not well-founded. A new method, easily incorporated in the TermiLog system...
Jeopardy: Inverting Mildly Deep Definitions (1999)
Nachum Dershowitz, Subrata Mitra
We consider functions defined by ground-convergent left-linear rewrite systems. By restricting the depth of left sides and disallowing defined symbols at the top of right sides, we obtain an...
An on-line problem database (1998)
Nachum Dershowitz, Ralf Treinen
The RTA list of open problems was created in 1991 by Jean-Pierre Jouannaud, Jan Willem Klop, and the rst author [19] on the occasion of the Fourth International Conference onRewriting Techniques and...
Nachum Dershowitz, Shmuel Zaks
0.8> B, and # g#B# the expected girth at an internal node in B. Consider the following correspondence between lattice paths in L n and binary trees: Traverse the path and build a binary tree in...
Nachum Dershowitz, Shmuel Zaks
.07> g(B) the expected girth of a tree in B, and ¯ g(B) the expected girth at an internal node in B. Consider the following correspondence between lattice paths in L n and binary trees: Traverse...
Innocuous constructor-sharing combinations (1997)
Abstract. We investigate conditions under which con uence and/or termination are preserved for constructor-sharing and hierarchical combinations of rewrite systems, one of which is left-linear and...
Semantic Matching in Rewrite Theories (1997)
Subrata Mitra, Nachum Dershowitz
"Semantic matching" is the process of generating a basis set of substitutions (of terms for variables) that makes one term equal to another in a specified theory. We restrict ourselves here...
Innocuous Constructor-Sharing Combinations (1997)
. We investigate conditions under which confluence and/or termination are preserved for constructor-sharing and hierarchical combinations of rewrite systems, one of which is left-linear and...
Problems in rewriting III (1995)
Nachum Dershowitz, Jean-pierre Jouannaud, Jan Willem Klop
We presented lists of open problems in the theory of rewriting in the proceedings of the previous two conferences [36; 37]. We continue with that tradition this year. We give references to solutions...
33 examples of termination (1995)
Abstract. A graded sequence of examples|presented in a uniform framework|spotlights stages in the development of methods for proving termination of rewrite systems. Let T be the set of all terms over...
Goal solving as operational semantics (1995)
To combine a functional or equational programming style with logic programming, one can use an underlying logic of Horn clauses with equality (as an interpreted predicate symbol) and (typed) terms....
Abstract. From a practical perspective, it is important for programs to have modular correctness properties. Some (largely syntactic) su cient conditions are given here for the union of terminating...
Problems in Rewriting III (1995)
Nachum Dershowitz, Jean-pierre Jouannaud, Jan Willem Klop
Introduction We presented lists of open problems in the theory of rewriting in the proceedings of the previous two conferences [ 36; 37 ] . We continue with that tradition this year. We give...
Problems in Rewriting III (1995)
Nachum Dershowitz, Jan Willem Klop
Introduction We presented lists of open problems in the theory of rewriting in the proceedings of the previous two conferences [ 36; 37 ] . We continue with that tradition this year. We give...
Goal Solving as Operational Semantics (1995)
To combine a functional or equational programming style with logic programming, one can use an underlying logic of Horn clauses with equality (as an interpreted predicate symbol) and (typed) terms....
33 Examples of Termination (1995)
. A graded sequence of examples---presented in a uniform framework---spotlights stages in the development of methods for proving termination of rewrite systems. Let T be the set of all terms over...
Nachum Dershowitz, Charles Hoot
. Two techniques are examined for showing termination of rewrite systems when simplification ordering are insufficient. The first approach generalizes the various path orderings and the conditions...
Hierarchical Termination (1995)
From a practical perspective, it is important for programs to have modular correctness properties. Some (largely syntactic) sufficient conditions are given here for the union of terminating rewrite...
Equational inference, canonical proofs, and proof orderings (1994)
Leo Bachmair, Nachum Dershowitz
We describe the application of proof orderings|a technique for reasoning about inference systems|to various rewrite-based theorem-proving methods, including re nements of the standard Knuth-Bendix...
More problems in rewriting (1993)
Nachum Dershowitz, Jean-pierre Jouannaud, Jan Willem Klop
Two years ago, in the proceedings of the previous conference, we presented a list of open problems in the theory of rewriting [Dershowitz et al., 1991a]. This time, we report on progress made during...
Deductive and Inductive Synthesis of Equational Programs (1993)
Nachum Dershowitz, Uday S. Reddy
An equational approach to the synthesis of functional and logic program is taken. Typically, the synthesis task involves nding equations which make the given speci cation an inductive theorem....
Yuh-jeng Lee, Nachum Dershowitz
Logic programming o ers a distinctive feature that is rarely met by other traditional programming languages: namely, one can use logic for both speci cation and computation. We present a methodology...
Deductive and Inductive Synthesis of Equational Programs (1993)
An equational approach to the synthesis of functional and logic programs is taken. Typically, a target program contains equations that are only true in the standard model of the given domain rules....
Calendrical Calculations, II: Three Historical Calendars (1993)
Edward Reingold, Nachum Dershowitz, Stewart M. Clamen, French Revolutionary, Old Hindu
this paper, we treat similarly three calendars of historical interest: the Mayan, French Revolutionary (le calendrier r'epublicain), and Old Hindu calendars. We follow the same conventions as in...
More Problems in Rewriting (1993)
Nachum Dershowitz, Jean-Pierre Jouannaud, Jan Willem Klop
Introduction Two years ago, in the proceedings of the previous conference, we presented a list of open problems in the theory of rewriting [ Dershowitz et al., 1991a ] . This time, we report on...
A Taste of Rewrite Systems (1993)
. This survey of the theory and applications of rewriting with equations discusses the existence and uniqueness of normal forms, the Knuth-Bendix completion procedure and its variations, as well as...
Nachum Dershowitz, D. N. Jayasimha
Bounded fairness, a stronger notion than the usual fairness based on eventuality, can be used, for example, to relate the frequency of shared resource access of a particular process with regard to...
Yuh-jeng Lee, Nachum Dershowitz
this paper, user input is shown in bold face and system generated output is shown in typewriter type font):
Ordinal Arithmetic with List Structures (1992)
Nachum Dershowitz, Edward M. Reingold
We provide a set of "natural" requirements for well-orderings of (binary) list structures. We show that the resultant order-type is the successor of the first critical epsilon number. The...
Decidable Matching for Convergent Systems (1992)
Nachum Dershowitz, Subrata Mitra, G. Sivakumar
We describe decision procedures for certain classes of semantic matching problems, where the equational theory with respect to which the semantic matching is performed has a convergent rewrite...
Rewriting Methods for Word Problems (1992)
This paper outlines various recent approaches to solving word problems. Term orderings are used to define a terminating rewrite relation. When confluent, that relation defines unique normal forms...
Equational Inference, Canonical Proofs, And Proof Orderings (1992)
Leo Bachmair, Nachum Dershowitz
We describe the application of proof orderings---a technique for reasoning about inference systems---to various rewrite-based theorem-proving methods, including refinements of the standard...
Deductive and Inductive Synthesis of Equational Programs (1992)
Nachum Dershowitz, Uday S. Reddy
An equational approach to the synthesis of functional and logic program is taken. Typically, the synthesis task involves finding equations which make the given specification an inductive theorem. To...
Path orderings for termination of associative-commutative rewriting (1992)
Nachum Dershowitz, Subrata Mitra
We show that a simple, and easily implementable, restriction on the recursive path ordering, which we call the "binary path condition, " suffices for establishing termination of extended...
Ordering-Based Strategies for Horn Clauses (1991)
Two new theorem-proving procedures for equational Horn clauses are presented. The largest literal is selected for paramodulation in both strategies, except that one method treats positive literals as...
Open Problems in Rewriting (1991)
Nachum Dershowitz, Jean-pierre Jouannaud, Jan Willem Klop
Introduction Interest in the theory and applications of rewriting has been growing rapidly, as evidenced in part by four conference proceedings (including this one) [15, 26, 41, 66]; three workshop...
A maximal-literal unit strategy for Horn clauses (1991)
A new positive-unit theorem-proving procedure for equational Horn clauses is presented. It uses a term ordering to restrict paxamodulation to potentially maximal sides of equations. Completeness is...
Canonical Sets of Horn Clauses (1990)
F27.09> s !R t (or just s ! t) stands for one replacement according to the orientation of a rewrite rule (in R); s ! t, for any number (including zero) of rewrites; s $ t also stands for one...
A Parallel Implementation of Equational Programming (1990)
Nachum Dershowitz, Naomi Lindenstrauss
A parallel implementation of rewriting and narrowing is described. This implementation is written in Flat Concurrent Prolog (FCP), but may be coded in any system in which processes are capable of...
Nachum Dershowitz, Jean-Pierre Jouannaud
Completion Completion has recently been put in a more abstract framework [ Bachmair-et al, 1986 ] , an approach we adopt here. As in traditional proof theory (cf. [ Takeuti, 1987 ] ), proofs are...
Inductive Synthesis of Equational Programs (1990)
Nachum Dershowitz, Eli Pinchover
An equational approach to the synthesis of functional and logic programs is taken. Typically, a target program contains equations that are only true in the standard model of the given domain rules....
Rewriting methods for word problems (1990)
This paper outlines various recent approaches to solving word problems. Term orderings are used to de ne a terminating rewrite relation. When con uent, that relation de nes unique normal forms that...
Completion without Failure (1989)
Leo Bachmair, Nachum Dershowitz, David A. Plaisted
. We present an "unfailing" extension of the standard KnuthBendix completion procedure that is guaranteed to produce a desired canonical system, provided certain conditions are met. We...
Rewrite, Rewrite, Rewrite, Rewrite, Rewrite, ... (1989)
Nachum Dershowitz, David A. Plaisted
. We study properties of rewrite systems that are not necessarily terminating, but allow instead for transfinite derivations that have a limit. In particular, we give conditions for the existence of...
Average Time Analyses Related to Logic Programming (1989)
Nachum Dershowitz, Naomi Lindenstrauss
Logic programs are known to be amenable to parallelization. Our work is an attempt to quantify the magnitude of speed-up one can expect from parallel execution of a logic program. To make average...
North-Holland PATTERNS IN TREES* (1988)
We give a general formula for the number of occurrences of a pattern, or set of patterns, in the class of ordered (plane-planted) trees with a given number of edges. The proof is com-binatorial. Many...
Completion for rewriting modulo a congruence (1988)
Leo Bachmair, Nachum Dershowitz
Abstract. We present completion methods for rewriting modulo a congruence, generalizing previous methods by Peterson and Stickel (1981) and Jouannaud and Kirchner (1986). We formalize our methods as...
Nachum Dershowitz, D. N. Jayasimha
Bounded fairness, a stronger notion than the usual fairness based on eventuality, can be used, for example, to relate the frequency of shared resource access of a particular process with regard to...
Nachum Dershowitz, D. N. Jayasimha, Seungjoon Park, Zohar Manna
Dedicated with boundless gratitude to
Rewrite Methods for Clausal and Nonclausal Theorem Proving (1983)
Jieh Hsiang, Nachum Dershowitz
Effective theorem provers are essential for automatic verification and generation of programs. The conventional resolution strategies, albeit complete, are inefficient. On the other hand, special...