Defeasible reasoning is a simple but efficient approach to nonmonotonic reasoning that has recently attracted considerable interest and that has found various applications. Defeasible logic and its variants are an imp...
详细信息
ISBN:
(纸本)3540439307
Defeasible reasoning is a simple but efficient approach to nonmonotonic reasoning that has recently attracted considerable interest and that has found various applications. Defeasible logic and its variants are an important family of defeasible reasoning methods. So far no relationship has been established between defeasible logic and mainstream nonmonotonic reasoning approaches. In this paper we establish close links to known semantics of extended logic programs. In particular, we give a translation of a defeasible theory D into a program P(D). We show that under a condition of decisiveness, the defeasible consequences of D correspond exactly to the sceptical conclusions of P(D) under the stable model semantics. Without decisiveness, the result holds only in one direction (all defeasible consequences of D axe included in all stable models of P(D)). If we wish a complete embedding for the general case, we need to use the Kunen semantics of P(D), instead.
In this work we present additional results, related to the property of strong equivalence of logic programs. this property asserts that two programs share the same set of stable models, even under the addition of new ...
详细信息
ISBN:
(纸本)0262511290
In this work we present additional results, related to the property of strong equivalence of logic programs. this property asserts that two programs share the same set of stable models, even under the addition of new rules. As shown in a recent work by Lifschitz, Pearce and Valverde, strong equivalence can be simply reduced to. equivalence in the logic of Here-and-there (HT). In this paper we provide an alternative based on 3-valued logic, using also, as a first step, a classical logic charaterization. We show that the 3-valued encoding provides a direct interpretation for nested expressions but, when moving to an unrestricted syntax, it generally yields different results from HT.
Nested logic programs have recently been introduced in order to allow for arbitrarily nested formulas in the heads and the bodies of logic program rules under the answer sets semantics. Previous results show that nest...
详细信息
ISBN:
(纸本)3540439307
Nested logic programs have recently been introduced in order to allow for arbitrarily nested formulas in the heads and the bodies of logic program rules under the answer sets semantics. Previous results show that nested logic programs can be transformed into standard (unnested) disjunctive logic programs in an elementary way, applying the negation-as-failure operator to body literals only. this is of great practical relevance since it allows us to evaluate nested logic programs by means of off-the-shelf disjunctive logicprogramming systems, like DLV. However, it turns out that this straightforward transformation results in an exponential blow-up in the worst-case, despite the fact that complexity results indicate that there is a polynomial translation among both formalisms. In this paper, we take up this challenge and provide a polynomial translation of logic programs with nested expressions into disjunctive logic programs. Moreover, we show that this translation is modular and (strongly) faithful. We have implemented boththe straightforward as well as our advanced transformation;the resulting compiler serves as a front-end to DLV and is publicly available on the Web.
logicprogramming based tools for real-time model checking are beginning to emerge. In a previous work we had demonstrated the feasibility of building such a model checker by combining constraint processing and tabula...
详细信息
ISBN:
(纸本)3540439307
logicprogramming based tools for real-time model checking are beginning to emerge. In a previous work we had demonstrated the feasibility of building such a model checker by combining constraint processing and tabulation. But efficiency and practicality of such a model checker were not adequately addressed. In this paper we describe XMC/dbm, an efficient model checker for real-time systems using tabling. Performance gains in XMC/dbmdirectly arise from the use of a lightweight constraint solver combined with tabling. Specifically the timing constraints axe represented by difference bound matrices which are encoded as Prolog terms. Operations on these matrices, the dominant component in real-time model checking, are shared using tabling. We provide experimental evidence that the performance of XMC/dbmis considerably better than our previous real-time model checker and is highly competitive to other well known real-time model checkers implemented in C/C++. An important aspect of XMC/dbm is that it can handle verification of systems consisting of untimed components with performance comparable to verification systems built specifically for untimed systems.
the paper introduces the SILK tool-set, a tool-set based on constraint logicprogramming techniques for the support of application integration. We focus on the Integrator component of SILK, which provides tools and te...
详细信息
ISBN:
(纸本)3540439307
the paper introduces the SILK tool-set, a tool-set based on constraint logicprogramming techniques for the support of application integration. We focus on the Integrator component of SILK, which provides tools and techniques to support the process of model evolution: unification of the models of the information sources and their mapping Onto the conceptual models of their user-groups. We present the basic axchitecture of SILK and introduce the SILK Knowledge Base, which stores the meta-information describing the information sources. the SILK Knowledge Base can contain both object-oriented and ontology-based descriptions, annotated with constraints. the constraints can be used both for expressing the properties of the objects and for providing mappings between them. We give a brief introduction to SILan, the language for Knowledge Base presentation and maintenance. We describe the implementation status of SILK and give a simple example, which shows how constraints and constraint reasoning techniques can be used to support model evolution.
Assertions, or more generally "programming by contract", have gained widespread acceptance in the computer science community as a means for correct program development. However the literature lacks an empiri...
详细信息
ISBN:
(纸本)0769518192
Assertions, or more generally "programming by contract", have gained widespread acceptance in the computer science community as a means for correct program development. However the literature lacks an empirical evaluation of the benefits a programmer gains by using assertions in his software development. this paper reports two controlled experiments that close this gap. Both experiments compare "programming by contract" to the traditional-programming style without assertions. the evaluation of the first experiment suggests that assertions decrease the programming effort for the extension of existing software, measured as time needed to finish tile task, while the programming effort slightly increases during the development of new code. the second experiment shows that the programming effort tended to be larger with assertions than without. In addition, it shows that the reliability of the written programs slightly increases withthe usage of assertions compared to the programs written without assertions.
We propose a new way of extending logicprogramming (LP) for reasoning with uncertainty. Probabilistic finite domains (Pfd) capitalise on ideas introduced by Constraint LP, on how to extend the reasoning capabilities ...
详细信息
ISBN:
(纸本)3540439307
We propose a new way of extending logicprogramming (LP) for reasoning with uncertainty. Probabilistic finite domains (Pfd) capitalise on ideas introduced by Constraint LP, on how to extend the reasoning capabilities of the LP engine. Unlike other approaches to the field, Pfd syntax can be intuitively related to the axioms defining Probability and to the underlying concepts of Probability theory, (PT) such as sample space, events, and probability function. Probabilistic variables are core computational units and have two parts. Firstly, a finite domain, which at each stage holds the collection of possible values that can be assigned to the variable, and secondly a probabilistic function that can be used to assign probabilities to the elements of the domain. the two constituents are kept in isolation from each other. there are two benefits in such an approach. Firstly, that propagation techniques from finite domains research are retained, since a domain’s representation is not altered. thus, a probabilistic variable continues to behave as a finite domain variable. Secondly, that the probabilistic function captures the probabilistic behaviour of the variable in a manner which is, to a large extent, independent of the particular domain values. the notion of events as used in PT can be captured by LP predicates containing probabilistic variables and the derives operator (⊢) as defined in LP. Pfd stores hold conditional constraints which are a computationally useful restriction of conditional probability from PT. Conditional constraints are defined by D1: π1⊕...⊕Dn: πn | Q1 ∧...∧ Qm where, Di and Qj are predicates and each πi is a probability measure (0 ≤ πi ≤ 1, 1 ≤ i ≤ n, 1 ≤ j ≤ m). the conjuction of Qj’s qualifies probabilistic knowledge about Di<
We propose a new translation from normal logic programs with constraints under the answer set semantics to propositional logic. Given a logic program, we show that by adding, for each loop program, a corresponding loo...
详细信息
ISBN:
(纸本)0262511290
We propose a new translation from normal logic programs with constraints under the answer set semantics to propositional logic. Given a logic program, we show that by adding, for each loop program, a corresponding loop formula to the program's completion, we obtain a one-to-one correspondence between the answer sets of the program. and the models of the resulting propositional theory. Compared withthe translation, by Ben-Eliyahu and Dechter, ours has the advantage that it does not use any extra variables, and is considerably simpler;thus easier to understand. However, in the worst case, it requires computing exponential number of loop formulas. To address this problem, we propose an approach that adds loop formulas a few at a time, selectively. Based on these results, we implemented a system called ASSAT(X), depending on the SAT solver X used, and tested it on a variety of benchmarks including, ing the graph coloring the blocks world planning, and Hamiltonian Circuit domains. the results are compared withthose by smodels and dlv, and it shows A clear-edge of ASSAT over them in these domains.
In the paper, we present a procedural semantics for fuzzy disjunctive programs - sets of graded strong literal disjunctions. We shall suppose that truth values constitute a complete Boolean lattice L = (L, less than o...
详细信息
ISBN:
(数字)9783540360780
ISBN:
(纸本)3540000100
In the paper, we present a procedural semantics for fuzzy disjunctive programs - sets of graded strong literal disjunctions. We shall suppose that truth values constitute a complete Boolean lattice L = (L, less than or equal to, boolean OR, boolean AND, double right arrow, 0, 1). A graded strong literal disjunction is a pair (D, c) where D is a strong literal disjunction of the form l(1)(V) over dot ... (V) over dot l(n) and c is a truth value from the lattice L. A graded disjunction can be understood as a means of the representation of incomplete and uncertain information, where the incompleteness is formalised by its strong literal disjunction, while the uncertainty by its truth degree. In the end, the coincidence of the procedural and fixpoint semantics, proposed in [18], will be reached.
the purpose of the work presented here is to convert the design documentation of procedural application systems into an object-oriented design for the purpose of populating an object-oriented repository. the prerequis...
详细信息
ISBN:
(纸本)0769518192
the purpose of the work presented here is to convert the design documentation of procedural application systems into an object-oriented design for the purpose of populating an object-oriented repository. the prerequisite is to have a single design representation - the object model as specified in the OMG Unified Modeling Language. that entails transforming procedural programs into class hierarchies as described in this paper. the technique used is an adaptation of the dominance tree approach described in previous papers from Burd and Munro combined withthe precedence graphs proposed by Horwitz and Reps.
暂无评论