Abstract The discovery of the Dead Sea Scrolls over sixty years ago is widely regarded as one of the greatest archaeological breakthroughs in modern history. Recent study of the scrolls presents ongoing computational challenges, including determining the provenance of fragments, clustering fragments based on their degree of similarity, and pairing fragments that originate from the same manuscript—all tasks that require focusing on individual letter and fragment shapes. This paper presents a computational method for segmenting ink and parchment regions in multispectral images of Dead Sea Scroll fragments. Using the newly developed Qumran Segmentation Dataset (QSD) consisting of 20 fragments, we apply multispectral thresholding to isolate ink and parchment regions based on their unique spectral signatures. To refine segmentation accuracy, we introduce an energy minimization technique that leverages ink contours, which are more distinguishable from the background and less noisy than inner ink regions. Experimental results demonstrate that this Multispectral Thresholding and Energy Minimization (MTEM) method achieves significant improvements over traditional binarization approaches like Otsu and Sauvola in parchment segmentation and is successful at delineating ink borders, in distinction from holes and background regions.

The digital era has made millions of manuscript images in Hebrew available to all. However, despite major advancements in handwritten text recognition over the past decade, an efficient pipeline for large scale and accurate conversion of these manuscripts into useful machine-readable form is still sorely lacking.We propose a pipeline that significantly improves recognition models for automatic transcription of Hebrew manuscripts. Transfer learning is used to fine-tune pretrained models. For post-recognition correction, it leverages text reuse, a common phenomenon in medieval manuscripts, and state-of-the-art large language models for medieval Hebrew.The framework successfully handles noisy transcriptions and consistently suggests alternate, better readings. Initial results show that word level accuracy increased by 10% for new readings proposed by text-reuse detection. Moreover, the character level accuracy improved by 18% by fine-tuning models on the first few pages of each manuscript.

Abstract We suggest a model for partial diacritization of deep orthographies. We focus on Arabic, where the optional indication of selected vowels by means of diacritics can resolve ambiguity and improve readability. Our partial diacritizer restores short vowels only when they contribute to the ease of understandability during reading a given running text. The idea is to identify those uncertainties of absent vowels that require the reader to look ahead to disambiguate. To achieve this, two independent neural networks are used for predicting diacritics, one that takes the entire sentence as input and another that considers only the text that has been read thus far. Partial diacritization is then determined by retaining precisely those vowels on which the two networks disagree, preferring the reading based on consideration of the whole sentence over the more naïve reading-order diacritization. For evaluation, we prepared a new dataset of Arabic texts with both full and partial vowelization. In addition to facilitating readability, we find that our partial diacritizer improves translation quality compared either to their total absence or to random selection. Lastly, we study the benefit of knowing the text that follows the word in focus toward the restoration of short vowels during reading, and we measure the degree to which lookahead contributes to resolving ambiguities encountered while reading. L’Herbelot had asserted, that the most ancient Korans, written in the Cufic character, had no vowel points; and that these were first invented by Jahia–ben Jamer, who died in the 127th year of the Hegira. “Toderini’s History of Turkish Literature,” Analytical Review (1789)

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.

In the multiparty number-in-hand set disjointness problem, we have k players, with private inputs X1,…,Xk ⊆ [n]. The players’ goal is to check whether ∩ℓ=1k Xℓ = ∅. It is known that in the shared blackboard model of communication, set disjointness requires Ω(n logk + 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 Θ̃(n1−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.

Most of the Dead Sea Scrolls have now been digitally transcribed and imaged to very high standards. Our goal is to align the transcriptions with the text visible in the image, glyph by (often fragmentary) glyph. This involves several tasks, normally considered in isolation: (A) Baseline segmentation. (B) Line polygon extraction. (C) Automated transcription by handwritten character recognition, to aid in alignment. (D) Alignment of the Unicode characters in a line transcription with the characters in the image of that line. The task is frustrated by the degraded nature of the frequently very small and/or warped fragments with many broken letters, substantially different allographs, ligatures, and scribal idiosyncrasies. Furthermore, a great number of inconsistencies between current cataloguing systems for the data need to be resolved. For each task, we apply state-of-the-art machine-learning methods in addition to more traditional techniques, each presenting significant difficulties on account of the poor state of most fragments' preservation. We have built ground-truth datasets and have managed to achieve good results with well-preserved fragments by leveraging heavily augmented transfer learning from prior work with medieval manuscripts.

We examine the use case of performing handwritten character recognition (HCR) on a newly compiled collection of Tibetan historical documents, which presents multiple challenges, including inherent challenges such as image quality and the lack of word separation, and dataset challenges such as a lack of supervised training data. To tackle these challenges, we introduce an end-to-end unsupervised full-document HCR approach composed of unsupervised line segmentation and a convolutional recurrent neural network, trained using solely synthetic data. Various augmentations are applied to these synthesized images, and we compare the effect of each augmentation on the HCR results. Since we work on a collection of historical manuscripts, we can fit the model to the available test data. During training, our network has access to both the labeled synthetic training data and the unlabeled images of the test set, and we adapt and evaluate four different semi-supervised learning and domain adaptation approaches for transductive learning in HCR. We test our approach on a set of 167 images from the "Kadam" collection, containing 829 lines. We show that correct data augmentation is crucial for the success of HCR trained solely on synthetic data and that using an effective transductive learning approach drastically improves results.

news Free Access Share on Zohar Manna (1939–2018) Authors: Nachum Dershowitz School of Computer Science, Tel Aviv University, Tel Aviv-Yafo, Israel School of Computer Science, Tel Aviv University, Tel Aviv-Yafo, IsraelSearch about this author , Richard Waldinger Artificial Intelligence Center, SRI International, Menlo Park, CA, USA Artificial Intelligence Center, SRI International, Menlo Park, CA, USASearch about this author Authors Info & Claims Formal Aspects of ComputingVolume 31Issue 6Dec 2019 pp 643–660https://doi.org/10.1007/s00165-019-00500-4Published:01 December 2019Publication History 1citation58DownloadsMetricsTotal Citations1Total Downloads58Last 12 Months49Last 6 weeks2 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

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.

The Dead Sea Scrolls are of great historical significance. Lamentably, in the decades since their discovery, many fragments have deteriorated. Fortunately, low-resolution grayscale infrared images of the Palestinian Archaeological Museum plates holding the scrolls in their discovered state are extant, along with recent high-quality multispectral images by the Israel Antiquities Authority. However, the necessary task of identifying each fragment in the new images on the old plates is tedious and time consuming to perform manually, and is often problematic when fragments have been moved from the original plate. We describe an automated system that segments the new and old images of fragments from the background on which they were imaged, finds their matches on the old plates and aligns and superimposes them. To this end, we developed a deep-learning based segmentation method and a cascade approach for template matching, based on scale, shape analysis and dense matching. We have tested the proposed method on five plates, comprising about 120 fragments. We present both quantitative and qualitative analyses of the results and perform an ablation study to evaluate the importance of each component of our system.

We describe an automated pipeline for digitization of catalog drawings of pottery types. This work is aimed at extracting a structured description of the main geometric features and a 3D representation of each class. The pipeline includes methods for understanding a 2D drawing and using it for constructing a 3D model of the pottery. These will be used to populate a reference database for classification of potsherds. Furthermore, we extend the pipeline with methods for breaking the 3D model to obtain synthetic sherds and methods for capturing images of these sherds in a way that matches the imaging methodology of archaeologists. These will serve to build a massive set of synthetic sherd images that will help train and test future automated classification systems.

Historical documents have been undergoing large-scale digitization over the past years, placing massive image collections online. Optical character recognition (OCR) often performs poorly on such material, which makes searching within these resources problematic and textual analysis of such documents difficult. We present two approaches to overcome this obstacle, one textual and one visual. We show that, for tasks like finding newspaper articles related by topic, poor-quality OCR text suffices. An ordinary vector-space model is used to represent articles. Additional improvements obtain by adding words with similar distributional representations. As an alternative to OCR-based methods, one can perform image-based search, using word spotting. Synthetic images are generated for every word in a lexicon, and word-spotting is used to compile vectors of their occurrences. Retrieval is by means of a usual nearest-neighbor search. The results of this visual approach are comparable to those obtained using noisy OCR. We report on experiments applying both methods, separately and together, on historical Hebrew newspapers, with their added problem of rich morphology.

The task of restoring fragmentary letters is fundamental to the reading of ancient manuscripts. We present a method to complete broken letters in the Dead Sea Scrolls, which is based on PixelCNN++. Since the generation of the broken letters is conditioned on the extant scroll, we modify the original method to allow reconstructions in multiple directions. Results on both simulated data and real scrolls demonstrate the advantage of our method over the baseline. The implementation may be found at https://github.com/ghostcow/pixel-cnn-qumran.

This paper explores the use of a learned classifier for post-OCR text correction. Experiments with the Arabic language show that this approach, which integrates a weighted confusion matrix and a shallow language model, improves the vast majority of segmentation and recognition errors, the most frequent types of error on our dataset.

Turing, in his immortal 1936 paper, observed that ‘[human] computing is normally done by writing… symbols on [two-dimensional] paper’, but noted that use of a second dimension ‘is always avoidable’ and that ‘the two-dimensional character of paper is no essential of computation’. We propose to promote two-dimensional models of computation and exploit the naturalness of two-dimensional representations of data. In particular, programs for a two-dimensional Turing machine can be recorded most naturally on its own two-dimensional input–output grid in such a transparent fashion that schoolchildren would have no difficulty comprehending their behaviour. This two-dimensional rendering allows, furthermore, for a most perspicacious rendering of Turing’s universal machine.

We present an end-to-end system for aligning transcript letters to their coordinates in a manuscript image. An intuitive GUI and an automatic line detection method enable the user to perform an exact alignment of parts of document pages. In order to bridge large regions in between annotation, and augment the manual effort, the system employs an optical-flow engine for directly matching at the pixel level the image of a line of a historical text with a synthetic image created from the transcript's matching line. Meanwhile, by accumulating aligned letters, and performing letter spotting, the system is able to bootstrap a rapid semi-automatic transcription of the remaining text. Thus, the amount of manual work is greatly diminished and the transcript alignment task becomes practical regardless of the corpus size.

Optical character recognition (OCR) quality, especially for under-resourced scripts like Bangla, as well as for documents printed in old typefaces, is a major concern. An efficient and effective pipeline for OCR betterment is proposed here. The method is unsupervised. It employs a baseline OCR engine as a black box plus a dataset of unlabeled document images. That engine is applied to the images, followed by a visual encoding designed to support efficient word spotting. Given a new document to be analyzed, the black-box recognition engine is first applied. Then, for each result, word spotting is carried out within the dataset. The unreliable OCR outputs of the retrieved word spotting results are then considered. The word that is the centroid of the set of OCR words, measured by edit distance, is deemed a candidate reading.

We present a tool for re-ranking the results of a specific query by considering the (n+1) × (n+1) matrix of pairwise similarities among the elements of the set of n retrieved results and the query itself. The re-ranking thus makes use of the similarities between the various results and does not employ additional sources of information. The tool is based on graphical Bayesian models, which reinforce retrieved items strongly linked to other retrievals, and on repeated clustering to measure the stability of the obtained associations. The utility of the tool is demonstrated within the context of visual search of documents from the Cairo Genizah and for retrieval of paintings by the same artist and in the same style.

A simple and efficient pipeline for word spotting in handwritten documents is proposed. The method allows for extremely rapid querying, while still maintaining high accuracy. The dataset images that are to be queried are preprocessed by a simple binarization operation, followed by the extraction of multiple overlapping candidate targets. Each binary target, as well as the binarized query, is resized to fit a fixed-size rectangle and represented by conventional image descriptors. Then, a cosine similarity operator -- followed by maximum pooling over random groups -- is used to represent each target or query as a concise 250D vector. Retrieval is performed in a fraction of a second by nearest-neighbor search within that space, followed by a simple suppression of extra overlapping candidates.

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.

Recent large-scale digitization and preservation efforts have made images of original manuscripts, accompanied by transcripts, commonly available. An important challenge, for which no practical system exists, is that of aligning transcript letters to their coordinates in manuscript images. Here we propose a system that directly matches the image of a historical text with a synthetic image created from the transcript for the purpose. This, rather than attempting to recognize individual letters in the manuscript image using optical character recognition (OCR). Our method matches the pixels of the two images by employing a dedicated dense flow mechanism coupled with novel local image descriptors designed to spatially integrate local patch similarities. Matching these pixel representations is performed using a message passing algorithm. The various stages of our method make it robust with respect to document degradation, to variations between script styles and to non-linear image transformations. Robustness, as well as practicality of the system, are verified by comprehensive empirical experiments.

The Dead Sea Scrolls were discovered in the Qumran area and elsewhere in the Judean desert beginning in 1947 and were photographed in infrared in the 1950s. Recently, the Israel Antiquities Authority embarked on an ambitious project to digitize all the fragments using multi-spectral cameras. We describe a method that utilizes information from both of these image sets: the highly detailed multispectral images and the older infrared images, which preserve the state of the fragments as it was shortly after discovery. We use a two-step registration procedure to align the image sets. First, a coarse global transformation is applied to the whole image of the new set, producing a rough alignment, followed by a fine, local wrapping based on interest point matching. The aligned images can be used to improve image binarization and to identify and repair fragments that have degraded further over the years. Additionally, the fine alignment parameters can be used for coarse attribute classification, such as the period when written.

Many significant historical corpora contain leaves that are mixed up and no longer bound in their original state as multi-page documents. The reconstruction of old manuscripts from a mix of disjoint leaves can therefore be of paramount importance to historians and literary scholars. Previously, it was shown that visual similarity provides meaningful pair-wise similarities between handwritten leaves. Here, we go a step further and suggest a semiautomatic clustering tool that helps reconstruct the original documents. The proposed solution is based on a graphical model that makes inferences based on catalog information provided for each leaf as well as on the pairwise similarities of handwriting. Several novel active clustering techniques are explored, and the solution is applied to a significant part of the Cairo Genizah, where the problem of joining leaves remains unsolved even after a century of extensive study by hundreds of scholars.

The Digital Age has brought with it large-scale digitization of historical records. The modern scholar of history or of other disciplines is often faced today with hundreds of thousands of readily-available and potentially-relevant full or fragmentary documents, but without computer aids that would make it possible to find the sought-after needles in the proverbial haystack of online images. The problems are even more acute when documents are handwritten, since optical character recognition does not provide quality results. We consider two tools: (1) a handwriting matching tool that is used to join together fragments of the same scribe, and (2) a paleographic classification tool that matches a given document to a large set of paleographic samples. Both tools are carefully designed not only to provide a high level of accuracy, but also to provide a clean and concise justification of the inferred results. This last requirement engenders challenges, such as sparsity of the representation, for which existing solutions are inappropriate for document analysis.

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 Λ in the number of variables n . To this end, we develop propositional proof systems under different measures of promises (i.e., different Λ) 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 ϵ…2 n , for any constant 0<ϵ<1. (2) There are no subexponential size resolution refutations for random 3CNF formulas, when the promise is 2 Δ n , for any constant 0<δ<1 (and the number of clauses is O ( n 3/2-ϵ ), for 0<ϵ<1/2). “ Goods Satisfactory or Money Refunded ” —The Eaton Promise

We apply the tree-pattern enumeration formulæof earlier work of ours [N. Dershowitz and S. Zaks, Discrete Appl. Math., 25 (1989), pp. 241–255], and a new extension thereof, to some recent enumerations of distributions of leaves in ordered trees [W. Y. C. Chen, E. Deutsch, and S. Elizalde, European J. Combin., 27 (2006), pp. 414–427] and in bicolored ordered trees [L. H. Clark, J. E. McCanna, and L. A. Székely, Bull. Inst. Combin. Appl., 21 (1997), pp. 33–45], and of distributions of up-down-up subpaths in Dyck lattice paths [Y. Sun, Discrete Math., 287 (2004), pp. 177–186]. Bijections are used to facilitate the derivation of statistics for bicolored trees.

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.

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.

Term Rewriting Systems by “Terese” (Marc Bezem, Jan Willem Klop, and Roel de Vrijer, eds.), Cambridge University Press, Cambridge Tracts in Theoretical Computer Science55, 2003, hard cover: ISBN 0-521-39115-6, xxii+884 pages - Volume 5 Issue 3

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 in the study of equational logic, involve finding appropriate presentations of a given theory to solve easily a given class of problems. We provide a general proof-theoretic setting within which completion-like processes can be modeled and studied. This framework centers around well-founded orderings of proofs. It allows for abstract definitions and very general characterizations of saturation processes and redundancy criteria.

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 Knuth-Bendix completion procedure based on critical pair criteria; Huet's procedure for rewriting modulo a congruence; ordered completion (a refutationally complete extension of standard completion); and a proof by consistency procedure for proving inductive theorems.

Abstract Algorithmic presentations are given for three calendars of historical interest, the Mayan, French Revolutionary, and Old Hindu.

Abstract 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 byproduct of the approach, as is the determination of secular and religious holidays.

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.

A bridge is presented between term-rewriting theory in computer science and proof theory in logic. It is shown that proof-theoretic tools are very useful for analyzing two basic attributes of term rewriting systems, the termination property and the Church-Rosser property. A counterexample is given to show that Knuth's critical pair lemma does not hold for conditional rewrite systems. Two restrictions on conditional systems under which the critical pair lemma holds are presented. One is considered a generalization of Bergstra-Klop's former result; the other is concerned with a generalization of Kaplan's and Jouannaud-Waldmann's systems.>

The construction of term-rewriting systems, specifically by the Knuth–Bendix completion procedure, is considered. We look for conditions that might ensure the existence of a finite canonical rewriting system for a given equational theory and that might guarantee that the completion procedure will find it. We define several notions of equivalence between rewriting systems in the ordinary and modulo case, and examine uniqueness of systems and the need for backtracking in implementing completion.

Our goal is to develop formal methods for abstracting a given set of programs into a program schema and for instantiating a given schema to satisfy concrete specifications. Abstraction and instantiation are two important phases in software development which allow programmers to apply knowledge learned in the solutions of past problems when faced with new situations. For example, from two programs using a linear (or binary) search technique, an abstract schema can be derived that embodies the shared idea and that can be instantiated to solve similar new problems. Along similar lines, the development and application of program transformations are considered. We suggest the formulation of analogies as a basic tool in program abstraction. An analogy is first sought between the specifications of the given programs; this yields an abstract specification that may be instantiated to any of the given concrete specifications. The analogy is then used as a basis for transforming the existing programs into an abstract schema that represents the embedded technique, with the invariant assertions and correctness proofs of the given programs helping to verify and complete the analogy. A given concrete specification of a new problem may then be compared with the abstract specification of the schema to suggest an instantiation of the schema that yields a correct program.

Methods are presented whereby an Algol-like program given together with its specifications can be documented automatically. The program is incrementaly annotated with invariant relations that hold between program variables at intermediate points in the program text and explain the actual workings of the program regardless of whether it is correct. Thus, this documentation can be used for proving correctness of programs or may serve as an aid in debugging incorrect programs.

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.

In a full-text natural-language retrieval system, frequent need for automatic hngulst~c analysis arises, e.g for keyword expansion in a search process, content analysis, or automatic construction of concordances The avadablhty of sophisticated hngulstic tools, which is highly desirable for languages such as Enghsh, is quite imperative for, say, Semmc languages, whose complex morphological structure renders simple-minded and approximate soluuons such as suffix stripping totally useless.Sophisticated tools were designed and constructed via the fusion of grammatical analysis and grammatical synthesis, resulting in a set of global files which provide in some sense a complete grammatical and lexlcal description of the language These files induce a set of local files which adapt to the database at hand and permit flexible on-hne morphological analysis.

An attempt is made to formulate techniques of program modification, whereby a given program that achieves one goal can be transformed into a new program that uses the same principles to achieve a different goal. For example, a program that uses the binary search paradigm to calculate the square root of a number may be modified to divide two numbers in a similar manner, or vice versa. The essence of the approach is to find an analogy between the specifications of the given and desired programs, and then to transform the given program accordingly.