The compositionality of the semantics of logic programs with respect to (different varieties of) program union has been studied recently by a number of researchers. The approaches used can be considered quite ad hoc i...
详细信息
The compositionality of the semantics of logic programs with respect to (different varieties of) program union has been studied recently by a number of researchers. The approaches used can be considered quite ad hoc in the sense that they provide, from scratch, the semantic constructions needed to ensure compositionality and, in some cases, full abstraction in the given framework. In this paper, we study the application of general algebraic methods for obtaining, systematically, this kind of results. In particular, the method proposed consists in studying the adequate institution for describing the given class of logic programs and, then, in using general institution-independent results to prove compositionality and full abstraction. This is done in detail for the class of definite logic programs with respect to three kinds of composition operations: Omega-union, standard union and module composition. In addition two different institutions are considered: the standard institution of Horn clause logic and a new institution that better captures the input/output operational behaviour of logic programs. Finally, a similar solution is sketched for other classes of logic programs.
In this paper we present a model transformation language based on logic programming. The language, called PTL (Prolog based Transformation Language), can be considered as a hybrid language in which ATL (Atlas Transfor...
详细信息
In this paper we present a model transformation language based on logic programming. The language, called PTL (Prolog based Transformation Language), can be considered as a hybrid language in which ATL (Atlas Transformation Language)-style rules are combined with logic rules for defining transformations. ATL-style rules are used to define mappings from source models to target models while logic rules are used as helpers. The implementation of PTL is based on the encoding of the ATL-style rules by Prolog rules. Thus, PTL makes use of Prolog as a transformation engine. We have provided a declarative semantics to PTL and proved the semantics equivalent to the encoded program. We have studied an encoding of OCL (Object Constraint Language) with Prolog goals in order to map ATL to PTL. Thus a subset of PTL can be considered equivalent to a subset of ATL. The proposed language can be also used for model validation, that is, for checking constraints on models and transformations. We have equipped our language with debugging and tracing capabilities which help developers to detect programming errors in PTL rules. Additionally, we have developed an Eclipse plugin for editing PTL programs, as well as for debugging, tracing and validation. Finally, we have evaluated the language with several transformation examples as well as tested the performance with large models. (C) 2015 Elsevier Inc. All rights reserved.
A temporal-constraint logic programming framework for the specification and automatic verification and synthesis of assembly sequences is developed. The implemented tool is based on the formulated and derived preceden...
详细信息
A temporal-constraint logic programming framework for the specification and automatic verification and synthesis of assembly sequences is developed. The implemented tool is based on the formulated and derived precedence properties for a general mechanical assembly. This tool, called the Mechanical Assembly Sequence Satisfiability Checker (MASS-C), supports the use of a subset of temporal logic for assembly constraint specification. MASS-C provides the logic programming framework by which the designer can be relieved of the tedium of finding the assembly sequences, and the assembly sequence planning process manifests itself in the implicit modelling of assembly sequences by acquiring and formulating the set of correct and complete assembly constraints as a logic program. MASS-C implements a class of temporal expressions as predicates for logic programming of assembly constraints. It provides facilities to either verify an assembly sequence or synthesise all assembly sequences that satisfy the specified constraints composed as a logic program. Two examples illustrate the use of MASS-C for such verification and synthesis.
We are proud to introduce this special issue of the Journal of Theory and Practice of logic programming (TPLP), dedicated to the full papers accepted for the 28th International Conference on logic programming (ICLP). ...
详细信息
We are proud to introduce this special issue of the Journal of Theory and Practice of logic programming (TPLP), dedicated to the full papers accepted for the 28th International Conference on logic programming (ICLP). The ICLP meetings started in Marseille in 1982 and since then constitute the main venue for presenting and discussing work in the area of logic programming.
We propose a logic-independent approach to logic programming through which the paradigm as we know it for Horn-clause logic can be explored for other formalisms. Our investigation is based on abstractions of notions s...
详细信息
We propose a logic-independent approach to logic programming through which the paradigm as we know it for Horn-clause logic can be explored for other formalisms. Our investigation is based on abstractions of notions such as logic program, clause, query, solution and computed answer, which we develop over Goguen and Burstall's theory of institutions. These give rise to a series of concepts that formalize the interplay between the denotational and the operational semantics of logic programming. We examine properties concerning the satisfaction of quantified sentences, discuss a variant of Herbrand's theorem that is not limited in scope to any particular logical system or construction of logic programs, and describe a general resolution-based procedure for computing solutions to queries. We prove that this procedure is sound;moreover, under additional hypotheses that reflect faithfully properties of actual logic-programming languages, we show that it is also complete.
Abstract interpretation is a systematic methodology to design static program analysis which has been studied extensively in the logic programming community, because of the potential for optimizations in logic programm...
详细信息
Abstract interpretation is a systematic methodology to design static program analysis which has been studied extensively in the logic programming community, because of the potential for optimizations in logic programming compilers and the sophistication of the analyses which require conceptual support. With the emergence of efficient generic abstract interpretation algorithms for logic programming, the main burden in building an analysis is the abstract domain which gives a safe approximation of the concrete domain of computation. However, accurate abstract domains for logic programming are often complex not only because of the relational nature of logic programming languages and of their typical interprocedural control-flow, but also because of the variety of analyses to perform, their interdependence, and the need to maintain structural information. The purpose of this paper is to propose conceptual and software support for the design of abstract domains. It contains two main contributions: the notion of open product and a generic pattern domain. The open product is a new, language independent, way of combining abstract domains allowing each combined domain to benefit from information from the other components through the notions of queries and open operations. It provides a framework to approximate Cousots' reduced product, while reusing existing implementations and providing methodological guidance on how to build domains for interaction and composition. It is orthogonal and complementary to Granger's product which improves the direct product by a decreasing iteration sequence based on refinements but lets the domains interact only after the individual operations. The generic pattern domain Pat(R) automatically upgrades a domain D with structural information yielding a more accurate domain Pat(D) without additional design or implementation cost. The two contributions are orthogonal and can be combined in various ways to obtain sophisticated domains while imposin
Constraint logic programming (CLP) is a general scheme for extending logic programming to include constraints. It is parametrized by D, the domain of the constraints. However, CLP(D) languages, as well as most other c...
详细信息
Constraint logic programming (CLP) is a general scheme for extending logic programming to include constraints. It is parametrized by D, the domain of the constraints. However, CLP(D) languages, as well as most other constraint systems, only allow the programmer to specify constraints that must hold. In many applications, such as interactive graphics, planning, document formatting, and decision support, one needs to express preferences as well as strict requirements. If we wish to make full use of the constraint paradigm, we need ways to represent these defaults and preferences declaratively, as constraints, rather than encoding them in the procedural parts of the language. We describe a scheme for extending CLP(D) to include both required and preferential constraints. An arbitrary number of strengths of preference are allowed. We present a theory of such constraint hierarchies, and an extension, hierarchical constraint logic programming (HCLP), of the CLP scheme to include constraint hierarchies. We give an operational, model theoretic, and fixed-point semantics for the HCLP scheme. Finally, we describe two interpreters we have written for instances of the HCLP scheme, give example programs, and discuss related work.
At present, the search for specific information on the World Wide Web is faced with several problems, which arise on the one hand from the vast number of information sources available, and on the other hand, from thei...
详细信息
At present, the search for specific information on the World Wide Web is faced with several problems, which arise on the one hand from the vast number of information sources available, and on the other hand, from their intrinsic heterogeneity, since standards are missing. A promising approach for solving the complex problems emerging in this context is the use of multi-agent systems of information agents, which cooperatively solve advanced information-retrieval problems. This requires advanced capabilities to address complex tasks, such as search and assessment of information sources, query planning, information merging and fusion, dealing with incomplete information, and handling of inconsistency. In this paper, our interest lies in the role which some methods from the field of declarative logic programming can play in the realization of reasoning capabilities for information agents. In particular, we are interested to see how they can be used, extended, and further developed for the specific needs of this application domain. We review some existing systems and current projects, which typically address information-integration problems. We then focus on declarative knowledge-representation methods, and review and evaluate approaches and methods from logic programming and nonmonotonic reasoning for information agents. We discuss advantages and drawbacks, and point out the possible extensions and open issues.
作者：
DARVAS, FUNIV FLORIDA
J HILLIS MILLER HLTH CTRCOLL PHARMCTR DRUG DESIGN & DELIVERYGAINESVILLEFL 32610
This paper discusses logic programming and its application for the expert system I use to simulate the metabolic fate of substances. An expert system called Metabolexpert accepts the formula of the compound to be meta...
详细信息
This paper discusses logic programming and its application for the expert system I use to simulate the metabolic fate of substances. An expert system called Metabolexpert accepts the formula of the compound to be metabolized and produces a treelike picture of the metabolites generated together with the formula of the compounds. On request, three-dimensional (3D) pictures of the metabolites are also displayed and hydrophobicity (logP) values of the compounds calculated. A retrospective investigation of Metabolexpert's achievement showed that the expert system can reproduce almost all primary, secondary and tertiary metabolites of amphetamine. A compound series has been suggested for benchmark testing of metabolic transformation knowledge bases.
The inclusion of universal quantification and a form of implication in goals in logic programming is considered. These additions provide a logical basis for scoping, but they also raise new implementation problems. Wh...
详细信息
The inclusion of universal quantification and a form of implication in goals in logic programming is considered. These additions provide a logical basis for scoping, but they also raise new implementation problems. When universal and existential quantifiers are permitted to appear in mixed order in goals, the devices of logic variables and unification that are employed in solving existential goals must be modified to ensure that constraints arising out of the order of quantification are respected. Suitable modifications that are based on attaching numerical tags to constants and variables and on using these tags in unification are described. The resulting devices are amenable to an efficient implementation and can, in fact, be assimilated easily into the usual machinery of the Warren Abstract Machine (WAM). The provision of implications in goals results in the possibility of program clauses being added to the program for the purpose of solving specific subgoals. A naive scheme based on asserting and retracting program clauses does not suffice for implementing such additions for two reasons. First, it is necessary to also support the resurrection of an earlier existing program in the face of backtracking. Second, the possibility for implication goals to be surrounded by quantifiers requires a consideration of the parameterization of program clauses by bindings for their free variables. Devices for supporting these additional requirements are described as also is the integration of these devices into the WAM. Further extensions to the machine are outlined for handling higher-order additions to the language. The ideas presented here are relevant to the implementation of the higher-order logic programming language lambda Prolog.
暂无评论