Displaying similar documents to “The Formalization of Decision-Free Petri Net”

Pickup and delivery problem with split demand and transfers

Jan Pelikán (2013)

Kybernetika

Similarity:

We deal with a logistic problem motivated by a case study from a company dealing with inland transportation of piece goods in regular cycles. The problem consists in transportation of goods among regional centres – hubs of a network. Demands on transportation are contained in a matrix of flows of goods between pairs of hubs. The transport is performed by vehicles covering the shipping demands and the task is to design a cyclical route and to place a depot for each vehicle. The route...

Beta-reduction as unification

A. Kfoury (1999)

Banach Center Publications

Similarity:

We define a new unification problem, which we call β-unification and which can be used to characterize the β-strong normalization of terms in the λ-calculus. We prove the undecidability of β-unification, its connection with the system of intersection types, and several of its basic properties.

On some remarkable properties of the two-dimensional Hammersley point set in base 2

Peter Kritzer (2006)

Journal de Théorie des Nombres de Bordeaux

Similarity:

We study a special class of ( 0 , m , 2 ) -nets in base 2. In particular, we are concerned with the two-dimensional Hammersley net that plays a special role among these since we prove that it is the worst distributed with respect to the star discrepancy. By showing this, we also improve an existing upper bound for the star discrepancy of digital ( 0 , m , 2 ) -nets over ℤ 2 . Moreover, we show that nets with very low star discrepancy can be obtained by transforming the Hammersley point set in a suitable way. ...

Model Checking. Part III

Kazuhisa Ishida, Yasunari Shidama (2008)

Formalized Mathematics

Similarity:

This text includes verification of the basic algorithm in Simple On-the-fly Automatic Verification of Linear Temporal Logic (LTL). LTL formula can be transformed to Buchi automaton, and this transforming algorithm is mainly used at Simple On-the-fly Automatic Verification. In this article, we verified the transforming algorithm itself. At first, we prepared some definitions and operations for transforming. And then, we defined the Buchi automaton and verified the transforming algorithm.MML...