Wyniki wyszukiwania - BazTech

1

“Small in size, but big in impact”: socio-environmental reforms for sustainable artisanal and small-scale mining

Owusu Obed, Bansah Kenneth Joseph, Mensah Albert Kobina

Journal of Sustainable Mining

|

2019

|

Vol. 18, iss. 1

38--44

EN

Artisanal and small-scale mining (ASM) - small sized, largely unrecognized, rudimentary, and an informal form of mining - occurs in more than 70 countries around the world and is mainly hailed for its socioeconomic benefits and reviled for its environmental devastation. As a result, many people are confused about the future of ASM. In Ghana, the government banned ASM in 2017 and formed a security taskforce drawn from the military and police to crack down on nomadic and local ASM workers who defy the ban. This approach is unsustainable, deals less with the fundamental problems, and increases poverty among the already impoverished local populations who depend on this type of mining as their only means of livelihood. To support the argument for sustainable reforms, revenue growth decomposition and growth accounting analyses were performed to determine the factors shaping ASM revenue over 25 years (1990-2016). Results show that production (gold output) is the most important factor that influences revenue growth from ASM, contrary to the usual view that the price of the metal is mainly responsible for the increase in revenue. Thus, increasing labor hours in ASM could significantly increase mining revenue, reduce unemployment, and improve local commerce. We strongly conclude that sustainable reforms such as increasing local participation in decision making, education and training, adoption of improved technology, strengthening regulatory institutions, legislation and enforcement of enactments, and the provision of technical support and logistics could ensure socio-environmental sustainability.

2

Algorithmic Completeness of Imperative Programming Languages

Marquer Yoann

Fundamenta Informaticae

|

2019

|

Vol. 168, nr 1

51--77

EN

According to the Church-Turing Thesis, effectively calculable functions are functions computable by a Turing machine. Models that compute these functions are called Turing-complete. For example, we know that common imperative languages (such as C, Ada or Python) are Turing complete (up to unbounded memory). Algorithmic completeness is a stronger notion than Turing-completeness. It focuses not only on the input-output behavior of the computation but more importantly on the step-by-step behavior. Moreover, the issue is not limited to partial recursive functions, it applies to any set of functions. A model could compute all the desired functions, but some algorithms (ways to compute these functions) could be missing (see [10, 27] for examples related to primitive recursive algorithms). This paper’s purpose is to prove that common imperative languages are not only Turing-complete but also algorithmically complete, by using the axiomatic definition of the Gurevich’s Thesis and a fair bisimulation between the Abstract State Machines of Gurevich (defined in [16]) and a version of Jones’ While programs. No special knowledge is assumed, because all relevant material will be explained from scratch.

3

Siting a centralised processing centre for artisanal and small-scale mining - a spatial multi-criteria approach

Amoah N., Stemn E.

Journal of Sustainable Mining

|

2018

|

Vol. 17, iss. 4

215--225

EN

Artisanal and small-scale mining is one of the global phenomena that is a threat to environmental health and safety. There are ambiguities in the manner in which an ore-processing facility operates. These ambiguities can cause environmental problems and hinder the mining capacity of these miners in Ghana. The vast majority of attempts to address these problems through the establishments of centralised processing centres have failed, with only a handful of successes. This research sought to use an established data-driven, geographic information based system to locate a centralised gold processing facility within the Wassa Amenfi-Prestea Mining Area in the Western region of Ghana. The study was designed to first determine the relevant factors that should be considered in the decision-making process for locating a centralised ore-processing facility. Secondly, it sought to implement the identified factors in a case study by identifying specific geospatial techniques that can best be applied to identify potential sites. By adopting in-depth consultations with four stakeholder groups for data collection and content analysis for data analysis, thirteen relevant factors were identified. However, in the case study, due to data unavailability, only seven of the factors were considered. Geoprocessing techniques including buffering and overlay analysis and multi-criteria decision analysis were employed to develop a model to identify the most preferred locations to site a centralised processing facility. Site characterisations and environmental considerations, incorporating identified constraints, to determine an appropriate location were selected. The final map output indicates estimated potential sites identified for the establishment of a centralised processing centre. The results obtained provide areas suitable for consideration.

4

Modyfikacja algorytmu aktywnych modeli kształtu eliminująca wpływ anizotropii danych tomograficznych

Kos A., Skalski A., Zieliński T.

Przegląd Elektrotechniczny

|

2015

|

R. 91, nr 5

41-44

PL

W artykule zaproponowano modyfikację algorytmu automatycznej segmentacji ASM, uwzględniającą anizotropię danych medycznych w reprezentacjach TK i MR na etapie generowania modelu statycznego. Przedstawiono również nową metodę generowania zbiorów punktów uczących/treningowych, wymaganych przez algorytm ASM, opartą o zmodyfikowany algorytm ICP. Zaproponowaną metodę przetestowano na testowej serii 15 rzeczywistych woluminów TK, osiągając średnią dokładność segmentacji, wyrażoną współczynnikiem Dice’a, na poziomie 0.8014.

EN

In the paper a modified ASM algorithm, that considers a CT and MRI medical data anisotropy at the stage of statistic shape model generation, is proposed. Additionally, a new, non-rigid ICP algorithm-based method of creating the ASM training data points sets is presented. The proposed approach had been tested on a series of 15 real patients CT volume data, reaching a mean accuracy of the segmentation 0.8014, measured by the Dice coefficient.

5

Dopasowanie chmur punktów do powierzchni dla potrzeb przetwarzania i analizy obrazów medycznych oraz systemów wizyjnych

Skalski A., Socha M.

Przegląd Elektrotechniczny

|

2014

|

R. 90, nr 5

160--163

PL

W artykule przedstawiono metodę dopasowania chmur punktów do powierzchni na przykładzie zagadnienia konstrukcji danych uczących w algorytmie ASM w zastosowaniu do segmentacji danych tomograficznych dla potrzeb planowania leczenia radioterapeutycznego. Zaproponowany algorytm składa się z 3 etapów: generacji chmur punktów dla danych uczących, sztywnego dopasowania (rotacji, przesunięcia) z wykorzystaniem ICP oraz lokalnej korekty wyników. Cała metodologia została przetestowana, a skuteczność oceniona na podstawie odległości punktów charakterystycznych w danych po dopasowaniu.

EN

This paper addresses a problem of automatic point clouds matching in context of training data construction in Active Shape Model algorithm. An algorithm was applied to CT data segmentation for radiotherapy planning. Proposed methodology consists of 3 steps: point clouds generation, rigid matching (rotation, translation) based on ICP and local corrections of points location. Algorithm was tested and validated using distance between points in data after matching.

6

Dekompozycja sieci działań układów sekwencyjnych w celu obniżenia poboru mocy

Bułatowa I., Salauyou V., Matujewicz P.

Pomiary Automatyka Kontrola

|

2014

|

R. 60, nr 7

501--503

PL

Opracowana została metoda syntezy układów sekwencyjnych o obniżonym poborze mocy, algorytmy sterowania których opisywane są za pomocą sieci działań. Metoda syntezy polega na dekompozycji sieci działań na fragmenty realizowane w postaci oddzielnych automatów połączonych w dwupoziomową strukturę hierarchiczną. Zmniejszenie poboru mocy osiąga się przez odłączenie sygnału synchronizacji od nieaktywnych w danym momencie automatów. Zaproponowano schemat bramkowania sygnału synchronizacji z wykorzystaniem sygnałów struktury hierarchicznej. Opracowany został algorytm dekompozycji sieci działań na fragmenty realizowane jako komponenty struktury hierarchicznej. Przeprowadzone badania potwierdziły efektywność zaproponowanej metody.

EN

In this paper a method for low-power design of hierarchical structures of sequential circuits specified by the Algorithmic State Machine (ASM) charts is presented. The proposed method uses a decomposition of the original sequential circuit into the smaller automata which are connected in a two-level hierarchical structure topology (Fig.1). A clock-gating approach [4, 5] is used to reduce power consumption of the sequential circuit. Due to this approach the power can be saved by clocking only one automaton of hierarchical structure at a time while the clock to the other automata is gated. As a result, only one automaton of hierarchical structure is active at any time while the others are idle, thus reducing the switching activity and minimizing the power dissipation. The algorithm of decomposition of the ASM chart into the fragments, which are implemented as components of a hierarchical structure, has been developed. The clockgating circuit (Fig. 2) which uses the control signals generated by the hierarchical structure is proposed. The power simulation method used to estimate the power consumption for original and decomposed circuits is described. Experimental results show that the proposed partitioning technique can reduce power consumption, on average 20.31%, over the original undecomposed circuit. An additional power saving is available by using special state encoding which reduces the switching activity of sequential circuits.

7

Formalna weryfikacja maszyny stanów z wykorzystaniem logiki temporalnej

Grobelna I.

Pomiary Automatyka Kontrola

|

2009

|

R. 55, nr 7

457-460

PL

Artykuł przedstawia koncepcję specyfikacji współbieżnego procesu sterowania cyfrowego za pośrednictwem diagramów algorytmicznych maszyn stanów ASM w języku aprobowanym przez profesjonalne narzędzie model checker. Specyfikacja może zostać następnie formalnie zweryfikowana pod kątem wymagań stawianych projektowanemu systemowi. Lista wymagań tworzona jest przy wykorzystaniu liniowej logiki temporalnej LTL. Formalna weryfikacja Model Checking polega na sprawdzeniu, czy model systemu spełnia stawiane mu wymagania. W przypadku wykrycia niespóności generowany jest odpowiedni kontrprzykład.

EN

The paper presents the formal specification method of concurrent control processes in form of algorithmic state machines ASM [5] in a language accepted by a professional model checker tool NuSMV. Basing on linear temporal logic LTL [7, 8, 9, 16] a requirement list (Fig. 6) for the system model is prepared. Formal verification Model Checking [17, 19] consists in comparison of the model description and the requirements list. If some requirements cannot be fulfilled, the appropriate counterexample is generated (Fig. 7), which allows localizing the error source. The ASM diagrams (Fig. 4) are fully determined, but they do not support modularity, that is why they are not well suited for specification of concurrent controlling processes. The paper includes a short introduction to the theory of algorithmic state machines ASM (Section 2), temporal logic (Section 3) and model checking technique (Section 4). The proposed solution is presented on an example (Section 5) of the process of controlling (partially concurrent) movements of two vehicles (Fig. 2). The formal verification method of the ASM diagrams with its advantages and disadvantages as well as the general conclusions are given at the end of the paper (Section 6).

8

Charakterystyka frakcji organicznych ścieków miejskich pod kątem modelu osadu czynnego ASM2d

Dymaczewski Z.

Przemysł Chemiczny

|

2008

|

T. 87, nr 5

440-442

9

Determinanty zarządzania przestrzenią powietrzną w wojskach lądowych

Glen A.

Zeszyty Naukowe AON

|

2002

|

nr 1(46)

149-161

EN

The article outlines and synthesises the problem situation asking a question concerning the determinants that define the problem of army airspace management, cause and condition elementary actions within this phenomenon. Solving the problem that has been formed in such a way, it has been explained that the aim can be recognised as the prime determinant conditioning elementary actions within the phenomenon of the airspace management (ASM). The functions of co-ordination, integration, supervision and Identification have been distinguished due to their contents that decide achieving the aim in ASM, in the army airspace management. The ASM system has been recognised as a subject which decides the basic actions within the ASM phenomenon. The subject of co-ordination of the army airspace users has been defined. The principal problem solving procedures in army airspace have been explained and the organisation of information flow fulfilling the requirements of all army airspace users has been presented. Defining ontological and epistemological bases of the ASM has been presented in the conclusion as necessary to develop further research tasks.