Combining logical and algebraic techniques for natural style proving in elementary analysis

PCS (Proving-Computing-Solving) introduced by B. Buchberger in 2001 and S-Decomposition, introduced by T. Jebelean in 2001, are strategies for handling proof problems by combining logic inference steps (e.g., modus ponens, Skolemization, instantiation) with rewriting steps (application of definitions) and solving procedures based on algebraic techniques (e.g., Groebner Bases, Cylindrical Algebraic Decomposition).     

Trees,grids, and MSO decidability: From graphs to matroids

Monadic second order (MSO) logic has proved to be a useful tool in many areas of application, reaching from decidability and complexity to picture processing, correctness of programs and parallel processes. To characterize the structural borderline between decidability and undecidability is a classical research problem here. This problem is related to questions in computational complexity, especially to the model checking problem, for which many tools developed in the area of decidability have proved to be useful. For more than two decades it was conjectured in [D. Seese, The structure of the models of decidable monadic theories of graphs, Ann. Pure Appl. Logic 53 (1991) 169–195] that decidability of monadic theories of countable structures implies that the theory can be reduced via interpretability to a theory of trees.     

A simple and efficient boolean solver for Constraint Logic Programming

We study in this paper the use of consistency techniques and local propagation methods, originally developed for constraints over finite domains, for solving boolean constraints in Constraint Logic Programming (CLP). To this aim, we first present a boolean CLP language clp(B/FD) built upon a CLP language over finite domains clp(FD) which uses a propagation-based constraint solver. It is based on a single primitive constraint which allows the boolean solver to be encoded at a low level. The boolean solver obtained in this way is both very simple and very efficient: on average it is eight times faster than the CHIP propagation-based boolean solver, i.e. nearly an order of magnitude faster, and infinitely better than the CHIP boolean unification solver. It also performs on average several times faster than special-purpose stand-alone boolean solvers. We then present in a second time several simplifications of the above approach, leading to the design of a very simple and compact dedicated boolean solver. This solver can be implemented in a WAM-based logical engine with a minimal extension limited to four new abstract instructions. This clp(B) system provides a further factor two speedup w.r.t. clp(B/FD).     

Constructing finite algebras with FALCON

The generation of models and counterexamples is an important form of reasoning. In this paper, we give a formal account of a system, called FALCON, for constructing finite algebras from given equational axioms. The abstract algorithms, as well as some implementation details and sample applications, are presented. The generation of finite models is viewed as a constraint satisfaction problem, with ground instances of the axioms as constraints. One feature of the system is that it employs a very simple technique, called the least number heuristic, to eliminate isomorphic (partial) models, thus reducing the size of the search space. The correctness of the heuristic is proved. Some experimental data are given to show the performance and applications of the system.     

On the completeness of incidence calculus

Incidence calculus is a mechanism for uncertain reasoning originally introduced by Bundy. He suggested a set of inference rules for deriving new incidence bounds from a given set of lower and upper bounds of some propositions. However, it is important to demonstrate that the inference axioms are complete in any axiomatization. It is proved in this paper that inference rules used by Bundy are indeed complete.     

A New Sparse Gaussian Elimination Algorithm and the Niederreiter Linear System for Trinomials over F 2

An important factorization algorithm for polynomials over finite fields was developed by Niederreiter. The factorization problem is reduced to solving a linear system over the finite field in question, and the solutions are used to produce the complete factorization of the polynomial into irreducibles. One charactersistic feature of the linear system arising in the Niederreiter algorithm is the fact that, if the polynomial to be factorized is sparse, then so is the Niederreiter matrix associated with it. In this paper, we investigate the special case of factoring trinomials over the binary field. We develop a new algorithm for solving the linear system using sparse Gaussian elmination with the Markowitz ordering strategy. Implementing the new algorithm to solve the Niederreiter linear system for trinomials over F₂ suggests that, the system is not only initially sparse, but also preserves its sparsity throughout the Gaussian elimination phase. When used with other methods for extracting the irreducible factors using a basis for the solution set, the resulting algorithm provides a more memory efficient and sometimes faster sequential alternative for achieving high degree trinomial factorizations over F₂.     

A type-theoretic interpretation of constructive domain theory

We present an interpreation of a constructive domain theory in Martin-Löf's type theory. More specifically, we construct a well-pointed Cartesian closed category of semilattices and approximable mappings. This construction is completely formalized and checked using the interactive proof assistant ALF. We base our work on Martin-Löf's domain interpretation of the theory of expressions underlying type theory. But our emphasis is different from Martin-Löf's, who interprets the program forms of type theory and proves a correspondence between their denotational and operational semantics. We instead show that a theory of domains can be developed within a well-defined fragment of (total) type theory. This is an important step toward constructing a model of all of partial type theory (type theory extended with general recursion) inside total type theory.     

A linear compound algorithm for uniform machine scheduling

In this paper, we consider the classical two uniform machine scheduling problem. We present a compound algorithm which consists of three Greedy-like subprocedures running independently. We prove that the algorithm has a worst-case bound of 7/6 and runs in linear time. Partially supported by SFB F003 “Optimierung und Kontrolle”, Projektbereich Diskrete Optimierung and by the National Natural Science Foundation of China.     

A fuzzy soft flood alarm model

A wide range of hydrological analyses for flood, water resources, water quality, ecological studies, etc., require reliable quantification of rainfall inputs. This work illustrates a fuzzy analysis that has the capability to simulate the unknown relations between a set of meteorological and hydrological parameters. A fuzzy approach to flood alarm prediction based on the fuzzy soft set theory is applied to five selected sites of Kerala, India to predict potential flood.     

Makespan minimization in preemptive two machine job shops

In this note we investigate the NP-complete problem of minimizing the makespan in a preemptive two machine job shop. We present a polynomial time approximation algorithm with worst case ratio 3/2 for this problem, and we also argue that this is the best possible result that can be derived via our line of approach.     

?ukasiewicz transform and its application to compression and reconstruction of digital images

We define the ?ukasiewicz transform as a residuated map and a homomorphism between semimodules over the semiring reducts of an MV-algebra. Then we describe the “?ukasiewicz Transform Based” (?TB) algorithm for image processing, demonstrating its applicability.     

Optimality of size-width tradeoffs for resolution

This paper is concerned with the complexity of proofs and of searching for proofs in resolution. We show that the recently proposed algorithm of Ben-Sasson & Wigderson for searching for proofs in resolution cannot give better than weakly exponential performance. This is a consequence of our main result: we show the optimality of the general relationship called size-width tradeoffs in Ben-Sasson & Wigderson. Moreover we obtain the optimality of the size-width tradeoffs for the widely used restrictions of resolution: regular, Davis-Putnam, negative, positive. Received: January 31, 2000.     

SpiNNaker: Fault tolerance in a power- and area- constrained large-scale neuromimetic architecture

SpiNNaker is a biologically-inspired massively-parallel computer designed to model up to a billion spiking neurons in real-time. A full-fledged implementation of a SpiNNaker system will comprise more than 10⁵ integrated circuits (half of which are SDRAMs and half multi-core systems-on-chip). Given this scale, it is unavoidable that some components fail and, in consequence, fault-tolerance is a foundation of the system design. Although the target application can tolerate a certain, low level of failures, important efforts have been devoted to incorporate different techniques for fault tolerance. This paper is devoted to discussing how hardware and software mechanisms collaborate to make SpiNNaker operate properly even in the very likely scenario of component failures and how it can tolerate system-degradation levels well above those expected.     

The complexity of deciding stability under FFS in the Adversarial Queueing model

We address the problem of deciding whether a given network is stable in the Adversarial Queueing Model when considering farthest-from-source (ffs) as the queueing policy to schedule the packets through its links. We show a characterisation of the networks which are stable under ffs in terms of a family of forbidden subgraphs. We show that the set of networks stable under ffs coincide with the set of universally stable networks. Since universal stability of networks can be checked in polynomial time, we obtain that stability under ffs can also be decided in polynomial time.     

Measuring the network robustness by Monte Carlo estimation of shortest path length distribution

Two kinds of robustness measure for networks are introduced and applied to the road network systems in Japan. One is on the connectivity of randomly chosen pair of vertices, another is on the shortest path length between pair of connected vertices. We devise Monte Carlo methods for the computation of two measures.     

The falkneer-skan equation: Numerical solutions within group invariance theory

The iterative transformation method, defined within the framework of the group invariance theory, is applied to the numerical solution of the Falkner-Skan equation with relevant boundary conditions. In this problem a boundary condition at infinity is imposed which is not suitable for a numerical use. In order to overcome this difficulty we introduce a free boundary formulation of the problem, and we define the iterative transformation method that reducess the free boundary formulation to a sequence of initial value problems. Moreover, as far as the value of the wall shear stress is concerned we propose a numerical test of convergence. The usefulness of our approach is illustrated by considering the wall shear stress for the classical Homann and Hiemenz flows. In the Homann's case we apply the proposed numerical test of convergence, and meaningful numerical results are listed. Moreover, for both cases we compared our results with those reported in literature.     

A self-stabilizing algorithm for strong fairness

Self-stabilization is a novel technique to deal with faults in distributed systems. This paper presents a distributed self-stabilizing algorithm for implementing strong fairness in an arbitrary network. A desirable feature of this algorithm is that it can be used to enforce the strong fairness property on any distributed algorithm including self-stabilizing algorithms. In addition, the algorithm does not require any initialization and can withstand transient failures. At the end of the paper such issues as improving the time complexity of the proposed algorithm and the limitations on the efficiency of any implementation of strong fairness are discussed.     

A Semi-smooth Newton Method for Regularized State-constrained Optimal Control of the Navier-Stokes Equations

In this paper, we study semi-smooth Newton methods for the numerical solution of regularized pointwise state-constrained optimal control problems governed by the Navier-Stokes equations. After deriving an appropriate optimality system for the original problem, a class of Moreau-Yosida regularized problems is introduced and the convergence of their solutions to the original optimal one is proved. For each regularized problem a semi-smooth Newton method is applied and its local superlinear convergence verified. Finally, selected numerical results illustrate the behavior of the method and a comparison between the max-min and the Fischer-Burmeister as complementarity functionals is carried out.     

Efficiency issues in the kbmag procedure

A well-known computational approach to finite presentations of infinite groups is the kbmag procedure of Epstein, Holt and Rees. We describe some efficiency issues relating to the procedure and detail two asymptotic improvements: an index for the rewriting system that uses generalized suffix trees and the use of dynamic programming to reduce the number of verification steps.