In this paper we present goal-directed deduction methods for Lukasiewicz infinite-valued logic L, giving logicprogramming style algorithms which both have a logical interpretation and provide a suitable basis for imp...
详细信息
ISBN:
(纸本)3540230246
In this paper we present goal-directed deduction methods for Lukasiewicz infinite-valued logic L, giving logicprogramming style algorithms which both have a logical interpretation and provide a suitable basis for implementation. We begin by considering a basic version with connections to calculi for other logics, then make refinements to obtain greater efficiency and termination properties, and to deal with further connectives and truth constants. We finish by considering applications of these algorithms to fuzzy logicprogramming.
A tableau calculus for a logic with constructive negation and an implementation of the related decision procedure is presented. this logic is an extension of Nelson logic and it has been used in the framework of progr...
详细信息
ISBN:
(纸本)3540230246
A tableau calculus for a logic with constructive negation and an implementation of the related decision procedure is presented. this logic is an extension of Nelson logic and it has been used in the framework of program verification and timing analysis of combinatorial circuits. the decision procedure is tailored to shrink the search space of proofs and it is proved correct by using a semantical technique. It has been implemented in C++ language.
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 the refinement calculus, monotonic predicate transformers are used to model specifications for (imperative) programs. Together with a natural notion of simulation, they form a category enjoying many algebraic prope...
详细信息
ISBN:
(纸本)3540230246
In the refinement calculus, monotonic predicate transformers are used to model specifications for (imperative) programs. Together with a natural notion of simulation, they form a category enjoying many algebraic properties. We build on this structure to make predicate transformers into a denotational model of full linear logic: all the logical constructions have a natural interpretation in terms of predicate transformers (i.e. in terms of specifications). We then interpret proofs of a formula by a safety property for the corresponding specification.
the aim of this work is to describe a tool (Spi2Java) that automatically generates Java code implementing cryptographic protocols described in the formal specification language spi calculus. Spi2Java is part of a set ...
详细信息
ISBN:
(纸本)0769520510
the aim of this work is to describe a tool (Spi2Java) that automatically generates Java code implementing cryptographic protocols described in the formal specification language spi calculus. Spi2Java is part of a set of tools for spi calculus, also including a pre-processor a parser and a security analyzer the latter can formally analyze protocols and detect protocol flaws. When a protocol has been analyzed and an adequate confidence about its correctness has been reached, Spi2Java can generate a corresponding correct Java implementation of the protocol, thus dramatically reducing the risk of introducing security flaws in the coding phase.
Using separation logic, this paper presents three Hoare logics (corresponding to different notions of correctness) for the simple While language extended with commands for heap access and modification. Properties of s...
详细信息
ISBN:
(纸本)3540230246
Using separation logic, this paper presents three Hoare logics (corresponding to different notions of correctness) for the simple While language extended with commands for heap access and modification. Properties of separating conjunction and separating implication are mechanically verified and used to prove soundness and relative completeness of all three Hoare logics. the whole development, including a formal proof of the Frame Rule, is carried out in the theorem prover Isabelle/HOL.
Wide area network (WAN) -based distributed computing (DC) has become an active field of research, especially under the label of grid computing. On the other hand, research on WAN-based real-time (RT) DC has remained i...
详细信息
ISBN:
(纸本)0769520510
Wide area network (WAN) -based distributed computing (DC) has become an active field of research, especially under the label of grid computing. On the other hand, research on WAN-based real-time (RT) DC has remained in an embryonic stage. the situation is changing, however. Continuous increase in the availability of optical channels, called lambdas, along with steady decrease of their costs, have given rise to efforts to establish optical network infrastructure in which the possibility of dynamically allocating entire end-to-end light-paths to different message streams created by a moderate number of important applications is real. With such infrastructure there is no major obstacle in facilitating RT DC. the notion of RT distributed virtual computer (DVC), which can also be viewed as an RT sub-grid, is introduced. then the challenging issues in adapting some promising technologies established for RT DC in LAN environments to enable realization of RT DVCs in WAN environments are discussed. programming model and resource management are the focus of the discussion.
the aim of this work is to give an alternative presentation for the multiplicative fragment of Yetter's cyclic linear logic. the new presentation is inspired by the calculus of structures, and has the interesting ...
详细信息
ISBN:
(纸本)3540230246
the aim of this work is to give an alternative presentation for the multiplicative fragment of Yetter's cyclic linear logic. the new presentation is inspired by the calculus of structures, and has the interesting feature of avoiding the cyclic rule. the main point in this work is to show how cyclicity can be substituted by deepness, i.e. the possibility of applying an inference rule at any point of a formula. We finally derive, through a new proof technique, the cut elimination property of the calculus.
We have developed a new magnet for open high field (0.7 T) MRI systems. In order to homogenize magnetic fields in the field of view, an optimization method to determine initial configurations of large correction iron ...
详细信息
We have developed a new magnet for open high field (0.7 T) MRI systems. In order to homogenize magnetic fields in the field of view, an optimization method to determine initial configurations of large correction iron pieces was developed. In our method, we combined linear programming (LP) and 3D magnetic FEA and, using analytic formulae for LP, we computed field harmonics due to the volume of magnetized iron.
Reconfigurable computing requires organizing computation with mixtures of processors and discrete logicthus presenting a difficult problem of hardware/software integration. An execution model and adaptation of functi...
详细信息
ISBN:
(纸本)0769521320
Reconfigurable computing requires organizing computation with mixtures of processors and discrete logicthus presenting a difficult problem of hardware/software integration. An execution model and adaptation of functional programming is proposed which removes the distinction between hardware and software while offering the possibility of "correct by construction" design. the resulting language is called "V" because one way of creating it is to begin withthe verifiable, synthesizable subset of Verilog, and then add functional programming features. V generates the net-list of elementary functions which are supported by an array. the compiler has stages of compilation and instantiation so that recursion can be supported in the early definition of a design. the execution model is cycle based synchronous dataflow. V syntax looks much like Verilog or C without pointers in order to facilitate adoption.
暂无评论