OpenRaiser/Intern-Atlas huggingface dataset:
A Coalgebraic Approach to Kleene Algebra with Tests
Venue: arXiv cs.LO 2004
Year: 2004

Kleene algebra with tests is an extension of Kleene algebra, the algebra of regular expressions, which can be used to reason about programs. We develop a coalgebraic theory of Kleene algebra with tests, along the lines of the coalgebraic theory of regular expressions based on deterministic automata. Since the known automata-theoretic presentation of Kleene algebra with tests does not lend itself to a coalgebraic theory, we define a new interpretation of Kleene algebra with tests expressions and a corresponding automata-theoretic presentation. One outcome of the theory is a coinductive proof principle, that can be used to establish equivalence of our Kleene algebra with tests expressions.
Typing constraint logic programs
Venue: arXiv cs.PL 2004
Year: 2004

We present a prescriptive type system with parametric polymorphism and subtyping for constraint logic programs. The aim of this type system is to detect programming errors statically. It introduces a type discipline for constraint logic programs and modules, while maintaining the capabilities of performing the usual coercions between constraint domains, and of typing meta-programming predicates, thanks to the flexibility of subtyping. The property of subject reduction expresses the consistency of a prescriptive type system w.r.t. the execution model: if a program is "well-typed", then all derivations starting from a "well-typed" goal are again "well-typed". That property is proved w.r.t. the abstract execution model of constraint programming which proceeds by accumulation of constraints only, and w.r.t. an enriched execution model with type constraints for substitutions. We describe our implementation of the system for type checking and type inference. We report our experimental results on type checking ISO-Prolog, the (constraint) libraries of Sicstus Prolog and other Prolog programs.
A Proof Theoretic Approach to Failure in Functional Logic Programming
Venue: arXiv cs.PL 2004
Year: 2004

How to extract negative information from programs is an important issue in logic programming. Here we address the problem for functional logic programs, from a proof-theoretic perspective. The starting point of our work is CRWL (Constructor based ReWriting Logic), a well established theoretical framework for functional logic programming, whose fundamental notion is that of non-strict non-deterministic function. We present a proof calculus, CRWLF, which is able to deduce negative information from CRWL-programs. In particular, CRWLF is able to prove finite failure of reduction within CRWL.
Study of Pakistan Election System as Intelligent e-Election
Venue: arXiv cs.CY 2004
Year: 2004

The proposed election system lies in ensuring that it is transparent and impartial.Thus while the electoral system may vary from country to country, It has to take into account the peculiarities of every society while at the same time incorporating remedies to problems prevailing in the system. The Electoral process expressed serious concerns regarding the independence of the Election Commission of Pakistan, the restrictions on political parties and their candidates, the misuse of state resources, some unbalanced coverage in the state media, deficiencies in the compilation of the voting register and significant problems relating to the provision of ID cards. The holding of a general election does not in itself guarantee the restoration of democracy. The unjustified interference with electoral arrangements, as detailed above, irrespective of the alleged motivation, resulted in serious flaws being inflicted on the electoral process. Additionally, questions remain as to whether or not there will be a full transfer of power from a military to civilian administration. The Independent study research has following modules: Login/Subscription Module Candidate Subscription Module Vote casting Module Administration Module Intelligent decision data analysis Module
A novel approach to symbolic algebra
Venue: arXiv cs.SC 2004
Year: 2004

A prototype for an extensible interactive graphical term manipulation system is presented that combines pattern matching and nondeterministic evaluation to provide a convenient framework for doing tedious algebraic manipulations that so far had to be done manually in a semi-automatic fashion.
The Computational Complexity of Orientation Search Problems in Cryo-Electron Microscopy
Venue: arXiv cs.DS 2004
Year: 2004

In this report we study the problem of determining three-dimensional orientations for noisy projections of randomly oriented identical particles. The problem is of central importance in the tomographic reconstruction of the density map of macromolecular complexes from electron microscope images and it has been studied intensively for more than 30 years. We analyze the computational complexity of the orientation problem and show that while several variants of the problem are $NP$-hard, inapproximable and fixed-parameter intractable, some restrictions are polynomial-time approximable within a constant factor or even solvable in logarithmic space. The orientation search problem is formalized as a constrained line arrangement problem that is of independent interest. The negative complexity results give a partial justification for the heuristic methods used in orientation search, and the positive complexity results on the orientation search have some positive implications also to the problem of finding functionally analogous genes. A preliminary version ``The Computational Complexity of Orientation Search in Cryo-Electron Microscopy'' appeared in Proc. ICCS 2004, LNCS 3036, pp. 231--238. Springer-Verlag 2004.
Web Services: A Process Algebra Approach
Venue: arXiv cs.AI 2004
Year: 2004

It is now well-admitted that formal methods are helpful for many issues raised in the Web service area. In this paper we present a framework for the design and verification of WSs using process algebras and their tools. We define a two-way mapping between abstract specifications written using these calculi and executable Web services written in BPEL4WS. Several choices are available: design and correct errors in BPEL4WS, using process algebra verification tools, or design and correct in process algebra and automatically obtaining the corresponding BPEL4WS code. The approaches can be combined. Process algebra are not useful only for temporal logic verification: we remark the use of simulation/bisimulation both for verification and for the hierarchical refinement design method. It is worth noting that our approach allows the use of any process algebra depending on the needs of the user at different levels (expressiveness, existence of reasoning tools, user expertise).
The Complexity of Agreement
Venue: arXiv cs.CC 2004
Year: 2004

A celebrated 1976 theorem of Aumann asserts that honest, rational Bayesian agents with common priors will never "agree to disagree": if their opinions about any topic are common knowledge, then those opinions must be equal. Economists have written numerous papers examining the assumptions behind this theorem. But two key questions went unaddressed: first, can the agents reach agreement after a conversation of reasonable length? Second, can the computations needed for that conversation be performed efficiently? This paper answers both questions in the affirmative, thereby strengthening Aumann's original conclusion. We first show that, for two agents with a common prior to agree within epsilon about the expectation of a [0,1] variable with high probability over their prior, it suffices for them to exchange order 1/epsilon^2 bits. This bound is completely independent of the number of bits n of relevant knowledge that the agents have. We then extend the bound to three or more agents; and we give an example where the economists' "standard protocol" (which consists of repeatedly announcing one's current expectation) nearly saturates the bound, while a new "attenuated protocol" does better. Finally, we give a protocol that would cause two Bayesians to agree within epsilon after exchanging order 1/epsilon^2 messages, and that can be simulated by agents with limited computational resources. By this we mean that, after examining the agents' knowledge and a transcript of their conversation, no one would be able to distinguish the agents from perfect Bayesians. The time used by the simulation procedure is exponential in 1/epsilon^6 but not in n.
Autogenic Training With Natural Language Processing Modules: A Recent Tool For Certain Neuro Cognitive Studies
Venue: arXiv cs.AI 2004
Year: 2004

Learning to respond to voice-text input involves the subject's ability in understanding the phonetic and text based contents and his/her ability to communicate based on his/her experience. The neuro-cognitive facility of the subject has to support two important domains in order to make the learning process complete. In many cases, though the understanding is complete, the response is partial. This is one valid reason why we need to support the information from the subject with scalable techniques such as Natural Language Processing (NLP) for abstraction of the contents from the output. This paper explores the feasibility of using NLP modules interlaced with Neural Networks to perform the required task in autogenic training related to medical applications.
An algorithm for two-dimensional mesh generation based on the pinwheel tiling
Venue: arXiv cs.CG 2004
Year: 2004

We propose a new two-dimensional meshing algorithm called PINW able to generate meshes that accurately approximate the distance between any two domain points by paths composed only of cell edges. This technique is based on an extension of pinwheel tilings proposed by Radin and Conway. We prove that the algorithm produces triangles of bounded aspect ratio. This kind of mesh would be useful in cohesive interface finite element modeling when the crack propagation pathis an outcome of a simulation process.
Track Layouts of Graphs
Venue: arXiv cs.DM 2004
Year: 2004

A \emph{$(k,t)$-track layout} of a graph $G$ consists of a (proper) vertex $t$-colouring of $G$, a total order of each vertex colour class, and a (non-proper) edge $k$-colouring such that between each pair of colour classes no two monochromatic edges cross. This structure has recently arisen in the study of three-dimensional graph drawings. This paper presents the beginnings of a theory of track layouts. First we determine the maximum number of edges in a $(k,t)$-track layout, and show how to colour the edges given fixed linear orderings of the vertex colour classes. We then describe methods for the manipulation of track layouts. For example, we show how to decrease the number of edge colours in a track layout at the expense of increasing the number of tracks, and vice versa. We then study the relationship between track layouts and other models of graph layout, namely stack and queue layouts, and geometric thickness. One of our principle results is that the queue-number and track-number of a graph are tied, in the sense that one is bounded by a function of the other. As corollaries we prove that acyclic chromatic number is bounded by both queue-number and stack-number. Finally we consider track layouts of planar graphs. While it is an open problem whether planar graphs have bounded track-number, we prove bounds on the track-number of outerplanar graphs, and give the best known lower bound on the track-number of planar graphs.
Reduced cost-based ranking for generating promising subproblems
Venue: arXiv cs.AI 2004
Year: 2004

In this paper, we propose an effective search procedure that interleaves two steps: subproblem generation and subproblem solution. We mainly focus on the first part. It consists of a variable domain value ranking based on reduced costs. Exploiting the ranking, we generate, in a Limited Discrepancy Search tree, the most promising subproblems first. An interesting result is that reduced costs provide a very precise ranking that allows to almost always find the optimal solution in the first generated subproblem, even if its dimension is significantly smaller than that of the original problem. Concerning the proof of optimality, we exploit a way to increase the lower bound for subproblems at higher discrepancies. We show experimental results on the TSP and its time constrained variant to show the effectiveness of the proposed approach, but the technique could be generalized for other problems.
Bug shallowness in open-source, Macintosh software
Venue: arXiv cs.SE 2004
Year: 2004

Central to the power of open-source software is bug shallowness, the relative ease of finding and fixing bugs. The open-source movement began with Unix software, so many users were also programmers capable of finding and fixing bugs given the source code. But as the open-source movement reaches the Macintosh platform, bugs may not be shallow because few Macintosh users are programmers. Based on reports from open-source developers, I, however, conclude that that bugs are as shallow in open-source, Macintosh software as in any other open-source software.
M@th Desktop and MD Tools - Mathematics and Mathematica Made Easy for Students
Venue: arXiv cs.MS 2004
Year: 2004

We present two add-ons for Mathematica for teaching mathematics to undergraduate and high school students. These two applications, M@th Desktop (MD) and M@th Desktop Tools (MDTools), include several palettes and notebooks covering almost every field. The underlying didactic concept is so-called "blended learning", in which these tools are meant to be used as a complement to the professor or teacher rather than as a replacement, which other e-learning applications do. They enable students to avoid the usual problem of computer-based learning, namely that too large an amount of time is wasted struggling with computer and program errors instead of actually learning the mathematical concepts. M@th Desktop Tools is palette-based and provides easily accessible and user-friendly templates for the most important functions in the fields of Analysis, Algebra, Linear Algebra and Statistics. M@th Desktop, in contrast, is a modern, interactive teaching and learning software package for mathematics classes. It is comprised of modules for Differentiation, Integration, and Statistics, and each module presents its topic with a combination of interactive notebooks and palettes. Both packages can be obtained from Deltasoft's homepage at http://www.deltasoft.at/ .
Design of a Parallel and Distributed Web Search Engine
Venue: arXiv cs.IR 2004
Year: 2004

This paper describes the architecture of MOSE (My Own Search Engine), a scalable parallel and distributed engine for searching the web. MOSE was specifically designed to efficiently exploit affordable parallel architectures, such as clusters of workstations. Its modular and scalable architecture can easily be tuned to fulfill the bandwidth requirements of the application at hand. Both task-parallel and data-parallel approaches are exploited within MOSE in order to increase the throughput and efficiently use communication, storing and computational resources. We used a collection of html documents as a benchmark, and conducted preliminary experiments on a cluster of three SMP Linux PCs.
The asymptotic number of binary codes and binary matroids
Venue: arXiv cs.IT 2004
Year: 2004

The asyptotic number of nonequivalent binary n-codes is determined. This is also the asymptotic number of nonisomorphic binary n-matroids. The connection to a result of Lefmann, Roedl, Phelps is explored. The latter states that almost all binary n-codes have a trivial automorphism group.
Roles Are Really Great!
Venue: arXiv cs.PL 2004
Year: 2004

We present a new role system for specifying changing referencing relationships of heap objects. The role of an object depends, in large part, on its aliasing relationships with other objects, with the role of each object changing as its aliasing relationships change. Roles therefore capture important object and data structure properties and provide useful information about how the actions of the program interact with these properties. Our role system enables the programmer to specify the legal aliasing relationships that define the set of roles that objects may play, the roles of procedure parameters and object fields, and the role changes that procedures perform while manipulating objects. We present an interprocedural, compositional, and context-sensitive role analysis algorithm that verifies that a program respects the role constraints.
On Generalized Records and Spatial Conjunction in Role Logic
Venue: arXiv cs.PL 2004
Year: 2004

We have previously introduced role logic as a notation for describing properties of relational structures in shape analysis, databases and knowledge bases. A natural fragment of role logic corresponds to two-variable logic with counting and is therefore decidable. We show how to use role logic to describe open and closed records, as well the dual of records, inverse records. We observe that the spatial conjunction operation of separation logic naturally models record concatenation. Moreover, we show how to eliminate the spatial conjunction of formulas of quantifier depth one in first-order logic with counting. As a result, allowing spatial conjunction of formulas of quantifier depth one preserves the decidability of two-variable logic with counting. This result applies to two-variable role logic fragment as well. The resulting logic smoothly integrates type system and predicate calculus notation and can be viewed as a natural generalization of the notation for constraints arising in role analysis and similar shape analysis approaches.
An Algorithm for Quasi-Associative and Quasi-Markovian Rules of Combination in Information Fusion
Venue: arXiv cs.AI 2004
Year: 2004

In this paper one proposes a simple algorithm of combining the fusion rules, those rules which first use the conjunctive rule and then the transfer of conflicting mass to the non-empty sets, in such a way that they gain the property of associativity and fulfill the Markovian requirement for dynamic fusion. Also, a new rule, SDL-improved, is presented.
Non-uniform Information Dissemination for Sensor Networks
Venue: arXiv cs.NI 2004
Year: 2004

Future smart environments will be characterized by multiple nodes that sense, collect, and disseminate information about environmental phenomena through a wireless network. In this paper, we define a set of applications that require a new form of distributed knowledge about the environment, referred to as non-uniform information granularity. By non-uniform information granularity we mean that the required accuracy or precision of information is proportional to the distance between a source node (information producer) and current sink node (information consumer). That is, as the distance between the source node and sink node increases, loss in information precision is acceptable. Applications that can benefit from this type of knowledge range from battlefield scenarios to rescue operations. The main objectives of this paper are two-fold: first, we will precisely define non-uniform information granularity, and second, we will describe different protocols that achieve non-uniform information dissemination and analyze these protocols based on complexity, energy consumption, and accuracy of information.
Multi-dimensional Type Theory: Rules, Categories, and Combinators for Syntax and Semantics
Venue: arXiv cs.CL 2004
Year: 2004

We investigate the possibility of modelling the syntax and semantics of natural language by constraints, or rules, imposed by the multi-dimensional type theory Nabla. The only multiplicity we explicitly consider is two, namely one dimension for the syntax and one dimension for the semantics, but the general perspective is important. For example, issues of pragmatics could be handled as additional dimensions. One of the main problems addressed is the rather complicated repertoire of operations that exists besides the notion of categories in traditional Montague grammar. For the syntax we use a categorial grammar along the lines of Lambek. For the semantics we use so-called lexical and logical combinators inspired by work in natural logic. Nabla provides a concise interpretation and a sequent calculus as the basis for implementations.
Application of the Double Metaphone Algorithm to Amharic Orthography
Venue: arXiv cs.CL 2004
Year: 2004

The Metaphone algorithm applies the phonetic encoding of orthographic sequences to simplify words prior to comparison. While Metaphone has been highly successful for the English language, for which it was designed, it may not be applied directly to Ethiopian languages. The paper details how the principles of Metaphone can be applied to Ethiopic script and uses Amharic as a case study. Match results improve as specific considerations are made for Amharic writing practices. Results are shown to improve further when common errors from Amharic input methods are considered.
A CHR-based Implementation of Known Arc-Consistency
Venue: arXiv cs.LO 2004
Year: 2004

In classical CLP(FD) systems, domains of variables are completely known at the beginning of the constraint propagation process. However, in systems interacting with an external environment, acquiring the whole domains of variables before the beginning of constraint propagation may cause waste of computation time, or even obsolescence of the acquired data at the time of use. For such cases, the Interactive Constraint Satisfaction Problem (ICSP) model has been proposed as an extension of the CSP model, to make it possible to start constraint propagation even when domains are not fully known, performing acquisition of domain elements only when necessary, and without the need for restarting the propagation after every acquisition. In this paper, we show how a solver for the two sorted CLP language, defined in previous work, to express ICSPs, has been implemented in the Constraint Handling Rules (CHR) language, a declarative language particularly suitable for high level implementation of constraint solvers.
Analysis and Visualization of Index Words from Audio Transcripts of Instructional Videos
Venue: arXiv cs.IR 2004
Year: 2004

We introduce new techniques for extracting, analyzing, and visualizing textual contents from instructional videos of low production quality. Using Automatic Speech Recognition, approximate transcripts (H75% Word Error Rate) are obtained from the originally highly compressed videos of university courses, each comprising between 10 to 30 lectures. Text material in the form of books or papers that accompany the course are then used to filter meaningful phrases from the seemingly incoherent transcripts. The resulting index into the transcripts is tied together and visualized in 3 experimental graphs that help in understanding the overall course structure and provide a tool for localizing certain topics for indexing. We specifically discuss a Transcript Index Map, which graphically lays out key phrases for a course, a Textbook Chapter to Transcript Match, and finally a Lecture Transcript Similarity graph, which clusters semantically similar lectures. We test our methods and tools on 7 full courses with 230 hours of video and 273 transcripts. We are able to extract up to 98 unique key terms for a given transcript and up to 347 unique key terms for an entire course. The accuracy of the Textbook Chapter to Transcript Match exceeds 70% on average. The methods used can be applied to genres of video in which there are recurrent thematic words (news, sports, meetings,...)
Probabilistic Analysis of Rule 2
Venue: arXiv cs.DM 2004
Year: 2004

Li and Wu proposed Rule 2, a localized approximation algorithm that attempts to find a small connected dominating set in a graph. Here we study the asymptotic performance of Rule 2 on random unit disk graphs formed from n random points in an s_n by s_n square region of the plane. If s_n is below the threshold for connectivity, then Rule 2 produces a dominating set whose expected size is O(n/(loglog n)^{3/2}). We conjecture that this bound is not optimal.