Intensional sets are sets given by a property rather than by enumerating their elements, similar to set comprehensions available in specification languages such as B and MiniZinc. In a previous paper [3] we have prese...
详细信息
The proceedings contain 6 papers. The topics discussed include: solving set constraints in B and event-B: foundations and applications;encoding sets as real numbers;programming in Java with restricted intensional sets...
The proceedings contain 6 papers. The topics discussed include: solving set constraints in B and event-B: foundations and applications;encoding sets as real numbers;programming in Java with restricted intensional sets;towards Coq formalisation of {log} set constraints resolution;on perfect matchings for some bipartite graphs;a set-based reasoner for the description logic DL4,x D;and polarized rewriting and tableaux in B set theory.
An experiment is described that confirms the security of a well-studied class of cryptographic protocols (Dolev-Yao intruder model) can be verified by two-way nondeterministic pushdown automata (2NPDA). A nondetermini...
详细信息
An experiment is described that confirms the security of a well-studied class of cryptographic protocols (Dolev-Yao intruder model) can be verified by two-way nondeterministic pushdown automata (2NPDA). A nondeterministic pushdown program checks whether the intersection of a regular language (the protocol to verify) and a given Dyck language containing all canceling words is empty. If it is not, an intruder can reveal secret messages sent between trusted users. The verification is guaranteed to terminate in cubic time at most on a 2NPDA-simulator. The interpretive approach used in this experiment simplifies the verification, by separating the nondeterministic pushdown logic and program control, and makes it more predictable. We describe the interpretive approach and the known transformational solutions, and show they share interesting features. Also noteworthy is how abstract results from automata theory can solve practical problems by programming language means.
Quantum computing exploits quantum phenomena such as superposition and entanglement to realize a form of parallelism that is not available to traditional computing. It offers the potential of significant computational...
详细信息
ISBN:
(纸本)9781450363556
Quantum computing exploits quantum phenomena such as superposition and entanglement to realize a form of parallelism that is not available to traditional computing. It offers the potential of significant computational speed-ups in quantum chemistry, materials science, cryptography, and machine learning. The dominant approach to programming quantum computers is to provide an existing high-level language with libraries that allow for the expression of quantum programs. This approach can permit computations that are meaningless in a quantum context;prohibits succint expression of interaction between classical and quantum logic;and does not provide important constructs that are required for quantum programming. We present Q#, a quantum-focused domain-specific language explicitly designed to correctly, clearly and completely express quantum algorithms. Q# provides a type system;a tightly constrained environment to safely interleave classical and quantum computations;specialized syntax;symbolic code manipulation to automatically generate correct transformations of quantum operations;and powerful functional constructs which aid composition.
The language {log} is a Constraint logicprogramming language that natively supports finite sets and constraints such as (non) equality and (non) membership. The set constraints resolution process is mathematically fo...
详细信息
Consistency-based diagnosis is a well-known theory of diagnosis using main knowledge of the normal structure and behaviour of a system. Central in this theory is the notion of a conflict, which describes the relations...
详细信息
It is well known that the dimensions of the pelvic bones depend on the gender and vary with the age of the individual. Indeed, and as a matter of fact, this work will focus on the development of an intelligent decisio...
详细信息
ISBN:
(纸本)9781509009732
It is well known that the dimensions of the pelvic bones depend on the gender and vary with the age of the individual. Indeed, and as a matter of fact, this work will focus on the development of an intelligent decision support system to predict individual's age based on pelvis' dimensions criteria. On the one hand, some basic image processing technics were applied in order to extract the relevant features from pelvic X-rays. On the other hand, the computational framework presented here was built on top of a logicprogramming approach to knowledgerepresentation and reasoning, that caters for the handling of incomplete, unknown, or even self-contradictory information, complemented with a Case Base approach to computing.
The proceedings contain 5 papers. The topics discussed include: the structure and complexity of credal semantics;probabilistic constraint logic theories;toward computing conflict-based diagnoses in probabilistic logic...
The proceedings contain 5 papers. The topics discussed include: the structure and complexity of credal semantics;probabilistic constraint logic theories;toward computing conflict-based diagnoses in probabilistic logicprogramming;sampling random bioinformatics puzzles using adaptive probability distributions;and notes on the implementation of FAM.
This paper presents implementation and optimization techniques to support objects in Ikra, an array-based parallel extension to Ruby with dynamic compilation. The high-level goal of Ikra is to allow developers to expl...
详细信息
ISBN:
(纸本)9781450343848
This paper presents implementation and optimization techniques to support objects in Ikra, an array-based parallel extension to Ruby with dynamic compilation. The high-level goal of Ikra is to allow developers to exploit GPU-based high-performance computing without paying much attention to intricate details of the underlying GPU infrastructure and CUDA. Ikra supports dynamically-typed object-oriented programming in Ruby and performs a number of optimizations. It supports parallel operations (e.g., map, each) on arrays of polymorphic objects, allowing polymorphic method calls inside a kernel by compiling them to conditional branches. To reduce branch divergence, Ikra shuffles thread assignments to base array elements based on runtime types of elements. To facilitate memory coalescing, Ikra stores objects in a structure-of-arrays (SoA) representation (columnar object layout). To eliminate intermediate data in global memory, Ikra merges cascaded parallel sections into one kernel using symbolic execution. Copyright is held by the owner/author(s). Publication rights licensed to ACM.
the proceedings contain 8 papers. The topics discussed include: appropriate design guided by simulation: an hovercraft application;intelligent agent-based stimulation for testing robotic software in human-robot intera...
ISBN:
(纸本)9781450342599
the proceedings contain 8 papers. The topics discussed include: appropriate design guided by simulation: an hovercraft application;intelligent agent-based stimulation for testing robotic software in human-robot interactions;model-driven structural and statistical testing of robot cooperation and reconfiguration;stochastic error propagation analysis of model-driven space robotic software implemented in Simulink;multi-agent plan verification with answer set programming;a knowledge-based architecture supporting declarative action representation for manipulation of everyday objects;and robot quarter 4.0: an urban testground for living, learning, and working with service robots.
暂无评论