We present an overview on the AT(x) approach which is capable of automatically analyzing programs with respect to given tests and a reference solution. In the context of small homework assignments with precisely descr...
详细信息
ISBN:
(纸本)3540255605
We present an overview on the AT(x) approach which is capable of automatically analyzing programs with respect to given tests and a reference solution. In the context of small homework assignments with precisely describable tasks, AT(P), a Prolog instance of the general AT(x) framework, is able to find many of the errors usually made by students and to communicate them in a manner understandable for beginners in Prolog programming. the system is being used in distance education where direct communication between students and tutors is most of the time not possible.
Recent progress of VR (Virtual Reality) technologies makes it possible to realize the VR space that is synchronized withthe real space. We can hereby build virtual workspace through which a worker in real workspace c...
详细信息
ISBN:
(纸本)3540255605
Recent progress of VR (Virtual Reality) technologies makes it possible to realize the VR space that is synchronized withthe real space. We can hereby build virtual workspace through which a worker in real workspace can automatically acquire and invoke appropriate plant maintenance agents. We propose spatial programming which is a manner of VR programming technique, locating various place-dependent agents and web information in VR space, and also describe the interface between agent world and real workspace as an application of spatial programming, towards ubiquitous maintenance.
the new generic scheme CFLP(D) has been recently proposed in [14] as a logical and semantic framework for lazy constraintfunctionallogicprogramming over a parametrically given constraint domain D. Further, [15] pre...
详细信息
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.
Summary form only given. Conforming to the underlying memory consistency rules is a fundamental requirement for implementing shared memory systems and developing multiprocessor programs. In order to promote understand...
详细信息
Summary form only given. Conforming to the underlying memory consistency rules is a fundamental requirement for implementing shared memory systems and developing multiprocessor programs. In order to promote understanding and enable automated verification, it is highly desirable that a memory model specification be both declarative and executable. We present a specification framework called Nemos (Nonoperational yet Executable Memory Ordering Specifications), which supports precise specification and automatic execution in the same framework. We employ a uniform notation based on predicate logic to define shared memory semantics in an axiomatic as well as compositional style. We also apply constraintlogicprogramming and SAT solving to make the axiomatic specifications executable for memory model analysis. To illustrate our approach, we formalize a collection of classical memory models, including sequential consistency, coherence, PRAM, causal consistency, and processor consistency.
In this paper, we present an abstract framework for learning a finite domain constraint solver modeled by a set of operators enforcing a consistency. the behavior of the consistency to be learned is taken as the set o...
详细信息
In this paper, we present an abstract framework for learning a finite domain constraint solver modeled by a set of operators enforcing a consistency. the behavior of the consistency to be learned is taken as the set of examples on which the learning process is applied. the best possible expression of this operator in a given language is then searched. We instantiate this framework to the learning of bound-consistency in the indexical language of Gnu-Prolog.
the proceedings contain 22 papers. the special focus in this conference is on Debugging and types, Tabling and constraints, Abstract interpretation, Program refinement, Verification, Partial evaluation and Rewriting a...
ISBN:
(纸本)9783540404385
the proceedings contain 22 papers. the special focus in this conference is on Debugging and types, Tabling and constraints, Abstract interpretation, Program refinement, Verification, Partial evaluation and Rewriting and object-oriented development. the topics include: Abstract diagnosis of functional programs;a cut-free sequent calculus for pure type systems verifying the structural rules of gentzen/kleene;constraint solver synthesis using tabled resolution for constraintlogicprogramming;translating datalog-like optimization queries into ILOG programs;tabling structures for bottom-up logicprogramming;towards optimal operators for sharing properties;two variables per linear inequality as an abstract domain;convex hull abstractions in specialization of CLP programs;collecting potential optimisations;an operational approach to program extraction in the calculus of constructions;refinement of higher-order logic programs;a generic program for minimal subsets with applications;justification based on program transformation;combining logic programs and monadic second order logics by program transformation;verification in ACL2 of a generic framework to synthesize SAT-provers;a proof system for information flow security;forward slicing of multi-paradigm declarative programs based on partial evaluation;a fixed point semantics for logic programs extended with cuts;abstract partial deduction challenged;towards correct object-oriented design frameworks in computational logic;mapping modular SOS to rewriting logic and program synthesis based on the equivalent transformation computation model.
We provide here a declarative and model-theoretic characterization of the approximations computed by consistency during the resolution of finite domain constraint satisfaction problems.
ISBN:
(纸本)3540439307
We provide here a declarative and model-theoretic characterization of the approximations computed by consistency during the resolution of finite domain constraint satisfaction problems.
暂无评论