Searcharxiv⌕ Search

arXiv subjects

Nachum Dershowitz

Publications and source records attributed to Nachum Dershowitz.

At least 37 records · Page 2Linked to original sources

Computational Ceramicology

Field archeologists are called upon to identify potsherds, for which purpose they rely on their experience and on reference works. We have developed two complementary machine-learning tools to propose identifications based on images captured on site. One method relies on the shape of the fracture outline of a sherd; the other is based on decorative features. For the outline-identification tool, a novel deep-learning architecture was employed, one that integrates shape information from points along the inner and outer surfaces. The decoration classifier is based on relatively standard architectures used in image recognition. In both cases, training the classifiers required tackling challenges that arise when working with real-world archeological data: paucity of labeled data; extreme imbalance between instances of the 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 the problems caused by under-populated classes and non-homogeneous distribution of discriminative features.

cs.CV↗

Nonleaf Patterns in Trees: Protected Nodes and Fine Numbers

A closed-form formula is derived for the number of occurrences of matches of a multiset of patterns among all ordered (plane-planted) trees with a given number of edges. A pattern looks like a tree, with internal nodes and leaves, but also contain components that match subtrees or sequences of subtrees. This result extends previous versatile tree-pattern enumeration formulae to incorporate components that are only allowed to match nonleaf subtrees and provides enumerations of trees by the number of protected (shortest outgoing path has two or more edges) or unprotected nodes.

cs.DM↗

Semantic Characteristics of Schizophrenic Speech

Natural language processing tools are used to automatically detect disturbances in transcribed speech of schizophrenia inpatients who speak Hebrew. We measure topic mutation over time and show that controls maintain more cohesive speech than inpatients. We also examine differences in how inpatients and controls use adjectives and adverbs to describe content words and show that the ones used by controls are more common than the those of inpatients. We provide experimental results and show their potential for automatically detecting schizophrenia in patients by means only of their speech patterns.

cs.CL↗

A Hackathon for Classical Tibetan

We describe the course of a hackathon dedicated to the development of linguistic tools for Tibetan Buddhist studies. Over a period of five days, a group of seventeen scholars, scientists, and students developed and compared algorithms for intertextual alignment and text classification, along with some basic language tools, including a stemmer and word segmenter.

cs.CL↗

Touchard's Drunkard

Based on Touchard's identity, a simple derivation is given for the enumeration of the N/S/E/W walks that remain on the north side of the origin.

cs.DM↗

1700 Forests

Since ordered trees and Dyck paths are equinumerous, so are ordered forests and grand-Dyck paths that start with an upwards step.

cs.DM↗

Tripartite Unions

This note provides conditions under which the union of three well-founded binary relations is also well-founded.

cs.LO↗

Axiomatizing Analog Algorithms

We propose a formalization of generic algorithms that includes analog algorithms. This is achieved by reformulating and extending the framework of abstract state machines to include continuous-time models of computation. We prove that every hybrid algorithm satisfying some reasonable postulates may be expressed precisely by a program in a simple and expressive language.

cs.LO↗

Cellular Automata are Generic

Any algorithm (in the sense of Gurevich's abstract-state-machine axiomatization of classical algorithms) operating over any arbitrary unordered domain can be simulated by a dynamic cellular automaton, that is, by a pattern-directed cellular automaton with unconstrained topology and with the power to create new cells. The advantage is that the latter is closer to physical reality. The overhead of our simulation is quadratic.

cs.LO↗

The Generic Model of Computation

Over the past two decades, Yuri Gurevich and his colleagues have formulated axiomatic foundations for the notion of algorithm, be it classical, interactive, or parallel, and formalized them in the new generic framework of abstract state machines. This approach has recently been extended to suggest a formalization of the notion of effective computation over arbitrary countable domains. The central notions are summarized herein.

cs.LO↗

From Total Assignment Enumeration to Modern SAT Solver

A new framework for presenting and analyzing the functionality of a modern DLL-based SAT solver is proposed. Our approach exploits the inherent relation between backtracking and resolution. We show how to derive the algorithm of a modern SAT solver from DLL step-by-step. We analyze the inference power of Boolean Constraint Propagation, Non-Chronological Backtracking and 1UIP-based Conflict-Directed Backjumping. Our work can serve as an introduction to a modern SAT solver functionality and as a basis for future work on the inference power of a modern SAT solver and on practical SAT solver design.

cs.LO↗

When are two algorithms the same?

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 a suitable equivalence relation. We argue that no such equivalence relation exists.

cs.GL↗

Enumeration Problems Related to Ground Horn Theories

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 of different theories in $n$ variables for slightly different characterizations. The method of counting is via counting models using a satisfiability checker.

cs.LO↗

Space-Efficient Bounded Model Checking

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 validity of Quantified Boolean Formulae (QBF) allow an exponentially more succinct representation of formulae to be checked, because no "unrolling" of the transition relation is required. These methods have not been widely used, because of the lack of an efficient decision procedure for QBF. We evaluate the usage of QBF in bounded model checking (BMC), using general-purpose SAT and QBF solvers. We develop 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.

cs.LO↗

Complexity of Propositional Proofs under a Promise

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 assignments, where ``many'' stands for an explicitly specified function $\Lam$ in the number of variables $n$. To this end, we develop propositional proof systems under different measures of promises (that is, different $\Lam$) as extensions of resolution. This is done by augmenting resolution with axioms that, roughly, can eliminate sets of truth assignments defined by Boolean circuits. We then investigate the complexity of such systems, obtaining an exponential separation in the average-case between resolution under different size promises: 1. Resolution has polynomial-size refutations for all unsatisfiable 3CNF formulas when the promise is $\eps\cd2^n$, for any constant $0<\eps<1$. 2. There are no sub-exponential size resolution refutations for random 3CNF formulas, when the promise is $2^{δn}$ (and the number of clauses is $o(n^{3/2})$), for any constant $0<δ<1$.

cs.CC↗

Abstract Canonical Inference

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, saturation, redundancy elimination, and rewrite-system reduction are connected to proof orderings. Fairness of deductive mechanisms is defined in terms of proof orderings, distinguishing between (ordinary) "fairness," which yields completeness, and "uniform fairness," which yields saturation.

cs.LO↗