We report on a successful experiment of computer-aided theorem discovery in the area of logicprogramming with answer set semantics. Specifically, withthe help of computers, we discovered exact conditions that captur...
详细信息
We report on a successful experiment of computer-aided theorem discovery in the area of logicprogramming with answer set semantics. Specifically, withthe help of computers, we discovered exact conditions that capture the strong equivalence between a set of a rule and the empty set, a set of a rule and another set of a rule, a set S of two rules and a subset of S with one rule, a set of two rules and a set of another rule, and a set S of three rules and a subset of S with two rules. We prove some general theorems that can help us verify the correctness of these conditions, and discuss the usefulness of our results in program simplification.
.Abstract logicprogramming is about designing logicprogramming languages via the proof theoretic notion of uniform provability. It allows the design of purely logical, very expressive logicprogramming languages, en...
详细信息
ISBN:
(纸本)3540206426
.Abstract logicprogramming is about designing logicprogramming languages via the proof theoretic notion of uniform provability. It allows the design of purely logical, very expressive logicprogramming languages, endowed with a rich meta theory. this tutorial intends to expose the main ideas of this discipline in the most direct and simple way.
this paper deals with automation of a creep-testing machine mainly dedicated to research activities. the requirements linked to the machine were established by the material science researchers. these requirements were...
详细信息
ISBN:
(纸本)9781538654132
this paper deals with automation of a creep-testing machine mainly dedicated to research activities. the requirements linked to the machine were established by the material science researchers. these requirements were then addressed to mechatronic researchers and teachers. In order to enhance the link between research activities and training in the engineering school linked to the research laboratory, students projects of Master degree driven by researchers were proposed. these projects were totally multi-disciplinary, mobilizing knowledge acquired by students during their cursus in the school. Several items were developed by students: automation, mechanics, power electronics and real-time programming.
We propose a path-based framework for deriving and simplifying source-tracking information for first-order term unification in the empty theory. Such a framework is useful for diagnosing unification-based systems, inc...
详细信息
We propose a path-based framework for deriving and simplifying source-tracking information for first-order term unification in the empty theory. Such a framework is useful for diagnosing unification-based systems, including debugging of type errors in programs and the generation of success and failure proofs in logicprogramming. the objects of source-tracking are deductions in the logic of term unification. the semantics of deductions are paths over a unification graph whose labels form the suffix language of a semi-Dyck set. Based on this idea of unification paths, two algorithms for generating proofs are presented: the first uses context-free labeled shortest-path algorithms to generate optimal (shortest) proofs in time O(n(3)) for a fixed signature, where n is the number of vertices of the unification graph. the second algorithm integrates easily with standard unification algorithms, entailing an overhead of only a constant factor, but generates non-optimal proofs. these non-optimal proofs may be further simplified by group rewrite rules. (c) 2005 Elsevier Inc. All rights reserved.
the work described here is motivated by our interest in the methodology of answer set programming (ASP). the idea of ASP is to solve a problem by writing a logic program the answer sets of which correspond to solutions.
ISBN:
(纸本)3540206426
the work described here is motivated by our interest in the methodology of answer set programming (ASP). the idea of ASP is to solve a problem by writing a logic program the answer sets of which correspond to solutions.
Building on the work of Burstall, this paper develops sound modelling and reasoning methods for imperative programs with pointers: heaps are modelled as mappings from addresses to values, and pointer structures are ma...
详细信息
Building on the work of Burstall, this paper develops sound modelling and reasoning methods for imperative programs with pointers: heaps are modelled as mappings from addresses to values, and pointer structures are mapped to higher-level data types for verification. the programming language is embedded in higher-order logic. Its Hoare logic is derived. the whole development is purely definitional and thus sound. Apart from some smaller examples, the viability of this approach is demonstrated with a non-trivial case study. We show the correctness of the Schorr-Waite graph marking algorithm and present part of its readable proof in Isabelle/HOL. (c) 2005 Elsevier Inc. All rights reserved.
Component-based Software Development (CBD) represents a paradigm shift in software development. In the tutorial I will explain what CBD is about, briefly survey current component technology, and posit that logic Progr...
详细信息
ISBN:
(纸本)3540206426
Component-based Software Development (CBD) represents a paradigm shift in software development. In the tutorial I will explain what CBD is about, briefly survey current component technology, and posit that logicprogramming can play a role in next-generation CBD. In this abstract, I give an overview of the material that I plan to cover in the tutorial.
Constraint-based synchronization pioneered by (concurrent) logic and concurrent constraint programming is a powerful mechanism for synchronizing concurrent computations. this paper describes (1) a general constraint-b...
详细信息
Today's high-speed network allows sophisticated applications of overlay networks. Meanwhile, usage of multicore processors has been spreading. the level of concurrency we need to handle has been rising rapidly, wh...
详细信息
ISBN:
(纸本)9780769532998
Today's high-speed network allows sophisticated applications of overlay networks. Meanwhile, usage of multicore processors has been spreading. the level of concurrency we need to handle has been rising rapidly, which necessitates a language that can express massive concurrency in a natural way, which can work with both tightly and loosely-coupled multiprocessor environments. this paper describes still work-in-progress design of "Overlay GHC", an overlay network programming language based on concurrent logic language GHC (Guarded Horn Clauses)[10], as a candidate for such a language.
logic Information Systems (LIS) use logic in a uniform way to describe their contents, to query it, to navigate through it, to analyze it, and to update it. they can be given an abstract specification that does not de...
详细信息
ISBN:
(纸本)3540206426
logic Information Systems (LIS) use logic in a uniform way to describe their contents, to query it, to navigate through it, to analyze it, and to update it. they can be given an abstract specification that does not depend on the choice of a particular logic, and concrete instances can be obtained by instantiating this specification with a particular logic. In fact, a logic plays in a LIS the role of a schema in data-bases. We present the principles of LIS, and a system-level implementation. We compare withthe use of logic in logicprogramming, in particular through the notions of intention and extension.
暂无评论