Coincidence of Vietoris and Wijsman Topologies: A New Proof

Let (X, d) be a metric space and CL(X) the family of all nonempty closed subsets of X. We provide a new proof of the fact that the coincidence of the Vietoris and Wijsman topologies induced by the metric d forces X to be a compact space. In the literature only a more involved and indirect proof using the proximal topology is known. Here we do not need this intermediate step. Moreover we prove that (X, d) is boundedly compact if and only if the bounded Vietoris and Wijsman topologies on CL(X) coincide.

Using SAT for Combinational Implementation Checking

The problem of checking whether a system of incompletely specified Boolean functions is implemented by the given combinational circuit is considered. The task is reduced to testing out if two given logical descriptions are equivalent on the domain of one of them having functional indeterminacy. We present a novel SAT-based verification method that is used for testing whether the given circuit satisfies all the conditions represented by the system of incompletely specified Boolean functions.

The Initial Stage of Teaching Proof in Mathematics Course

This article discusses techniques for organization of propaedeutic stage of teaching proof in mathematics course. It identifies types of tasks that allow students of 5–6 classes to form the ability to carry out simple proofs. This article describes each type of tasks features, it gives some examples.

Approximate Model Checking of Real-Time Systems for Linear Duration Invariants

Real-time systems are usually modelled with timed automata and real-time requirements relating to the state durations of the system are often specifiable using Linear Duration Invariants, which is a decidable subclass of Duration Calculus formulas. Various algorithms have been developed to check timed automata or real-time automata for linear duration invariants, but each needs complicated preprocessing and exponential calculation. To the best of our knowledge, these algorithms have not been implemented. In this paper, we present an approximate model checking technique based on a genetic algorithm to check real-time automata for linear durration invariants in reasonable times. Genetic algorithm is a good optimization method when a problem needs massive computation and it works particularly well in our case because the fitness function which is derived from the linear duration invariant is linear. ACM Computing Classification System (1998): D.2.4, C.3.

Zolotarev's proof of Gauss reciprocity and Jacobi symbols

2000 Mathematics Subject Classification: Primary 11A15.