Open Access. Powered by Scholars. Published by Universities.®

Physical Sciences and Mathematics Commons

Open Access. Powered by Scholars. Published by Universities.®

Articles 1 - 7 of 7

Full-Text Articles in Physical Sciences and Mathematics

Fault-Tolerant Concurrent Branch And Bound Algorithms Derived From Program Verification, Hanan Lutfiyya, Aggie Sun, Bruce M. Mcmillin Jan 1992

Fault-Tolerant Concurrent Branch And Bound Algorithms Derived From Program Verification, Hanan Lutfiyya, Aggie Sun, Bruce M. Mcmillin

Computer Science Faculty Research & Creative Works

An important aspect which is often overlooked in software design of distributed environments is that of fault tolerance. Many methodologies in the past have attempted to provide fault tolerance efficiently but have never been successful at eliminating explicit time and space redundancy. One approach for providing fault tolerance is through examining the behavior and properties of the application and deriving executable assertions that detect faults. Our work focuses on transforming the assertions of a verification proof of a program to executable assertions. These executable assertions may be embedded in the program to create a fault-tolerant program. It is also shown …


Proving Functionally Difficult Problems Through Model Generation, Richard Rankin, Ralph W. Wilkerson Jan 1992

Proving Functionally Difficult Problems Through Model Generation, Richard Rankin, Ralph W. Wilkerson

Computer Science Faculty Research & Creative Works

Satchmo [MA88] is a Theorem Prover Implemented in Prolog Which Attempts to Provide Satisfiability Checking through Model Generation. This Paper Gives a Brief Introduction to SATCHMO and Reports Extensions to the Original Work Which Allow SATCHMO to Solve Problems Previously Considered to Be Finitely Unprovable within the SATCHMO System. the Specific Problems Are from [PE86, MO85, LU85] and Were Designed to Convert Simple Propositional Logic Problems into Functionally Difficult First Order Problems. Although the Benefits of using the SATCHMO System Are Many, the Fact that It Could Not Offer Proofs for a Set of Problems Provable in Other Systems is …


Formation Of Clusters And Resolution Of Ordinal Attributes In Id3 Classification Trees, Chaman Sabharwal, Keith R. Hacke, Daniel C. St. Clair Jan 1992

Formation Of Clusters And Resolution Of Ordinal Attributes In Id3 Classification Trees, Chaman Sabharwal, Keith R. Hacke, Daniel C. St. Clair

Computer Science Faculty Research & Creative Works

Many learning systems have been designed to construct classification trees from a set of training examples. One of the most widely used approaches for constructing decision trees is the ID3 algorithm [Quinlan 1986]. Decision trees are ill-suited to handle attributes with ordinal values. Problems arise when a node representing an ordinal attribute has a branch for each value of the ordinal attribute in the training set. This is generally infeasible when the set of ordinal values is very large. Past approaches have sought to cluster large sets of ordinal values before the classification tree is constructed [Quinlan 1986; Lebowitz 1985; …


Parallel Error Tolerance Scheme Based On The Hill Climbing Nature Of Simulated Annealing, Bruce M. Mcmillin, Chul-Eui Hong Jan 1992

Parallel Error Tolerance Scheme Based On The Hill Climbing Nature Of Simulated Annealing, Bruce M. Mcmillin, Chul-Eui Hong

Computer Science Faculty Research & Creative Works

In parallelizing simulated annealing in a multicomputer, maintaining the global state S involves explicit message traffic and is a critical performance bottleneck. One way to mitigate this bottleneck is to amortize the overhead of these state updates over as many parallel state changes as possible. Using this technique introduces errors in the calculated cost C(S) of a particular state S used by the annealing process. Analytically derived bounds are placed on this error in order to assure convergence to the correct result. The resulting parallel simulated annealing algorithm dynamically changes the frequency of global updates as a function of the …


Experimentation With Proof Methods For Non-Horn Sets, Christopher J. Merz, Ralph W. Wilkerson Jan 1992

Experimentation With Proof Methods For Non-Horn Sets, Christopher J. Merz, Ralph W. Wilkerson

Computer Science Faculty Research & Creative Works

Two Resolution Proof Strategies Developed by Peterson Are Implemented by Modifying Otter, an Existing Automated Theorem Prover. the Methods, Lock-T Refutation and LNL-T Refutation, Are Generalizations of Unit Refutation and Input Resolution, Respectively, to Non-Horn Sets and Represent Independent, Equivalent but Opposite Ways of Searching. the Algorithms Used Are based on a Corrected Version of the Foundational Work. the Strategies Have Been Tested on Various Non-Horn Challenge Problems from the Tarskian Geometry and the Non-Obvious Problem, with the Results Being in Some Cases Quite Favorable When Compared to Other Resolution Techniques.


Composite Stock Cutting Through Simulated Annealing, Hanan Lutfiyya, Bruce M. Mcmillin, Pipatpong Poshyanonda, Cihan H. Dagli Jan 1992

Composite Stock Cutting Through Simulated Annealing, Hanan Lutfiyya, Bruce M. Mcmillin, Pipatpong Poshyanonda, Cihan H. Dagli

Computer Science Faculty Research & Creative Works

This paper explores the use of Simulated Annealing as an optimization technique for the problem of Composite Material Stock Cutting. The shapes are not constrained to be convex polygons or even regular shapes. However, due to the composite nature of the material, the orientation of the shapes on the stock is restricted. For placements of various shapes, we show how to determine a cost function, annealing parameters and performance. © 1992.


Semi-Supervised Adaptive Resonance Theory (Smart2), Christopher J. Merz, William E. Bond, Daniel C. St. Clair Jan 1992

Semi-Supervised Adaptive Resonance Theory (Smart2), Christopher J. Merz, William E. Bond, Daniel C. St. Clair

Computer Science Faculty Research & Creative Works

Adaptive resonance theory (ART) algorithms represent a class of neural network architectures which self-organize stable recognition categories in response to arbitrary sequences of input patterns. The authors discuss incorporation of supervision into one of these architectures, ART2. Results of numerical experiments indicate that this new semi-supervised version of ART2 (SMART2) outperformed ART for classification problems. The results and analysis of runs on several data sets by SMART2, ART2, and backpropagation are analyzed. The test accuracy of SMART2 was similar to that of backpropagation. However, SMART2 network structures are easier to interpret than the corresponding structures produced by backpropagation.