Narrow Results

Each rapid prototyping (RP) process has its special and unique advantages and disadvantages. The chapter presents a state-of-the-art study of RP technologies and classifies broadly all the different types of rapid prototyping methods. Subsequently, the fundamental principles and technological limitations of different methods of RP will be closely examined. Comparison of the present and ultimate performance of the rapid prototyping processes will be made so as to highlight the possibility of future improvements for a new generation of RP system.

The basic unit of image coding based on DCT was deemed as a complete entity, such as 8 × 8 code block in JPEG standard, therefore, the image coding based on DCT has large difficulty to implement resolution scalability. This paper proposed a resolution scalability scheme for image codec based on DCT. The encoder recombines the DCT coefficients according to their frequency, and the sub DCT code blocks are encoded in term of the image resolution. After decoding the coefficients form low-frequency to high-frequency, the decoder selects the IDCT models to reconstruct the image from low resolution to high resolution. Experimental results show that our method can get more flexible scalability than that of the methods of DWT base.

Because of the large number of strategies and inference rules presently under consideration in automated theorem proving, there is a need for developing a language especially oriented toward automated theorem proving. This paper discusses some of the features and instructions of this language. The use of this language permits easy extension of automated theorem-proving programs to include new strategies and/or new inference rules. Such extendability will permit general experimentation with the various alternative systems.

The key concepts for this automated theorem-proving paper are those of Horn set and strictly-unit refutation. A Horn set is a set of clauses such that none of its members contains more than one positive literal. A strictly-unit refutation is a proof by contradiction in which no step is justified by applying a rule of inference to a set of clauses all of which contain more than one literal. Horn sets occur in many fields of mathematics such as the theory of groups, rings, Moufang loops, and Henkin models. The usual translation into first-order predicate calculus of the axioms of these and many other fields yields a set of Horn clauses. The striking feature of the Horn property for finite sets of clauses is that its presence or absence can be determined by inspection. Thus, the determination of the applicability of the theorems and procedures of this paper is immediate.

In Theorem 1 it is proved that, if is an unsatisfiable Horn set, there exists a strictly-unit refutation of employing binary resolution alone, thus eliminating the need for factoring; moreover, one of the immediate ancestors of each step of the refutation is in fact a positive unit clause. A theorem similar to Theorem 1 for paramodulation-based inference systems is proven in Theorem 3 but with the inclusion of factoring as an inference rule. In Section 3 two reduction procedures are discussed. For the first, Chang's splitting, a rule is provided to guide both the choice of clauses and the way in which to split. The second reduction procedure enables one to refute a Horn set by refuting but one of a corresponding family of simpler subproblems.

The two objectives of this paper are 1) to give a large and varied problem set, complete clause sets for use in testing automated theorem-proving programs and 2) the presentation of a number of experiments with an existing program under a variety of conditions.

The problems range from quite trivial to quite difficult, including some for which a refutation was not obtained. The statements of a problem without the full list of corresponding clauses would be of only cursory value when viewed from either of the objectives of this paper. The problems are taken from the usually studied algebraic systems, Tarskian geometry, Henkin models, and from Wang's suggested test cases, among others. Among those included herein, the following are of added interest because of their difficulty, especially from the viewpoint of automated theorem proving.

1) In group theory x³ = e implies the cummutator ((x,y),y) = e. The proof is rather longer than that of the usually cited test problems for theorem-proving programs. The problem is even somewhat challenging for the individual unaided by the computer.

2) Using the Tarski axioms for plane geometry, the relation of betweenness can be shown to be symmetric. This axiom set is quite nonintuitive. The problems taken from this field provide an interesting test for programs because, among other considerations, they use six place functions in the corresponding clause sets.

The experiments compare the inference rules of UR-resolution, hyperresolution, paramodulation, taken separately, and in combination. Presented herein are examples employing the set of support strategy, various complexity schemes (C-sets), inclusion of lemmas, various demodulation approaches, and various clause representations.

The program was developed at Northern Illinois University and the experiments are from its use at the Argonne National Laboratory on an IBM 370/195. Time for the experiments, number of clauses generated, number of clauses retained, percentage of successful unifications, and some of the parameters governing each experiment are given together with the actual set of clauses employed therein.

This article discusses the two incarnations of Otter entered in the CADE-13 Automated Theorem Proving Competition. Also presented are some historical background, a summary of applications that have led to new results in mathematics and logic, and a general discussion of Otter.

Resolution principle proposed originally by Robinson in 1965 has dominated automated deduction for over three decades while the current most successful automated deduction systems are based on resolution. In this paper, we consider a generalization of the standard resolution principle and their variation since then, it is proposed as a multi-ary, dynamic, contradiction separation based inference rule for automated deduction, where the existing resolution rule and its variations are its special cases. The key concepts and some conclusions are briefly outlined in this short paper.

A number of image processing parameters in the 3D reconstruction of a ribosome complex from a cryo-EM data set were varied to test their effects on the final resolution. The parameters examined were pixel size, window size, and mode of Fourier amplitude enhancement at high spatial frequencies. In addition, the strategy of switching from large to small pixel size during angular refinement was explored. The relationship between resolution (in Fourier space) and the number of particles was observed to follow a lin-log dependence, a relationship that appears to hold for other data, as well. By optimizing the above parameters, and using a lin-log extrapolation to the full data set in the estimation of resolution from half-sets, we obtained a 3D map from 131,599 ribosome particles at 6.7 Å resolution (FSC = 0.5).

Contradiction separation based dynamic automated deduction is a novel development of the standard static (i.e., fixed) binary resolution into a dynamic multi-clause synergized contradiction separation based inference rule. In this paper, we consider some distinctive features/advantages of this novel automated deduction mechanism, including multi-clause involvement, dynamic deduction, synergized deduction, robustness, exchangeability, controllability, scaling, repeatability, integrity and flexibility, along with some illustrative examples.

In the present paper, an ideal-based resolution principle for the lattice-valued prepositional logic LP(X) based on lattice implication algebra is focused. A LI-ideal of lattice implication algebra is taken as the criterion for measuring the unsatisfiability of a lattice-valued logical formula. The ideal-based resolution principle for lattice-valued propositional logic LP(X) is established. The soundness and weak completeness theorems of A – resolution principle based on LP(X) are established. Finally, the properties of A – resolution are discussed.