High-level finite-state-machine is a behavioral level hardware system design specification method. Each of its state transitions is tagged with a description of an expression executed during the corresponding state transition. In order to verify the equivalence between a high-level finite-state-machine and its deriving low-level finite-state-machine, we can extract expressions executed in state transition sequences from an annotated state to another. Then, the extracted expression can be checked against the corresponding expression in the high-level finite-state-machine for their equivalence. Past research adopted a simulation-based validation technique to examine expression equivalence. Due to its combinatorial complexity, it can not guarantee hundred percent equivalence for expression passing the test. In this research, we designed software of our expression equivalence verification method applied on the extracted expressions. It consists of software design tasks of tree system functionalities : 1. By applying a normalization method on commutative, associative, and distributive laws, we can transform each expression into an equivalent reduced expression graph. It can reduce the size of the equivalence space to be explored in the equivalence verification process and thus reduce computation time and storage size of explored equivalent expressions. 2. For equivalent expression s explored during the verification process, we can share the common sub-expression structures and form a formal shared expression graph. We can furthermore reduce the storage size of the evolved expressions and facilitate isomorphism checking between them to improve performance. 3. In the shared expression graph, we can match its sub-expressions against axiom patterns and derive corresponding unification. Then, substitute the matched sub-expression with the corresponding axiom template with unified variable values and form a new equivalent expression graph from axiom transformation. We carried out experiments of this expression equivalence verification method. Experimental results shows that this method obtains the equivalence verification capability to be applied between a hardware system design and its low level design.

Thesis (M.Sc.) - Carleton University, 2006. / Includes bibliographical references (p. 70-71). Also available in electronic format on the Internet.

The purpose of this paper is to develop the Peano postulates from a weaker axiom system than the system used by John L. Kelley in General Topology. The axiom of regularity which states "If X is a non-empty set, then there is a member Y of X such that the intersection of X and Y is empty." is not assumed in this thesis. The axiom of amalgamation which states "If X is a set, then the union of the elements of X is a set." is also not assumed. All other axioms used by Kelley relevant to the Peano postulates are assumed. The word class is never used in the thesis, though the variables can be interpreted as classes.

The purpose of this paper is to investigate Saunders MacLane's axioms for plane geometry. The wording of the axioms has been modified; however, the concept suggested by each axiom remains the same.

This thesis concerns two-point sets, which are subsets of the real plane which intersect every line in exactly two points. The existence of two-point sets was first shown in 1914 by Mazukiewicz, and since this time, the properties of these objects have been of great intrigue to mathematicians working in both topology and set theory. Arguably, the most famous problem about two-point sets is concerned with their so-called "descriptive complexity"; it remains open, and it appears to be deep. An informal interpretation of the problem, which traces back at least to Erdos, is: The term "two-point" set can be defined in a way that it is easily understood by someone with only a limited amount of mathemat- ical training. Even so, how hard is it to construct a two-point set? Can one give an effective algorithm which describes precisely how to do so? More formally, Erdos wanted to know if there exists a two-point set which is a Borel subset of the plane. An essential tool in showing the existence of a two-point set is the Axiom of Choice, an axiom which is taken to be one of the basic truths of mathematics.

Thesis (Ph. D.)--West Virginia University, 2001. / Title from document title page. Document formatted into pages; contains iv, 60 p. Includes abstract. Includes bibliographical references (p. 64-66).

No description available.

In this paper several equivalences of the axiom of choice are examined. In particular, the axiom of choice, Zorn's lemma, Tukey's lemma, the Hausdorff maximal principle, and the well-ordering theorem are shown to be equivalent. Cardinal and ordinal number theory is also studied. The Schroder-Bernstein theorem is proven and used in establishing order results for cardinal numbers. It is also demonstrated that the first uncountable ordinal space is unique up to order isomorphism. We conclude by encountering several applications of the axiom of choice. In particular, we show that every vector space must have a Hamel basis and that any two Hamel bases for the same space must have the same cardinality. We establish that the Tychonoff product theorem implies the axiom of choice and see the use of the axiom of choice in the proof of the Hahn- Banach theorem.

This thesis Models of Lobachevskij's geometry and the possibilities of their use at secondary school focuses on one kind of non-Euclidean geometries, the Bolyai - Lobachevskij's geometry. The first chapter describes the history of non-Euclidean geometry, shows difficulties of understanding of one publication dedicated to these problems by current students of secondary schools and shows some chosen methods in the didactics of mathematics, especialy the constructivist method. The second chapter is dedicated to elemental concepts of projective geometry, Bolyai - Lobachevskij's geometry and it shows its basic models. It further analyses the specific features of this kind of geometry in Beltrami - Klein's model, especially mutual positions of straight lines. This theses further contains a set of gradual tasks. The third chapter is dedicated to the description of a didactical experiment. In this experiment were students of secondary school acquainted with this theory and tasks, which they solved. Student's solution were writen down and than analysed in the constructivist methodology term in the didactics of mathematics.

Axiom pinpointing has been introduced in description logics (DLs) to help the user to understand the reasons why consequences hold and to remove unwanted consequences by computing minimal (maximal) subsets of the knowledge base that have (do not have) the consequence in question. The pinpointing algorithms described in the DL literature are obtained as extensions of the standard tableau-based reasoning algorithms for computing consequences from DL knowledge bases. Although these extensions are based on similar ideas, they are all introduced for a particular tableau-based algorithm for a particular DL. The purpose of this paper is to develop a general approach for extending a tableau-based algorithm to a pinpointing algorithm. This approach is based on a general definition of „tableau algorithms,' which captures many of the known tableau-based algorithms employed in DLs, but also other kinds of reasoning procedures.