| 1. |
- Alferes, José Julio, et al.
(författare)
-
A compilation of updates plus preferences
- 2002
-
Ingår i: Logics in Artificial Intelligence 8th European Conference, JELIA 2002 Cosenza, Italy, September 23–26, 2002 Proceedings. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783540441908 - 9783540457572 ; , s. 62-74
-
Bokkapitel (refereegranskat)abstract
- We show how to compile programs formalizing update plus preference reasoning into standard generalized logic programs and show the correctness of the transformation.
|
|
| 2. |
- Alferes, José Júlio, et al.
(författare)
-
Dynamic Logic Programming
- 1997
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- In this paper we investigate updates of knowledge bases represented by logic programs. In order to represent negative information, we use generalized logic programs which allow default negation not only in their bodies but also in their heads. We start by introducing the notion of an update $P \oplus U$ of a logic program $P$ by another logic program $U$. Subsequently, we provide a precise semantic characterization of $P \oplus U$, and study some basic properties of program updates. In particular, we show that our update programs generalize the notion of interpretation update. We then extend this notion to sequences of logic programs updates $P_1 \oplus P_2 \oplus \dots$, defining dynamic program updates, thereby introducing the paradigm of dynamic logic programming. This paradigm significantly facilitates modularization of logic programming, and thus modularization of non-monotonic reasoning as a whole. Suppose that we are given a set of logic program modules, each describing a different state of our knowledge of the world. Different states may represent different time points or different sets of priorities or perhaps even different viewpoints. Consequently, program modules may contain mutually contradictory as well as overlapping information. The role of the dynamic program update is to use the mutual relationships existing between different states to precisely determine, at any given state, the declarative and the procedural semantics of the combined program, resulting from all these modules.
|
|
| 3. |
- Alferes, José Júlio, et al.
(författare)
-
Preface
- 2019
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - 1611-3349 .- 0302-9743. ; 11372 LNCS, s. V-VI
-
Tidskriftsartikel (övrigt vetenskapligt/konstnärligt)
|
|
| 4. |
- Ericsson, AnnMarie, 1972-
(författare)
-
Enabling Tool Support for Formal Analysis of ECA Rules
- 2009
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Rule-based systems implemented as event-condition-action (ECA) rules utilize a powerful and flexible paradigm when it comes to specifying systems that need to react to complex situation in their environment. Rules can be specified to react to combinations of events occurring at any time in any order. However, the behavior of a rule based system is notoriously hard to analyze due to the rules ability to interact with each other.Formal methods are not utilized in their full potential for enhancing software quality in practice. We argue that seamless support in a high-level paradigm specific tool is a viable way to provide industrial system designers with powerful verification techniques. This thesis targets the issue of formally verifying that a set of specified rules behaves as indented.The prototype tool REX (Rule and Event eXplorer) is developed as a proof of concept of the results of this thesis. Rules and events are specified in REX which is acting as a rule-based front-end to the existing timed automata CASE tool UPPAAL. The rules, events and requirements of application design are specified in REX. To support formal verification, REX automatically transforms the specified rules to timed automata, queries the requirement properties in the model-checker provided by UPPAAL and returns results to the user of REX in terms of rules and events.The results of this thesis consist of guidelines for modeling and verifying rules in a timed automata model-checker and experiences from using and building a tool implementing the proposed guidelines. Moreover, the result of an industrial case study is presented, validating the ability to model and verify a system of industrial complexity using the proposed approach.
|
|
