In this paper we present a theory of proof nets for full multiplicative linear logic, including the two units. It naturally extends the well-known theory of unit-free multiplicative proof nets. A linking is no longer ...
详细信息
ISBN:
(纸本)3540230246
In this paper we present a theory of proof nets for full multiplicative linear logic, including the two units. It naturally extends the well-known theory of unit-free multiplicative proof nets. A linking is no longer a set of axiom links but a tree in which the axiom links are subtrees. these trees will be identified according to an equivalence relation based on a simple form of graph rewriting. We show the standard results of sequentialization and strong normalization of cut elimination. Furthermore, the identifications enforced on proofs are such that the proof nets, as they are presented here, form the arrows of the free (symmetric) *-autonomous category.
We investigate the logical aspects of the partial A-calculus with equality, exploiting an equivalence between partial A-theories and partial cartesian closed categories (pcccs) established here. the partial A-calculus...
详细信息
ISBN:
(纸本)3540230246
We investigate the logical aspects of the partial A-calculus with equality, exploiting an equivalence between partial A-theories and partial cartesian closed categories (pcccs) established here. the partial A-calculus with equality provides a full-blown intuitionistic higher order logic, which in a precise sense turns out to be almost the logic of toposes, the distinctive feature of the latter being unique choice. We give a linguistic proof of the generalization of the fundamental theorem of toposes to pcccs with equality;type theoretically, one thus obtains that the partial A-calculus with equality encompasses a Martin-Lof-style dependent type theory. this work forms part of the semantical foundations for the higher order algebraic specification language HASCASL.
Classical linear-time temporal logic (LTL) is capable of specifying of and reasoning about infinite behaviors only. While this is appropriate for specifying non-terminating reactive systems, there are situations (e. g...
详细信息
ISBN:
(纸本)3540230246
Classical linear-time temporal logic (LTL) is capable of specifying of and reasoning about infinite behaviors only. While this is appropriate for specifying non-terminating reactive systems, there are situations (e. g., assume-guarantee reasoning, run-time verification) when it is desirable to be able to reason about finite and infinite behaviors. We propose an interpretation of the operators of LTL on finite and infinite behaviors, which defines an intuitionistic temporal logic (ILTL). We compare the expressive power of LTL and ILTL. We demonstrate that ILTL is suitable for assume-guarantee reasoning and for expressing properties that relate finite and infinite behaviors. In particular, ILTL admits an elegant logical characterization of safety and liveness properties.
this paper reports on the results of the Fifthinternational Workshop on Object-Oriented Reengineering in Oslo on June 15, 2004. It enumerates the presentations made, classifies the contributions and lists the main re...
详细信息
ISBN:
(纸本)354023988X
this paper reports on the results of the Fifthinternational Workshop on Object-Oriented Reengineering in Oslo on June 15, 2004. It enumerates the presentations made, classifies the contributions and lists the main results of the discussions held at the workshop. As such it provides the context for future workshops around this topic.
the proceedings contains 13 papers from the conference on Ninthinternational Workshop on High-Level Parallel programming Models and Supportive Environments. the topics discussed include: the multiloop programming con...
详细信息
the proceedings contains 13 papers from the conference on Ninthinternational Workshop on High-Level Parallel programming Models and Supportive Environments. the topics discussed include: the multiloop programming construct;modeling master-worker application in POETRIES;abstraction for dynamic data distribution;the cascade high productivity language;techniques for wrapping scientific application to CORBA components;arches: an infrastructure for PSE development and DCA: a distributed CCA framework based on MPI.
Preference elicitation is a serious bottleneck in many decision support applications and agent specification tasks. Ceteris paribus (CP)-nets were designed to make the process of preference elicitation simpler and mor...
详细信息
Preference elicitation is a serious bottleneck in many decision support applications and agent specification tasks. Ceteris paribus (CP)-nets were designed to make the process of preference elicitation simpler and more intuitive for lay users by graphically structuring a set of CP preference statements-preference statements that most people find natural and intuitive. Beside their usefulness in the process of preference elicitation, CP-nets support efficient optimization algorithms that are crucial in most applications (e. g., the selection of the best action to execute or the best product configuration). In various contexts, CP-nets with an underlying cyclic structure emerge naturally. Often, they are inconsistent according to the current semantics, and the user is required to revise them. In this paper, we show how optimization queries can be meaningfully answered in many "inconsistent" networks without troubling the user with requests for revisions. In addition, we describe a method for focusing the user's revision process when revisions are truly needed. In the process, we provide a formal semantics that justifies our approach and new techniques for computing optimal outcomes. Some of the methods we use are based on a reduction to the problem of computing stable models for nonmonotonic logic programs, and we explore this relationship closely.
As early as the 1960s, Slovenia, one of the former Yugoslav republics, had already recognized computer science as being the most prospective technology. the World Computer Congress (WCC) held in Ljubljana in 1971, pla...
详细信息
ISBN:
(纸本)1402081359
As early as the 1960s, Slovenia, one of the former Yugoslav republics, had already recognized computer science as being the most prospective technology. the World Computer Congress (WCC) held in Ljubljana in 1971, played a very important role in the promotion of computer science. Slovenian school authorities enjoyed relative autonomy in the former Yugoslavia and this made it possible for them to promote computer education. they also had strong support from civil society. this expressed orientation towards an information society was one of the major differences between Slovenia and the rest of the former Yugoslavia and one of the causes contributing to the attainment of Slovenia's independence.
An optimal design method for magnets with double-layered coaxial coils to generate a uniform central magnetic field and a small stray magnetic field has been proposed. To find the optimal current density distribution,...
详细信息
An optimal design method for magnets with double-layered coaxial coils to generate a uniform central magnetic field and a small stray magnetic field has been proposed. To find the optimal current density distribution, we used linear programming with constraints on the multipole field strengths, computed with analytical formulae, of the central and stray fields. the final coil positions were optimized with a quasi-Newton method, again taking into account the inner and outer multipole field strengths.
In this paper, we propose an access control model that is suitable for a distributed object oriented environment. Our model has two features: authentication with object properties and method categorization by a securi...
详细信息
ISBN:
(纸本)0769520510
In this paper, we propose an access control model that is suitable for a distributed object oriented environment. Our model has two features: authentication with object properties and method categorization by a security level. the object property is meta information of a client, and the client is vested with it in advance. To use the object properties, a server can identify a huge number of clients in the environment by groups that is categorized withthe object properties of the clients. And also, to use a combination of multiple object properties in authentication, an administrator of the server can determine the flexible range of target clients. the security level shows how much impact the method affects server's data. If a designer of the server categorizes the server's methods with a security level, an administrator of the server can set an authorization rule to each category instead of each server's method. the categories constitute a tree structure, since a parent category includes child categories. As a result of this, the administrator can set an authorization rule easier than authorization without categorization by the security level. Furthermore, we implemented above the access control model and we evaluated their efficiency.
We have developed a new magnet for open high field (0.7 T) MRI systems. Since MRI systems are installed in hospital sites, it is important to reduce stray magnetic fields of the magnets. We studied passive, active and...
详细信息
We have developed a new magnet for open high field (0.7 T) MRI systems. Since MRI systems are installed in hospital sites, it is important to reduce stray magnetic fields of the magnets. We studied passive, active and hybrid shielding methods and compared them. In order to study feasibility of active shielding, we considered higher order multipole stray fields. We present details of the calculation method and the results.
暂无评论