Wyniki wyszukiwania - BazTech

1

A cut-free proof system for a predicate extension of the logic of provability

Tanaka Y.

Reports on Mathematical Logic

|

2018

|

Vol. 53

97--109

EN

In this paper, we introduce a proof system NQGL for a Kripke complete predicate extension of the logic GL of provability. While GL is defined by K and the L¨ob formula ✷(✷p ⊃ p) ⊃ ✷p, NQGL does not have the L¨ob formula as its axiom, but has a non-compact rule, that is, a derivation rule with countably many premises, instead. We show that NQGL enjoys cut admissibility and is complete with respect to the class of Kripke frames such that for each world, the supremum of the length of the paths from the world is finite.

2

Recursive-rule extraction algorithm with J48graft and applications to generating credit scores

Tanaka Y., Takagi T., Saito T., Iiduka H., Kikuchi H., Bologna G., Mitra S.

Journal of Artificial Intelligence and Soft Computing Research

|

2016

|

Vol. 6, No. 1

35--44

EN

The purpose of this study was to generate more concise rule extraction from the Recursive- Rule Extraction (Re-RX) algorithm by replacing the C4.5 program currently employed in Re-RX with the J48graft algorithm. Experiments were subsequently conducted to determine rules for six different two-class mixed datasets having discrete and continuous attributes and to compare the resulting accuracy, comprehensibility and conciseness. When working with the CARD1, CARD2, CARD3, German, Bene1 and Bene2 datasets, Re-RX with J48graft provided more concise rules than the original Re-RX algorithm. The use of Re-RX with J48graft resulted in 43.2%, 37% and 21% reductions in rules in the case of the German, Bene1 and Bene2 datasets compared to Re-RX. Furthermore, the Re-RX with J48graft showed 8.87% better accuracy than the Re-RX algorithm for the German dataset. These results confirm that the application of Re-RX in conjunction with J48graft has the capacity to facilitate migration from existing data systems toward new concise analytic systems and Big Data.

3

Opportunistic routing using prioritized forwarders with retransmission control

Yamazaki T., Yamamoto R., Miyoshi T., Asaka T., Tanaka Y.

Image Processing & Communications

|

2016

|

Vol. 21, no. 1

55--64

EN

In ad hoc networks, broadcastbased forwarding protocols called opportunistic routing have been proposed. In general backoff-based opportunistic routing protocols, each receiver autonomously makes a forwarding decision using a random back off time based on logical distance. However, each potential forwarder must wait for the expiration of the backoff timer before the packet forwarding. Moreover, they cannot gain forwarding path diversityinsparseenvironments. Inthispaper,we propose a novel forwarder selection method for opportunistic routing. In the proposed method, a terminal called, a prioritized forwarder, and which is selected from among neighbours and can forward packets without using the backoff time. In addition, we integrate a hop-by-hop retransmission control in the proposed method, wchich improvesthe packet transmission success rate in sparse environments. We evaluate the proposed method in comparison with the conventional protocols in computer simulations.

4

Simultaneous realization of water quality improvement and sludge sediment elimination on the aquatic environment by the continuous addition of a novel bio-catalyst, Waterkeeper

Kumazawa H., Tanaka Y.

Inżynieria i Aparatura Chemiczna

|

2010

|

Nr 3

65-66

EN

Waterkeeper is a selective bio-catalyst having both capabilities to activate effective microorganisms living in the aquatic sphere and to deactivate putrefactive and miscellaneous bacteria living there. First improvement stages of water quality by continuous addition of Waterkeeper into a typical aquatic sphere is outlined. Next, several practical examples exhibiting the simultaneous realization of water quality improvement and sludge sediment elimination are introduced.

PL

Waterkeeper jest selektywnym biokatalizatorem wykazującym zdolność do aktywowania mikroorganizmów w otoczeniu wodnym oraz deaktywacji zarówno bakterii gnilnych, jak i innych bakterii. Naszkicowano pierwszy etap poprawy jakości wody zachodzący w wyniku dodania biokatalizatora Waterkeeper. Następnie przedstawiono kilka praktycznych przykładów dowodzących jednoczesnej poprawy jakości wody i jednoczesnej eliminacji osadu.

5

Design and implementation of flexible, robust and efficient Grid-enabled hybrid QM/MD simulation

Tanaka Y., Takemiyia H., Nakada H., Sekiguchi S.

Computational Methods in Science and Technology

|

2006

|

Vol. 12, nr 1

79-87

EN

This paper describes the implementation of Grid-enabled hybrid Quantum Mechanics/Classical Molecular Dynamics (QM/MD) Simulation. The Grid-enabled QM/MD simulation is capable of (1) dynamic resource allocation and migration, (2) automatic recovery from faults, and (3) managing large number of CPUs in geographically distributed sites. In the implementation, both GridRPC and MPI are used to complement each other, that is, GridRPC allows dynamic resource allocation and migration and automatic recovery from faults while MPI provides high-performance parallel processing on each cluster. We ran the hybrid QM/MD simulation on an international Grid testbed in the Asia Pacific Region for about 52 days. The experimental results indicated that the hybrid QM/MD simulation could (1) adapt to the dynamic behavior of the simulation and can change the number of CPUs and the number of clusters, (2) adapt to unstable Grid infrastructure and recovers from faults automatically, and (3) manage hundreds to thousands of CPUs on distributed locations, and (4) survive for several weeks without interrupting manual operation. This paper reports on the details of the implementation, strategies for long-run, and experimental results.

6

Some proof systems for predicate common knowledge logic

Tanaka Y.

Reports on Mathematical Logic

|

2003

|

No. 37

79-100

EN

Common knowledge logic is a multi-modal epistemic logic with a modal operator which describes common knowledge condition. In this paper, we discuss some proof systems for the logic CKL, the predicate common knowledge logic characterized by the class of all Kripke frames with constant domains. Various systems for CKL and other related logics are surveyed by Kaneko-Nagashima-Suzuki-Tanaka, however, they did not give a proof of the completeness theorem of their main system for CKL. We first give a proof of their completeness theorem by an algebraic method. Next, we give a cut-free system for CKL, and show that the class of formulas in $\ckpl$ which have some positive occurrences of the common knowledge operator and some occurrences of knowledge operators and quantifiers is not recursively axiomatizable and its complement is recursively axiomatizable. As a corollary, we obtain a cut-free system for the predicate modal logic K with the Barcan formula.