Search

Abstract: Elimination Game is a well-known algorithm that simulates Gaussian elimination of matrices on graphs, and it computes a triangulation of the input graph. The number of fill edges in the computed triangulation is highly dependent on the order in which Elimination Game processes the vertices, and in general the produced triangulations are neither minimum nor minimal. In order to obtain a triangulation which is close to minimum, the Minimum Degree heuristic is widely used in practice, but until now little was known on the theoretical mechanisms involved. In this paper we show some interesting properties of Elimination Game; in particular that it is able to compute a partial minimal triangulation of the input graph regardless of the order in which the vertices are processed. This results in a new algorithm to compute minimal triangulations that are sandwiched between the input graph and the triangulation resulting from Elimination Game. One of the strengths of the new approach is that it is easily parallelizable, and thus we are able to present the first parallel algorithm to compute such sandwiched minimal triangulations. In addition, the insight that we gain through Elimination Game is used to partly explain the good behavior of the Minimum Degree algorithm. We also give a new algorithm for producing minimal triangulations that is able to use the minimum degree idea to a wider extent. [Copyright &y& Elsevier]

Abstract: A numerical elimination method is presented in this paper for floating-point computation in polynomial algebra. The method is designed to calculate one or more polynomials in an elimination ideal by a sequence of matrix rank/kernel computation. The method is reliable in numerical computation with verifiable stability and a sensitivity measurement. Computational experiment shows that the method possesses significant advantages over classical resultant computation in numerical stability and in producing eliminant polynomials with lower degrees and fewer extraneous factors. The elimination algorithm combined with an approximate GCD finder appears to be effective in solving polynomial systems for positive dimensional solutions. [Copyright &y& Elsevier]

Abstract: With many applications in engineering and scientific fields, quantifier elimination (QE) has received increasing attention. Cylindrical algebraic decomposition (CAD) is used as a basis for a general QE algorithm. In this paper we present an effective symbolic–numeric cylindrical algebraic decomposition (SNCAD) algorithm for QE incorporating several new devices, which we call “quick tests”. The simple quick tests are run beforehand to detect an unnecessary procedure that might be skipped without violating the correctness of results and they thus considerably reduce the computing time. The effectiveness of the SNCAD algorithm is examined in a number of experiments including practical engineering problems, which also reveal the quality of the implementation. Experimental results show that our implementation has significantly improved efficiency compared with our previous work. [Copyright &y& Elsevier]

Abstract: We re-consider perfect elimination digraphs, that were introduced by Haskins and Rose in 1973, and view these graphs as directed analogues of chordal graphs. Several structural properties of chordal graphs that are crucial for algorithmic applications carry over to the directed setting, including notions like simplicial vertices, perfect elimination orderings, and vertex layouts. We show that semi-complete perfect elimination digraphs are also characterised by a set of forbidden induced subgraphs resemblant of chordless cycles. Moreover, just as the chordal graphs are related to treewidth, the perfect elimination digraphs are related to Kelly-width. [Copyright &y& Elsevier]

Abstract: When investigating the complexity of cut-elimination in first-order logic, a natural subproblem is the elimination of quantifier-free cuts. So far, the problem has only been considered in the context of general cut-elimination, and the upper bounds that have been obtained are essentially double exponential. In this note, we observe that a method due to Dale Miller can be applied to obtain an exponential upper bound. [Copyright &y& Elsevier]

Abstract: We consider the use of state elimination to construct shorter regular expressions from finite-state automata (FAs). Although state elimination is an intuitive method for computing regular expressions from FAs, the resulting regular expressions are often very long and complicated. We examine the minimization of FAs to obtain shorter expressions first. Then, we introduce vertical chopping based on bridge states and horizontal chopping based on the structural properties of given FAs. We prove that we should not eliminate bridge states until we eliminate all non-bridge states to obtain shorter regular expressions. In addition, we suggest heuristics for state elimination that leads to shorter regular expressions based on vertical chopping and horizontal chopping. [Copyright &y& Elsevier]

Abstract: Geometry of Interaction is a transcendental syntax developed in the framework of operator algebras. This fifth installment of the program takes place inside a von Neumann algebra, the hyperfinite factor. It provides a built-in interpretation of cut-elimination as well as an explanation for light, i.e., complexity sensitive, logics. [Copyright &y& Elsevier]

Abstract: We give a semantic account of the execution time (i.e. the number of cut elimination steps leading to the normal form) of an untyped net. We first prove that: (1) a net is head-normalizable (i.e. normalizable at depth ) if and only if its interpretation in the multiset based relational semantics is not empty and (2) a net is normalizable if and only if its exhaustive interpretation (a suitable restriction of its interpretation) is not empty. We then give a semantic measure of execution time: we prove that we can compute the number of cut elimination steps leading to a cut free normal form of the net obtained by connecting two cut free nets by means of a cut-link, from the interpretations of the two cut free nets. These results are inspired by similar ones obtained by the first author for the untyped lambda-calculus. [Copyright &y& Elsevier]