作者：
Morozov, AARAS
Inst Radio Engn & Elect Moscow 125009 Russia
One of the most interesting and promising approaches to programming Internet agents is logicprogramming of agents. this approach has good prospects, because the ideology and principles of logicprogramming are very c...
ISBN:
(纸本)3540206426
One of the most interesting and promising approaches to programming Internet agents is logicprogramming of agents. this approach has good prospects, because the ideology and principles of logicprogramming are very convenient for searching, recognition, and analysis of unstructured, poorly structured, and hypertext information. Many ideas and methods of logicprogramming of Internet agents based on various modifications of Prolog and non-classical logic (linear, modal, etc.) were developed during the recent decade. Nevertheless, there has been no mathematical apparatus providing sound and complete operation of logic programs in the dynamic Internet environment (i.e., under conditions of permanent update and revision of information). To solve this problem, we have created a mathematical apparatus based on the principle of repeated proving of sub-goals (so-called logical actors).
Program changes take up a substantial part of the entire programming effort. Often a preliminary step of improving the design without altering the external behaviour can be recommended. this is the idea behind refacto...
ISBN:
(纸本)3540206426
Program changes take up a substantial part of the entire programming effort. Often a preliminary step of improving the design without altering the external behaviour can be recommended. this is the idea behind refactoring, a source-to-source program transformation that recently came to prominence in the OO-community [1]. Unlike the existing results on automated program transformation, refactoring does not aim at transforming the program entirely automatically. the decision on whether the transformation should be applied and how it should be done is left to the program developer. However, providing automated support for refactoring is useful and an important challenge.
logicprogramming has been advocated as a language for system specification, especially for logical behaviours, rules and knowledge. However, modeling problems involving negation, which is quite natural in many cases,...
详细信息
ISBN:
(纸本)3540206426
logicprogramming has been advocated as a language for system specification, especially for logical behaviours, rules and knowledge. However, modeling problems involving negation, which is quite natural in many cases, is somewhat restricted if Prolog is used as the specification/implementation language. these constraints are not related to theory viewpoint, where users can find many different models withtheir respective semantics; they concern practical implementation issues. the negation capabilities supported by current Prolog systems are rather limited, and a correct and complete implementation there is not available. Of all the proposals, constructive negation [1,2] is probably the most promising because it has been proven to be sound and complete [4], and its semantics is fully compatible with Prolog’s.
We present a higher-order term indexing strategy based on substitution trees. the strategy is based in linear higher-order patterns where computationally expensive parts are delayed. Insertion of terms into the index ...
详细信息
ISBN:
(纸本)3540206426
We present a higher-order term indexing strategy based on substitution trees. the strategy is based in linear higher-order patterns where computationally expensive parts are delayed. Insertion of terms into the index is based on computing the most specific linear generalization of two linear higher-order patterns. Retrieving terms is based on matching two linear higher-order patterns. this indexing structure is implemented as part of the Twelf system to speed-up the execution of the tabled higher-logicprogramming interpreter. Experimental results show substantial performance improvements, between 100% and over 800%.
Tabling has emerged as an important evaluation technique in logicprogramming. Currently, changes to a program (due to addition/deletion of rules/facts) after query evaluation compromise the completeness and soundness...
详细信息
ISBN:
(纸本)3540206426
Tabling has emerged as an important evaluation technique in logicprogramming. Currently, changes to a program (due to addition/deletion of rules/facts) after query evaluation compromise the completeness and soundness of the answers in the tables. this paper presents incremental algorithms for maintaining the freshness of tables upon addition or deletion of facts. Our algorithms improve on existing materialized view maintenance algorithms and can be easily extended to handle changes to rules as well. We describe an implementation of our algorithms in the XSB tabled logicprogramming system. Preliminary experimental results indicate that our incremental algorithms are efficient. Our implementation represents a first step towards building a practical system for incremental evaluation of tabled logic programs.
An approach to authorization that is based on attributes of the resource requester provides flexibility and scalability that is essential in the context of large distributed systems. logicprogramming provides an eleg...
详细信息
ISBN:
(纸本)3540206426
An approach to authorization that is based on attributes of the resource requester provides flexibility and scalability that is essential in the context of large distributed systems. logicprogramming provides an elegant, expressive, and well-understood framework in which to work with attribute-based authorization policy. We summarize one specific attribute-based authorization framework built on logicprogramming: RT, a family of Role-based Trust-management languages. RT's logicprogramming foundation has facilitated the conception and specification of several extensions that greatly enhance its expressivity with respect to important security concepts such as parameterized roles, thresholds, and separation of duties. After examining language design issues, we consider the problem of assessing authorization policies with respect to vulnerability of resource owners to a variety of security risks due to delegations to other principals, risks such as undesired authorizations and unavailability of critical resources. We summarize analysis techniques for assessing such vulnerabilities.
We propose a parametric introduction of intensionally defined sets into any CLP(D) language. the result is a language CLP({D}), where constraints over sets of elements of D and over sets of sets of elements, and so on...
详细信息
ISBN:
(纸本)3540206426
We propose a parametric introduction of intensionally defined sets into any CLP(D) language. the result is a language CLP({D}), where constraints over sets of elements of D and over sets of sets of elements, and so on, can be expressed. the semantics of CLP({D}) is based on the semantics of logic programs with aggregates and the semantics of CLP over sets. We investigate the problem of constraint resolution in CLP({D}) and propose algorithms for constraints simplification.
One recent development in logicprogramming has been the application of abstract interpretation to verify the partial correctness of a logic program with respect to a given set of assertions. One approach to verificat...
详细信息
ISBN:
(纸本)3540206426
One recent development in logicprogramming has been the application of abstract interpretation to verify the partial correctness of a logic program with respect to a given set of assertions. One approach to verification is to apply forward analysis that starts with an initial goal and traces the execution in the direction of the control-flow to approximate the program state at each program point. this is often enough to verify that the assertions hold. the dual approach is to apply backward analysis to propagate properties of the allowable states against the control-flow to infer queries for which the program will not violate any assertion. this paper is a systematic comparison of these two approaches to verification. the paper reports some equivalence results that relate the relative power of various forward and backward analysis frameworks.
Termination is well-known to be one of the most intriguing aspects of program verification. Since logic programs are Turing-complete, it follows by the undecidability of the halting problem that there exists no algori...
ISBN:
(纸本)3540206426
Termination is well-known to be one of the most intriguing aspects of program verification. Since logic programs are Turing-complete, it follows by the undecidability of the halting problem that there exists no algorithm which, given an arbitrary logic program, decides whether the program terminates. However, one can propose both conditions that are equivalent to termination and their approximations that imply termination and can be verified automatically. this paper briefly discusses these kinds of conditions that were studied in [2].
this is a slightly enhanced version of the acceptance speech given by the author after receiving the Herbrand Award at the 19thinternationalconference on Automated Deduction (CADE-19) in Miami, Florida, on August 1,...
详细信息
this is a slightly enhanced version of the acceptance speech given by the author after receiving the Herbrand Award at the 19thinternationalconference on Automated Deduction (CADE-19) in Miami, Florida, on August 1, 2003. Historical matters related to Herbrand's theorem, higher-order logic, and the author's work are discussed. Contributions by others that have been helpful to the author are noted.
暂无评论