Forgetting is an operation which removes information from a set of logical statements, such that a) the language used by the logic is simplified; and b) as much information as possible from the original logical statements are preserved. Forgetting operations are useful in a variety of contexts, including knowledge representation, where it is necessary to have an operation for removing information from knowledge bases; and the problem of relevance, where logical statements are simplified by removing irrelevant information. In this thesis we consider forgetting operations on logic programs with negation-as-failure according to the stable model semantics. There are existing notions of forgetting on logic programs in the literature: the strong forgetting and weak forgetting of Zhang and Foo, and the semantic approach to forgetting introduced by Wang et al. However, these notions are inadequate: the strong and weak forgettings are defined syntactically with no obvious connections to semantic notions of forgetting; while the semantic approach of Wang et al. does not take into account ``hidden'' information encoded in unused rules. The idea of equivalence on logic programs capture the extent of information contained in a logic program. We consider that two logic programs are equivalent iff the two programs contain the same information. For logic programs, there are many different possible notions of equivalence. We look at the well-known notion of strong equivalence and a new notion of equivalence which we call T-equivalence. Associated with each of these equivalences is a consequence relation on logic program rules. We present sound and complete set of inference rules for both consequence relations. We present a novel approach to logic program forgetting which uses as its basis a set of postulates, which are defined relative to a notion of equivalence. We show that if we use T-equivalence as the equivalence relation, then the only possible forgetting operations (up to equivalence) are strong forgetting and weak forgetting. If strong equivalence is used instead, then there are also only two possible forgetting operations (up to equivalence).

Forgetting is an operation which removes information from a set of logical statements, such that a) the language used by the logic is simplified; and b) as much information as possible from the original logical statements are preserved. Forgetting operations are useful in a variety of contexts, including knowledge representation, where it is necessary to have an operation for removing information from knowledge bases; and the problem of relevance, where logical statements are simplified by removing irrelevant information. In this thesis we consider forgetting operations on logic programs with negation-as-failure according to the stable model semantics. There are existing notions of forgetting on logic programs in the literature: the strong forgetting and weak forgetting of Zhang and Foo, and the semantic approach to forgetting introduced by Wang et al. However, these notions are inadequate: the strong and weak forgettings are defined syntactically with no obvious connections to semantic notions of forgetting; while the semantic approach of Wang et al. does not take into account ``hidden'' information encoded in unused rules. The idea of equivalence on logic programs capture the extent of information contained in a logic program. We consider that two logic programs are equivalent iff the two programs contain the same information. For logic programs, there are many different possible notions of equivalence. We look at the well-known notion of strong equivalence and a new notion of equivalence which we call T-equivalence. Associated with each of these equivalences is a consequence relation on logic program rules. We present sound and complete set of inference rules for both consequence relations. We present a novel approach to logic program forgetting which uses as its basis a set of postulates, which are defined relative to a notion of equivalence. We show that if we use T-equivalence as the equivalence relation, then the only possible forgetting operations (up to equivalence) are strong forgetting and weak forgetting. If strong equivalence is used instead, then there are also only two possible forgetting operations (up to equivalence).

In this thesis, a model for argument revision is presented, in terms of the expansion and contraction of a system of structured argumentation. At its core, the model uses the belief revision concept of minimal change, but without requiring a pre-determined entrenchment ordering to establish minimality. In the first part of the thesis, a model for argument revision is defined and described. Specified in terms of the ASPIC\+ framework for argumentation, the model is divided into two main concepts: argument expansion, whose goal is to make certain arguments acceptable in the system, possibly by adding them; and argument contraction, whose goal is to make certain arguments unacceptable in the system, possibly by removing them. The goal of a revision process can be achieved in multiple different ways, thus a method of choosing which, based on measures of minimal change, is also specified. The second part of the thesis demonstrates two applications of the model in the context of multi-agent dialogue. The first is used to assist a participant when faced with a need to update its commitment store during persuasion dialogue, while the second shows how a participant can use argument revision techniques to both assess and maintain a lie.The main contributions of the thesis are twofold. First, the characterisation of a model for argument revision, based on established belief revision principles but with a key difference. The model for argument revision demonstrates how it is possible to use measurable effects on the system when determining minimal change instead of relying on a pre-determined, qualitative entrenchment ordering.Second, the thesis demonstrates two applications of argument revision in dialogue. The first is in assisting an agent in retracting a commitment that has been defeated, and for which it can offer no defence. When retracting a claim, the participant may also be required to retract other claims from which the defeated one is a consequence. Applying argument revision techniques allow the participant to reason about what constitutes a minimal set of retractions, in terms of current commitments and potential future communications in the dialogue.The second dialogical application relates to the opposite of retraction; instead of choosing to retract an undefended claim, the participant could instead choose to lie in order to defend it. Argument revision allows the participant to not only assess whether or not lying is ``minimal'' (compared to retracting), but to also to maintain the lie, by using the measures of minimal change.Overall, the thesis shows that not only is justifiable argument revision possible without relying on a pre-determined entrenchment ordering, it is also a powerful tool for participants in a dialogue, assisting with dialogue move selection.

Within a distributed system, autonomous agents may find it necessary to cooperate in order to achieve their objectives. Interaction protocols provide standard frameworks within which to conduct common classes of interaction, but they are only useful when the agents using them have a common interpretation of the constraints imposed by those protocols. In open systems, where there are no system-wide objectives and components are contributed from a variety of sources, this is difficult to ensure. An agent within a sufficiently complex environment will find it necessary to draw inferences from information sources of varying integrity and completeness. Given flawed or incomplete information, it may be necessary for an agent to resort to nonmonotonic reasoning in order to be able to make concrete decisions within limited windows of opportunity. This can be expected to create inconsistencies in the joint beliefs of agents which can only be repaired by dialogue between peers. To verify and repair all possible sources of inconsistency is impractical for any sizable body of inference however—any belief revision must therefore be subject to prioritisation. In this thesis, we introduce a mechanism by which agents can perform opportunistic argumentation during dialogue in order to perform distributed belief revision. An interaction portrayal uses the protocol for a given interaction to identify the logical constraints which must be resolved during the interaction as it unfolds. It then compares and reconciles the expectations of agents prior to the resolution of those constraints by generating and maintaining a system of arguments. The composition and scope of arguments is restricted in order to minimise the information exchange whilst still trying to ensure that all available admissible viewpoints are adequately represented immediately prior to any decision. This serves both to make interaction more robust (by allowing agents to make decisions based on the distributed wisdom of its peer group without being explicitly directed by a protocol) and to reconcile beliefs in a prioritised fashion (by focusing only on those beliefs which directly influence the outcome of an interaction as determined by its protocol).

Belief Revision addresses the problem of how to change epistemic states, usually represented in the literature by sets of logical sentences. Solid theoretical results were consolidated with the AGM paradigm, which deals with theories (logically closed sets of sentences). After that, the theory was extended to belief bases, that is, arbitrary sets of sentences. Besides all this theoretical framework, AI researchers face serious difficulties when trying to implement belief revision systems. One of the major complications is the closure required by AGM theory, which cannot be easily computed. Even belief bases, which do not require closure, seem to be improper for practical purposes, since their changes are usually very rigid (syntax dependent). Some operations, known as pseudo-contractions, are in the middle ground between belief set change and belief base change. In the present work we have proposed a new pseudo-contraction operation, studied its properties and characterized it. We have also found connections between this operator and some other pseudo-contractions. / Revisão de Crenças aborda o problema de como alterar estados epistêmicos, normalmente representados na literatura como conjuntos de sentenças lógicas. Resultados teóricos sólidos foram consolidados com o paradigma AGM, que lida com teorias (conjuntos de sentenças logicamente fechados). Depois disso, a teoria foi estendida para bases de crenças, isto é, conjuntos arbitrários de sentenças. Apesar de todo esse arcabouço teórico, pesquisadores de IA enfrentam sérias dificuldades ao tentar implementar sistemas de revisão de crenças. Uma das maiores complicações é o fecho exigido pela teoria AGM, que não pode ser facilmente computado. Mesmo bases de crenças, que não exigem fechamento, parecem ser impróprias para fins práticos, pois suas alterações são geralmente muito rígidas (dependentes de sintaxe). Algumas operações, conhecidas como pseudo-contrações, estão no meio do caminho entre mudanças para conjuntos de crenças e mudanças para bases de crenças. Nesse trabalho, propomos uma nova operação de pseudo-contração, estudamos suas propriedades e a caracterizamos. Também encontramos conexões entre esse operador e algumas outras pseudo-contrações.

Belief Revision addresses the problem of how to change epistemic states, usually represented in the literature by sets of logical sentences. Solid theoretical results were consolidated with the AGM paradigm, which deals with theories (logically closed sets of sentences). After that, the theory was extended to belief bases, that is, arbitrary sets of sentences. Besides all this theoretical framework, AI researchers face serious difficulties when trying to implement belief revision systems. One of the major complications is the closure required by AGM theory, which cannot be easily computed. Even belief bases, which do not require closure, seem to be improper for practical purposes, since their changes are usually very rigid (syntax dependent). Some operations, known as pseudo-contractions, are in the middle ground between belief set change and belief base change. In the present work we have proposed a new pseudo-contraction operation, studied its properties and characterized it. We have also found connections between this operator and some other pseudo-contractions. / Revisão de Crenças aborda o problema de como alterar estados epistêmicos, normalmente representados na literatura como conjuntos de sentenças lógicas. Resultados teóricos sólidos foram consolidados com o paradigma AGM, que lida com teorias (conjuntos de sentenças logicamente fechados). Depois disso, a teoria foi estendida para bases de crenças, isto é, conjuntos arbitrários de sentenças. Apesar de todo esse arcabouço teórico, pesquisadores de IA enfrentam sérias dificuldades ao tentar implementar sistemas de revisão de crenças. Uma das maiores complicações é o fecho exigido pela teoria AGM, que não pode ser facilmente computado. Mesmo bases de crenças, que não exigem fechamento, parecem ser impróprias para fins práticos, pois suas alterações são geralmente muito rígidas (dependentes de sintaxe). Algumas operações, conhecidas como pseudo-contrações, estão no meio do caminho entre mudanças para conjuntos de crenças e mudanças para bases de crenças. Nesse trabalho, propomos uma nova operação de pseudo-contração, estudamos suas propriedades e a caracterizamos. Também encontramos conexões entre esse operador e algumas outras pseudo-contrações.

No description available.

Thesis (PhD (Mathematics))--University of Stellenbosch, 2010. / ENGLISH ABSTRACT: Classical formulations model belief revision as a deterministic process. Under certain circumstances, the process may have more than one outcome, which suggests that belief revision is non-deterministic instead. Representations exist that model belief revision in either format, and for both formats there are axiom schemes that determine whether the representation is in fact a belief revision process. Although the axiom scheme for the non-deterministic case generalises that of the deterministic case, both schemes entail that all of the beliefs held by an agent are affected by new information, which is perhaps unintuitive. Rather, one may consider that belief revision should be local, with beliefs only affected if the new information is pertinent to them. We approach the problem of belief revision from the standpoint that it is local and non-deterministic, and the purpose and contribution of this dissertation is the development of a topological framework with which to model belief revision in this manner. / AFRIKAANSE OPSOMMING: Geloofshersiening word gewoonlik as ’n deterministiese proses voorgestel. Meer as een uitkoms mag bestaan vir verskeie omstandighede, wat aandui dat die proses liewer nie-deterministies van aard is. Beide die gevalle word deur aksiomaskemas gereguleer, en die aksiomas vir die nie-deterministiese geval veralgemeen dié van die deterministiese geval. Albei aksiomaskemas stipuleer, miskien onintuïtief, dat alle gelowe van ’n agent deur die nuwe informasie geaffekteer word. ’n Beter metode is dat net daardie gelowe waarvoor die nuwe informasie toepaslik is geaffekteer word. Ons benader die probleem van geloofshersiening uit die standpunt dat dit lokaal en nie-deterministies is, en die doel en bydrae van hierdie proefskrif is dus die ontwikkeling van ’n topologiese raamwerk waarmee ons geloofshersiening op hierdie manier kan voorstel.

Verificação de modelos é uma das mais eficientes técnicas de verificação automática de sistemas. No entanto, apesar de poder lidar com verificações complexas, as ferramentas de verificação de modelos usualmente não fornecem informação alguma sobre como reparar inconsistências nestes modelos. Nesta dissertação, mostramos que abordagens desenvolvidas para a atualização de modelos CTL inconsistentes não são capazes de lidar com todos os tipos de alterações em modelos. Introduzimos então o conceito de revisão de modelos: uma abordagem baseada em revisão de crenças para o reparo de modelos inconsistentes em um contexto estático. Relacionamos nossa proposta com trabalhos clássicos em revisão de crenças. Definimos um operador de revisão de modelos e mostramos que este obedece postulados de racionalidade clássico de revisão de crenças. Propomos um algoritmo de revisão com base no algoritmo utilizado pela abordagem de atualização de modelos. Discutimos sobre problemas e limites do algoritmo proposto, e mostramos que essa estratégia de adaptação não é uma solução apropriada. / Model checking is one of the most robust techniques in automated system verification. But, although this technique can handle complex verifications, model checking tools usually do not give any information on how to repair inconsistent system models. In this dissertation, we show that approaches developed for CTL model update cannot deal with all kinds of model changes. We introduce the concept of CTL model revision: an approach based on belief revision to handle system inconsistency in a static context. We relate our proposal to classical works on belief revision. We define an operator for model revision and we show that it obeys the classical rationality postulates of belief revision. We propose an algorithm for model revision based on the algorithm used by the model update approach. We discuss problems and limitations of our proposed algorithm and show that this strategy of adaptation is not an appropriate solution.

Neste trabalho apresentamos uma implementação de revisão de crenças baseada em comparação de modelos (estados) em uma ferramenta de verificação automática de sistemas de estados finitos. Dada uma fórmula (na lógica CTL) inconsistente com o modelo do sistema, revisamos esse modelo de tal maneira que essa fórmula temporal se torne verdadeira. Como temos oito operadores temporais (AG, AF, AX, AU, EG, EF, EX e EU), foram criados algoritmos especícos para cada um deles. Como o modelo do sistema deriva do seu código na linguagem SMV, a sua revisão passa obrigatoriamente por mudanças na sua descrição. A nossa implementação contempla três tipos de mudanças: acréscimo de linhas, eliminação de linhas e mudança no estado inicial, sendo que as duas primeiras provocam modicações nas transições entre os estados que compõe o modelo. Alguns testes foram aplicados para comprovar a contribuição da revisão de crenças (revisão de modelos) como ferramenta de auxílio ao usuário durante o processo de modelagem de sistemas. / In this work we present an implementation of belief revision based on comparison of models (states) in a tool for automatic verication of nite state systems. Given a formula (in the language of CTL) inconsistent with the model of the system, we revise this model in such way that the temporal formula becomes valid. As we have eight temporal operators (AG, AF, AX, AU, EG, EF, EX and EU), specic algorithms for each one of them have been created. As the model of the system is related with its code in SMV language, its revision forces changes in its description. Our implementation contemplates three types of change: addition of lines, elimination of lines and change in the initial state, where the rst two cause modications in the transitions between the states of the model. Some tests were applied to prove the contribution of the belief revision (model revision) as aid-tool to the user during the process of systems modeling.