McMillan (1992) described a technique for deadlock detection based on net unfoldings. We extend its applicability to the properties of a temporal logic with a possibility operator. the new algorithm is shown to be pol...
详细信息
McMillan (1992) described a technique for deadlock detection based on net unfoldings. We extend its applicability to the properties of a temporal logic with a possibility operator. the new algorithm is shown to be polynomial in the size of the net for 1-safe conflict-free Petri nets, while the algorithms of the literature require exponential time.
In this paper, a logic program synthesis method from first-order logic specifications is described. the specifications are described by Horn clauses extended by universally quantified implicational formulas. these for...
详细信息
In this paper, a logic program synthesis method from first-order logic specifications is described. the specifications are described by Horn clauses extended by universally quantified implicational formulas. these formulas are transformed into definite clause programs by unfold/fold transformation. We show that some classes of first-order formulas can be successfully transformed into definite clauses by unfold/fold transformation.
In the last decade defeasible argumentation frameworks have evolved to become a sound setting to formalize commonsense, qualitative reasoning. the logicprogramming paradigm has shown to be particularly useful for dev...
详细信息
In the last decade defeasible argumentation frameworks have evolved to become a sound setting to formalize commonsense, qualitative reasoning. the logicprogramming paradigm has shown to be particularly useful for developing different argument-based frameworks on the basis of different variants of logicprogramming which incorporate defeasible rules. Most of such frameworks, however, are unable to deal with both explicit uncertainty and vague knowledge, as defeasibility is directly encoded in the object language. this paper presents possibilistic defeasible logicprogramming (P-DeLP), a new logicprogramming language which combines features from argumentation theory and logicprogramming, incorporating as well the treatment of possibilistic uncertainty. Such features are formalized on the basis of PGL, a possibilistic logic based on Godel fuzzy logic. One of the applications of P-DeLP is providing an intelligent agent with non-monotonic, argumentative inference capabilities. In this paper we also provide a better understanding of such capabilities by defining two non-monotonic operators which model the expansion of a given program by adding new weighed facts associated with argument conclusions and warranted literals, respectively. Different logical properties for the proposed operators are studied. (c) 2008 Elsevier B.V. All rights reserved.
this special issue of theory and Practice of logicprogramming consists of extended versions of five selected papers from the 3rd International Joint conference on Rules and Reasoning (RuleML+RR 2019). RuleML+RR 2019 ...
详细信息
this special issue of theory and Practice of logicprogramming consists of extended versions of five selected papers from the 3rd International Joint conference on Rules and Reasoning (RuleML+RR 2019). RuleML+RR 2019 was held in conjunction withthe 5th Global conference on Artificial Intelligence, GCAI 2019, as part of the Bolzano Rules and Artificial INtelligence Summit in Bolzano, Italy, from 17 to 19 of September 2019.
the problem of composing assumption-commitment specifications arises in the hierarchical development of reactive or concurrent systems. Abadi and Lamport's composition principle has been proposed as a logic-indepe...
详细信息
the problem of composing assumption-commitment specifications arises in the hierarchical development of reactive or concurrent systems. Abadi and Lamport's composition principle has been proposed as a logic-independent solution to that problem. In this paper, we apply it to derive a parallel rule for UNITY-like assumption-commitment specifications. For that purpose, we first interpret UNITY formulas in Abadi and Lamport's compositional model. then, the premises of the parallel rule are reduced to proof obligations that can be carried with rules inherited from the UNITY logic. the approach is illustrated by an example.
In this paper we consider the theory of fuzzy logicprogramming without negation. Our results cover logical systems with a wide variety of connectives ranging from t-norm and conorms, through conjunctors and disjuncto...
详细信息
In this paper we consider the theory of fuzzy logicprogramming without negation. Our results cover logical systems with a wide variety of connectives ranging from t-norm and conorms, through conjunctors and disjunctors and their residuals to aggregation operators. Rules of our programs are many valued implications. We emphasize, that in contrast to other approaches, our logic is truth functional, i.e. according to P. Hajek, we work in fuzzy logic in narrow sense. We prove the soundness and the completeness of our formal model. We deal with applications to threshold computation, abduction, fuzzy unification based on similarity. We show that fuzzy unification based on similarities has applications to fuzzy databases and flexible querying. (C) 2001 Elsevier Science B.V. All rights reserved.
this paper proposes new semantics for merging object programming into logicprogramming. It differs from previous attempts in that it takes a relational view of method evaluation and inheritance mechanisms originating...
详细信息
In this paper, we will attempt to give a procedural interpretation to modal logic. Modal logic is used as a programming language and then its procedural interpretation defines a computational procedure for the languag...
详细信息
this paper proposes a constructive logic in which a concurrent System can be defined as a proof of a specification. the logic is defined by adding stream types and several rules for them to a simple constructive logic...
详细信息
this paper proposes a constructive logic in which a concurrent System can be defined as a proof of a specification. the logic is defined by adding stream types and several rules for them to a simple constructive logic based on intuitionism. the unique feature of the obtained system is in the (MPST) rule, which is a kind of structural induction on streams. the (MPST) rule is based on the idea of Brouwer's theory of choice sequences in intuitionism and it allows to define a concurrent process, which is actually a Purge's mapstream function, as a proof of a specification with a good intuition on computation. Several techniques for defining stream-based concurrent programs are also presented through various examples.
Most of the work conducted so far in the field of logicprogramming has focused on representing static knowledge, i.e., knowledge that does not evolve with time. To overcome this limitation, in a recent paper, the aut...
详细信息
Most of the work conducted so far in the field of logicprogramming has focused on representing static knowledge, i.e., knowledge that does not evolve with time. To overcome this limitation, in a recent paper, the authors introduced dynamic logicprogramming. there, they studied and defined the declarative and operational semantics of sequences of logic programs (or dynamic logic programs). Each program in the sequence contains knowledge about some given state, where different states may, for example, represent different time periods or different sets of priorities. But how, in concrete situations, is a sequence of logic programs built? For instance, in the domain of actions, what are the appropriate sequences of programs that represent the performed actions and their effects? Whereas dynamic logicprogramming provides a way for, given the sequence, determining what should follow, it does not provide a good practical language for the specification of the sequence of updates which may be conditional on the intervening states. Here we define the language LUPS-"Language for dynamic updates"-designed for specifying changes to logic programs. Given an initial knowledge base (as a logic program) LUPS provides a way for sequentially updating it. the declarative meaning of a sequence of sets of update actions in LUPS is defined by the semantics of the dynamic logic program generated by those actions. Additionally, we provide a translation of the sequence of update statements sets into a single logic program written in a meta-language, in such a way that the stable models of the resulting program correspond to the previously defined declarative semantics. Finally, we exhibit the usage of LUPS in several application domains. (C) 2002 Elsevier Science B.V. All rights reserved.
暂无评论