Nachum Dershowitz

FLAP Journal 2025 Journal Article

What’s Logic?

• Nachum Dershowitz

AAAI Conference 2021 Conference Paper

Computational Visual Ceramicology: Matching Image Outlines to Catalog Sketches

• Barak Itkin
• Lior Wolf
• Nachum Dershowitz

Field archeologists are called upon to identify potsherds, for which they rely on their professional experience and on reference works. We have developed a recognition method starting from images captured on site, which relies on the shape of the sherd’s fracture outline. The method sets up a new target for deep-learning, integrating information from points along inner and outer surfaces to learn about shapes. Training the classifiers required tackling multiple challenges that arose on account of our working with real-world archeological data: paucity of labeled data; extreme imbalance between instances of different categories; and the need to avoid neglecting rare classes and to take note of minute distinguishing features of some classes. The scarcity of training data was overcome by using synthetically-produced virtual potsherds and by employing multiple data-augmentation techniques. A novel form of training loss allowed us to overcome classification problems caused by under-populated classes and inhomogeneous distribution of discriminative features.

STOC Conference 2021 Conference Paper

The communication complexity of multiparty set disjointness under product distributions

• Nachum Dershowitz
• Rotem Oshman
• Tal Roth

In the multiparty number-in-hand set disjointness problem, we have k players, with private inputs X 1 ,…, X k ⊆ [ n ]. The players’ goal is to check whether ∩ ℓ=1 k X ℓ = ∅. It is known that in the shared blackboard model of communication, set disjointness requires Ω( n log k + k ) bits of communication, and in the coordinator model, it requires Ω( kn ) bits. However, these two lower bounds require that the players’ inputs can be highly correlated. We study the communication complexity of multiparty set disjointness under product distributions, and ask whether the problem becomes significantly easier, as it is known to become in the two-party case. Our main result is a nearly-tight bound of Θ ̃ ( n 1−1/ k + k ) for both the shared blackboard model and the coordinator model. This shows that in the shared blackboard model, as the number of players grows, having independent inputs helps less and less; but in the coordinator model, when k is very large, having independent inputs makes the problem much easier. Both our upper and our lower bounds use new ideas, as the original techniques developed for the two-party case do not scale to more than two players.

TCS Journal 2019 Journal Article

Drags: A compositional algebraic framework for graph rewriting

• Nachum Dershowitz
• Jean-Pierre Jouannaud

We are interested in a natural generalization of term-rewriting techniques to what we call drags, viz. finite, directed, ordered, rooted multigraphs, each vertex of which is labeled by a function symbol. To this end, we develop a rich algebra of drags that generalizes the familiar term algebra and its associated rewriting capabilities. Viewing graphs as terms provides an initial building block for rewriting with such graphs, one that should impact the many areas where computations take place on graphs.

LPAR Conference 2018 Conference Paper

Graph Path Orderings

• Nachum Dershowitz
• Jean-Pierre Jouannaud

We define well-founded rewrite orderings on graphs and show that they can be used to show termination of a set of graph rewrite rules by verifying all their cyclic extensions. We then introduce the graph path ordering inspired by the recursive path ordering on terms and show that it is a well-founded rewrite ordering on graphs for which checking termination of a finite set of graph rewrite rules is decidable. Our ordering applies to arbitrary finite, directed, labeled, ordered multigraphs, hence provides a building block for rewriting with graphs, which should impact the many areas in which computations take place on graphs.

SAT Conference 2015 Conference Paper

Hints Revealed

• Jonathan Kalechstain
• Vadim Ryvchin
• Nachum Dershowitz

Abstract We propose a notion of hints, clauses that are not necessarily consistent with the input formula. The goal of adding hints is to speed up the SAT solving process. For this purpose, we provide an efficient general mechanism for hint addition and removal. When a hint is determined to be inconsistent, a hint-based partial resolution-graph of an unsatisfiable core is used to reduce the search space. The suggested mechanism is used to boost performance by adding generated hints to the input formula. We describe two specific hint-suggestion methods, one of which increases performance by 30% on satisfiable SAT ’13 competition instances and solves 9 instances not solved by the baseline solver.

CSL Conference 2013 Conference Paper

Res Publica: The Universal Model of Computation (Invited Talk)

• Nachum Dershowitz

We proffer a model of computation that encompasses a broad variety of contemporary generic models, such as cellular automata---including dynamic ones, and abstract state machines---incorporating, as they do, interaction and parallelism. We ponder what it means for such an intertwined system to be effective and note that the suggested framework is ideal for representing continuous-time and asynchronous systems.

TCS Journal 2012 Journal Article

Jumping and escaping: Modular termination and the abstract path ordering

• Nachum Dershowitz

Combinatorial commutation properties for reordering a sequence consisting of two kinds of steps, and for separating the well-foundedness of their combination into well-foundedness of each, are investigated. A weak commutation property, called “jumping”, along with a weakened version of the lifting property, called “escaping” and requiring only an eventual lifting, are used for proving well-foundedness of a generic, abstract version of the recursive path orderings.

CSL Conference 2010 Conference Paper

Exact Exploration and Hanging Algorithms

• Andreas Blass
• Nachum Dershowitz
• Yuri Gurevich

Abstract Recent analysis of sequential algorithms resulted in their axiomatization and in a representation theorem stating that, for any sequential algorithm, there is an abstract state machine (ASM) with the same states, initial states and state transitions. That analysis, however, abstracted from details of intra-step computation, and the ASM, produced in the proof of the representation theorem, may and often does explore parts of the state unexplored by the algorithm. We refine the analysis, the axiomatization and the representation theorem. Emulating a step of the given algorithm, the ASM, produced in the proof of the new representation theorem, explores exactly the part of the state explored by the algorithm. That frugality pays off when state exploration is costly. The algorithm may be a high-level specification, and a simple function call on the abstraction level of the algorithm may hide expensive interaction with the environment. Furthermore, the original analysis presumed that state functions are total. Now we allow state functions, including equality, to be partial so that a function call may cause the algorithm as well as the ASM to hang. Since the emulating ASM does not make any superfluous function calls, it hangs only if the algorithm does.

I&C Journal 2007 Journal Article

Leanest quasi-orderings

• 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. Unfortunately, a minimum in terms of set inclusion can be non-existent even when an intuitive “minimum” exists. We suggest an alternative to set inclusion, called “leanness”, show that leanness is a partial order on quasi-orderings, and provide sufficient conditions for the existence of a “leanest” member of a set of total well-founded quasi-orderings.

SAT Conference 2007 Conference Paper

Towards a Better Understanding of the Functionality of a Conflict-Driven SAT Solver

• Nachum Dershowitz
• Ziyad Hanna
• Alexander 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 learning schemes, like 1UIP or All UIP, depends on their ability to guide the solver towards refutations associated with compact decision trees. We propose an enhancement of 1UIP that is empirically helpful for real-world industrial benchmarks.

SAT Conference 2006 Conference Paper

A Scalable Algorithm for Minimal Unsatisfiable Core Extraction

• Nachum Dershowitz
• Ziyad Hanna
• Alexander 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 verification benchmarks confirming that our algorithm finds smaller cores than suboptimal algorithms; and that it runs faster than those algorithms that guarantee minimality of the core. (A more complete version of this paper may be found at arXiv. org/pdf/cs. LO/0605085.)

TCS Journal 2006 Journal Article

Abstract canonical presentations

• Nachum Dershowitz
• Claude Kirchner

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 called “completion processes”, in particular in the study of equational logic, involve finding appropriate presentations of a given theory to more easily solve a given class of problems. We provide a general proof-theoretic setting that relies directly on the fundamental concept of “good”, that is, normal-form, proofs, itself defined using well-founded orderings on proof objects. This foundational framework allows for abstract definitions of canonical presentations and very general characterizations of saturation and redundancy criteria.

LPAR Conference 2006 Conference Paper

Boolean Rings for Intersection-Based Satisfiability

• 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 representation for Boolean-ring polynomials with which one can easily apply Gaussian elimination and Horn-clause methods to advantage. We demonstrate that this framework, with its enhanced simplification, is especially amenable to intersection-based learning, as in recursive learning and the method of Stålmarck. Experiments support the idea that problem variables can be eliminated and search trees can be shrunk by incorporating learning in the form of Boolean-ring saturation.

SAT Conference 2005 Conference Paper

A Clause-Based Heuristic for SAT Solvers

• Nachum Dershowitz
• Ziyad Hanna
• Alexander 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 variable is chosen from the top-most unsatisfied clause. Various methods of initially organizing the list and moving the clauses within it are studied. Our approach is an extension of one used in Berkmin, and adopted by other modern solvers, according to which only conflict clauses are organized in a list, and a literal-scoring-based secondary heuristic is used when there are no more unsatisfied conflict clauses. Our approach, implemented in the 2004 version of zChaff solver and in a generic Chaff-based SAT solver, results in a significant performance boost on hard industrial benchmarks.

SAT Conference 2005 Conference Paper

Bounded Model Checking with QBF

• Nachum Dershowitz
• Ziyad Hanna
• Jacob Katz

Abstract Current algorithms for bounded model checking (BMC) use SAT methods for checking satisfiability of Boolean formulas. These BMC methods suffer from a potential memory explosion problem. Methods based on the validity of Quantified Boolean Formulas (QBF) allow an exponentially more succinct representation of the checked formulas, but have not been widely used, because of the lack of an efficient decision procedure for QBF. We evaluate the usage of QBF in BMC, using general-purpose SAT and QBF solvers. We also present a special-purpose decision procedure for QBF used in BMC, and compare our technique with the methods using general-purpose SAT and QBF solvers on real-life industrial benchmarks. Our procedure performs much better for BMC than the general-purpose QBF solvers, without incurring the space overhead of propositional SAT.

LPAR Conference 2005 Conference Paper

The Four Sons of Penrose

• Nachum Dershowitz

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 the question raised by the argument, skirting the issue of introspection per se.

SAT Conference 2004 Conference Paper

Boolean Ring Satisfiability

• Nachum Dershowitz
• Jieh Hsiang
• Guan-Shieng Huang
• Daher Kaiss

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 distributive law by employing a combined linear and binomial representation. Several complexity results suggest why the method may be relatively effective in many cases. The framework is also amenable to learning from intersections, as in Stålmarck’s method. Some experiments have been undertaken.

MFCS Conference 1997 Invited Paper

When are Two Rewrite Systems More than None?

• Nachum Dershowitz

Abstract It is important for programs to have modular correctness properties. We look at non-deterministic programs expressed as term-rewriting systems (which compute normal forms of input terms) and consider the case where individual systems share constructors, but not defined symbols. We present some old and new sufficient conditions under which termination (existence of normal forms, regardless of computation strategy) and confluence (uniqueness) are preserved by such combinations.

TCS Journal 1995 Journal Article

Natural termination

• Nachum Dershowitz
• Charles Hoot

Two techniques are examined for showing termination of rewrite systems when simplification orderings are insufficient. The first approach generalizes the various path orderings and the conditions under which they work. Examples of its use are given and a brief description of an implementation is presented. The second approach uses restricted derivations, called “forward closures”, for proving termination of orthogonal and overlaying systems. Both approaches allow the use of “natural” interpretations under which rules rewrite terms to terms of the same value.

TCS Journal 1991 Journal Article

Rewrite, rewrite, rewrite, rewrite, rewrite, …

• Nachum Dershowitz
• Stéphane Kaplan
• 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 a limit and for its uniqueness and relate the operational and algebraic semantics of infinitary theories. We also consider sufficient completeness of hierarchical systems.

TCS Journal 1990 Journal Article

A rationale for conditional equational programming

• Nachum Dershowitz
• Mitsuhiro Okada

Conditional equations provide a paradigm of computation that combines the clean syntax and semantics of LISP-like functional programming with Prolog-like logic programming in a uniform manner. For functional programming, equations are used as rules for left-to-right rewriting; for logic programming, the same rules are used for conditional narrowing. Together, rewriting and narrowing provide increased expressive power. We discuss some aspects of the theory of conditional rewriting, and the reasons underlying certain choices in designing a language based on them. The most important correctness property a conditional rewriting program may posses is ground confluence; this ensures that at most one value can be computed from any given (variable-free) input term. We give criteria for confluence. Reasonable conditions for ensuring the completeness of narrowing as an operational mechanism for solving goals are provided; these results are then extended to handle rewriting with existentially quantified conditions and built-in predicates. Some termination issues are also considered, including the case of rewriting with higher-order terms.

AAAI Conference 1990 Conference Paper

Inductive Synthesis of Equational Programs

• Nachum Dershowitz

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. To synthesize such programs, induction is necessary. We propose heuristics for generalizing from a sequence of deductive consequences. These are combined with rewrite-based methods of inductive proof to derive provably correct programs. a survey of rewriting, see (Dershowitz & Jouannaud 1990); for completion and its applications, see (Dershowitz 1989). Consider the following toy system S for addition and doubling (d) of natural numbers in unary notation: x+0 + x x + S(Y) + s(x+y) d(x) + x+x

TCS Journal 1989 Journal Article

Completion for rewriting modulo a congruence

• Leo Bachmair
• Nachum Dershowitz

Completion modulo a congruence is a method for constructing a presentation of an equational theory as a rewrite system that defines unique normal forms with respect to the congruence. We formulate this completion method as an equational inference system and present techniques for proving the correctness of procedures based on the inference system. Our correctness results cover generalized and improved versions of the Peterson-Stickel and the Jouannaud-Kirchner procedure.

AAAI Conference 1988 Conference Paper

Goal-Directed Equation Solving

• Nachum Dershowitz

IJCAI Conference 1985 Conference Paper

Synthesis by Completion

• Nachum Dershowitz

AIJ Journal 1985 Journal Article

Synthetic programming

• Nachum Dershowitz

Given a formal specification for a desired program, our goal is to transform it step-by-step into executable code. We proceed in a top-down fashion—as suggested by ‘structured programming’ methodology. Each step consists of applying a synthesis rule to rewrite a segment of the developing program in increased detail. If every step is transparent enough to ensure correctness, each partial program in the series is sure to be equivalent to its predecessor. In particular, the final program is guaranteed to satisfy the initial specifications. In this paper, we concentrate on automatable strategies for the formation of iterative loops, giving rules based on ‘invariant assertions’ and on ‘subgoal assertions’.

IJCAI Conference 1983 Conference Paper

Associative-Commutative Rewriting

• Nachum Dershowitz
• Jien Hsiang
• N. Alan Josephson
• David A. Plaisted

TCS Journal 1982 Journal Article

Orderings for term-rewriting systems

• Nachum Dershowitz

Methods of proving that a term-rewriting system terminates are presented. They are based on the intuitive notion of ‘simplification orderings’, orderings in which any term that is syntactically simpler than another is smaller than the other. As a consequence of Kruskal's Tree Theorem, any nonterminating system must be self-embedding in the sense that it allows for the derivation of some term from a simpler one; thus termination is guaranteed if every rule in the system is a reduction in some simplification ordering. Most of the orderings that have been used for proving termination are indeed simplication orderings; using this notion often allows for much easier proofs. A particularly useful class of simplification orderings, the ‘recursive path orderings’, is defined. Examples of the use of simplication orderings in termination proofs are given.

FOCS Conference 1979 Conference Paper

Orderings for Term-Rewriting Systems

• Nachum Dershowitz

Methods of proving that a term-rewriting system terminates are presented. They are based on the notion of "simplification orderings", orderings in which any term that is homeomorphically embeddable in another is smaller than the other. A particularly useful class of simplification orderings, the "recursive path orderings", is defined. Several examples of the use of such orderings in termination proofs are given.