This article presents an overview of research in an area loosely called belief revision. Belief revision concentrates on the issue of revising systems of beliefs to reflect perceived changes in the environment or acquisition of new information. The paper includes both an essay surveying the literature and a descriptor-indexed bibliography of over 200 papers and books.

In two studies, the author attempts to develop a general symbol theoretical approach to knowledge representation. The first study, Modeling change - the frame problem, critically examines the - so far unsuccessful - attempts to solve the notorious frame problem. By discussing and analyzing a number of related problems - the prediction problem, the revision problem, the qualification problem, and the book-keeping problem - the frame problem is distinguished as the problem of finding a representational form permitting a changing, complex world to be efficiently and adequately represented. This form, it is argued, is dictated by the metaphysics of the problem world, the fundamental form of the symbol system we humans use in rightly characterizing the world. In the second study, Pictures and words, the symbol theoretical approach is made more explicit. The subject Is the distinction between pictorial (non-linguistic, non-propositional, analogical, "direct") representation and verbal (linguistic, propositional) representation, and the further implications of this distinction. The study focuses on pictorial representation, which has received little attention compared to verbal representation. Observations, ideas, and theories in AI, cognitive psychology, and philosophy are critically examined. The general conclusion is that there is as yet no cogent and mature theory of pictorial representation that gives good support to computer applications. The philosophical symbol theory of Nelson Goodman is found to be the most thoroughly developed and most congenial with the aims and methods of AI. Goodman's theory of pictorial representation, however, in effect excludes computers from the use of pictures. In the final chapter, an attempt is made to develop Goodman's analysis of pictures further turning it into a theory useful to AI. The theory outlined builds on Goodman's concept of exemplification. The key idea is that a picture is a model of a description that has the depicted object as its standard model. One consequence Is that pictorial and verbal forms of representation are seen less as competing alternatives than as complementary forms of representation mutually supporting and depending on each other. / digitalisering@umu

No description available.

The subject matter of master disseration is rational behavior. Its dedicated to the following questions: what kind of behavior can be named “rational”, and how we can model it in strict logical terms (and then in program languages). These questions were raised earlier in Artificial Intelligence researches, and very soon the modeling of human behavior for computers encounters some problems. The general name of these problems is the frame problem.The main aim of the research work is solution of the frame problem from deontic logic point of view. I find this formalism the most suitable for investigation of human (rational) behavior. The work contain historical consideration of the frame problem and its strict definition in terms of basic formalism, as interconnection of two correlated problems: ramification problem and qualification problem. The ramification problem is given an option to solve it by extending the basic formalism (with adding of notion of state constraints, influence information and, most importantly, the laws of causal relationships). To solve the problem of qualification the formalism is extended by introducing possible worlds semantic. We consider the properties of this model and offers a solution to the problem of qualification through valuation by the expectation degree, and introducing normative modal operators on this basis. / Общая тема магистерской диссертации - рациональное поведение. Рассмотрение последнего в рамках Искусственного Интеллекта с точки зрения моделирования в строгих логических терминах (для последующего воспроизведения в языках программирования) привело к выявлению ряда трудностей. Общее название им - проблема фреймов. Главная цель данной работы - решение проблемы фреймов с точки зрения логики деонтических модальностей. В диссертации проводится историческое рассмотрение проблемы фреймов, дается строгое её определение для введенного базового формализма (как двух взаимосвязанных проблем — проблемы ветвлений и проблемы квалификации). Рассматривается проблема ветвлений, дается вариант её решения за счет расширения базового формализма (добавляются понятия ограничений состояний, информации о влияниях, и, самое главное, законов причинных связей). Рассматривается проблема квалификации, базовый формализм расширяется посредством введения для него семантики возможных миров, рассматриваются свойства этой модели и предлагается вариант решения проблемы квалификации за счет оценки по степени ожидаемости, и вводящихся на этой основе модальных нормативных операторов.

Dans le domaine de la vérification formelle de logiciels, il est impératif d'identifier les limites au sein desquelles les éléments ou fonctions opèrent. Ces limites constituent les propriétés de frame (frame properties en anglais). Elles sont habituellement spécifiées manuellement par le programmeur et leur validité doit être vérifiée: il est nécessaire de prouver que les opérations du programme n'outrepassent pas les limites ainsi déclarées. Dans le contexte de la vérification formelle interactive de systèmes complexes, comme les systèmes d'exploitation, un effort considérable est investi dans la spécification et la preuve des propriétés de frame. Cependant, la plupart des opérations ont un effet très localisé et ne menacent donc qu'un nombre limité d'invariants. Étant donné que la spécification et la preuve de propriétés de frame est une tache fastidieuse, il est judicieux d'automatiser l'identification des invariants qui ne sont pas affectés par une opération donnée. Nous présentons dans cette thèse une solution inférant automatiquement leur préservation. Notre solution a pour but de réduire le nombre de preuves à la charge du programmeur. Elle est basée sur l'analyse statique, et ne nécessite aucune annotation de frame. Notre stratégie consiste à combiner une analyse de dépendances avec une analyse de corrélations. Nous avons conçu et implémenté ces deux analyses statiques pour un langage fonctionnel fortement typé qui manipule structures, variants et tableaux. Typiquement, une propriété fonctionnelle ne dépend que de quelques fragments de l'état du programme. L'analyse de dépendances détermine quelles parties de cet état influent sur le résultat de la propriété fonctionnelle. De même, une fonction ne modifiera que certaines parties de ses arguments, copiant le reste à l'identique. L'analyse de corrélations détecte quelles parties de l'entrée d'une fonction se retrouvent copiées directement (i.e. non modifiés) dans son résultat. Ces deux analyses calculent une approximation conservatrice. Grâce aux résultats de ces deux analyses statiques, un prouveur de théorèmes interactif peut inférer automatiquement la préservation des invariants qui portent sur la partie non affectée par l’opération concernée. Nous avons appliqué ces deux analyses statiques à la spécification fonctionnelle d'un micro-noyau, et obtenu des résultats non seulement d'une précision adéquate, mais qui montrent par ailleurs que notre approche peut passer à l'échelle. / In the field of software verification, the frame problem refers to establishing the boundaries within which program elements operate. It has notoriously tedious consequences on the specification of frame properties, which indicate the parts of the program state that an operation is allowed to modify, as well as on their verification, i.e. proving that operations modify only what is specified by their frame properties. In the context of interactive formal verification of complex systems, such as operating systems, much effort is spent addressing these consequences and proving the preservation of the systems' invariants. However, most operations have a localized effect on the system and impact only a limited number of invariants at the same time. In this thesis we address the issue of identifying those invariants that are unaffected by an operation and we present a solution for automatically inferring their preservation. Our solution is meant to ease the proof burden for the programmer. It is based on static analysis and does not require any additional frame annotations. Our strategy consists in combining a dependency analysis and a correlation analysis. We have designed and implemented both static analyses for a strongly-typed, functional language that handles structures, variants and arrays. The dependency analysis computes a conservative approximation of the input fragments on which functional properties and operations depend. The correlation analysis computes a safe approximation of the parts of an input state to a function that are copied to the output state. It summarizes not only what is modified but also how it is modified and to what extent. By employing these two static analyses and by subsequently reasoning based on their combined results, an interactive theorem prover can automate the discharching of proof obligations for unmodified parts of the state. We have applied both of our static analyses to a functional specification of a micro-kernel and the obtained results demonstrate both their precision and their scalability.

Först presenteras metafysisk funktionalism. En Ramseysats för smärta spelar en central roll som en implicit definition av ett mentalt tillstånd över sensorisk input och beteendemässig output. Därefter presenteras reliabilismen som en teori om kunskap. Några allmänna kunskapsteoretiska problem, samt några av reliabilismens problem presenteras. De mest relevanta problem är följande: fallet med en elak demon, klärvoajans samt Mr. Truetemp, och generalitetsproblemet. En formell och schematisk presentation ges för reliabilism som en teori för kunskap, eller möjligen tillskrivande av kunskap, och processreliabilism som en teori för epistemiskt rättfärdigande. Därefter exponeras strukturella likheter mellan funktionalism och processreliabilism. Det får anses plausibelt att det råder ett nära släktskap mellan dessa teorier då Ramseysatser för rättfärdigade trosföreställningar presenteras. Dessa analyseras sedan utifrån möjliga fall. Med ny teoretisk bakgrund prövas reliabilismens problem ånyo inom ett funktionalistisk ramverk. Nya sätt att bemöta problemen presenteras genom en analys av det Kinesiska Rummet. Det svårlösta generalitetsproblemet kan ses som ett frameproblem och hanteras med hjälp av enveloping. / Firstly, a presentation of metaphysical functionalism. A Ramsey sentence plays a central role as an implicit definition of a mental state over sensory input and behavouristic output. A presentation of reliabilism as a theory of knowledge. A summary of some general epistemological problems and some specific to reliabilism; the main ones are the evil demon, clairvoyance and Mr. Truetemp, and the generality problem. A formal and schematic presentation of reliabilism as a theory of knowlege, or possibly knowlege attribution, and process reliabilism as a theory of belief justification. Structural similarities between functionalism and process reliabilism are exposed. A close kinship between these two theories seems plausible because of the possibility to present Ramsey sentences for justified beliefs. These Ramsey sentences are then analysed over possible cases. This new theoretical background, warrents another look at problems for reliabilism. New ways to counter these problems are presented via an analysis of the Chinese Room. The elusive genrality problem is seen as a frame problem and treated using enveloping.