Formal reasoning in intelligent database systems

Expert database systems were proposed to solve the difficulties encountered in traditional database systems. Prolog provides a fast prototyping tool for building such database systems. However, an intelligent database system implemented in Prolog faces a major restriction that only Horn rules are allowed in the knowledge base. We propose a theorem prover which can make inference for non-Horn intelligent database systems. Conclusions can be deduced from the facts and rules stored in a knowledge base. For a knowledge base with a finite domain, the prover can provide correct answers to queries, derive logical consequences of the database, and provide help in detecting inconsistencies or locating bugs in the database. The theorem prover is efficient in deriving conclusions from large knowledge bases which might swamp most of the other deductive systems. The theorem prover is also useful in solving heuristically the satisfiability problem related to a database with an infinite domain. A truth maintenance mechanism is provided to help eliminate repetitious work for the same goals.Supported by National Science Council under grant NSC 81-0408-E-110-9.     

Uncertain reasoning about agents' beliefs and reasoning

Reasoning about mental states and processes is important in varioussubareas of the legal domain. A trial lawyer might need to reason andthe beliefs, reasoning and other mental states and processes of membersof a jury; a police officer might need to reason about the conjecturedbeliefs and reasoning of perpetrators; a judge may need to consider adefendant's mental states and processes for the purposes of sentencing;and so on. Further, the mental states in question may themselves beabout the mental states and processes of other people. Therefore, if AIsystems are to assist with reasoning tasks in law, they may need to beable to reason about mental states and processes. Such reasoning isriddled with uncertainty, and this is true in particular in the legaldomain. The article discusses how various different types ofuncertainty arise, and shows how they greatly complicate the task ofreasoning about mental states and processes. The article concentrates onthe special case of states of belief and processes of reasoning, andsketches an implemented, prototype computer program (ATT-Meta) thatcopes with the various types of uncertainty in reasoning about beliefsand reasoning. In particular, the article outlines the system'sfacilities for handling conflict between different lines of argument,especially when these lie within the reasoning of different people. Thesystem's approach is illustrated by application to a real-life muggingexample.     

A framework to support qualitative reasoning about COAs in a dynamic spatial environment

We propose a framework to reason qualitatively about courses of action (COAs) which need to be executed in a realistic geographic space that may change. Particularly, the framework aims to support human mental ‘What-If’ analysis by simulating the execution of COAs in a virtual geographic environment, which can change during the simulation, and by allowing the user to explore various scenarios (different COAs) and to analyse their outcomes using causal reasoning techniques. In this article, we first present a framework which is based on a conceptual model of spatio-temporal situations, a multi-agent geosimulation platform and qualitative spatio-temporal causal reasoning techniques. Then, we illustrate the framework using a case study.     

Formal behavior modeling and effective automatic refinement

Modeling and refining behaviors of software systems are two crucial issues in the methodology of Model-Driven Development (MDD). Traditional methods include Unified Modeling Language (UML) based methods and formal methods. Recently integrated methods by taking full advantages of these two methods have received increasing attention. Unfortunately, there are still no effective formal modeling and automatic refinement methods for behaviors. Besides, difficulties exist in generating some structures, e.g., explicit loop structures, via existing approaches.In this paper, we propose a B-notations based framework for formal modeling and automatically refining behaviors. In our framework, three issues are involved: automatic behavior modeling, theory of behavior refinement, and automatic behavior refinement. For automatic behavior modeling, we propose a B-notation based automatic modeling method for behaviors. For theory of behavior refinement, we propose a refinement theory focusing on behaviors that regards the behavior refinement problem as a search problem. For automatic behavior refinement, we propose an automatic refinement approach by combining top-down logic reduction based method and bottom-up local search based method, where explicit loop structures can be well generated.     

Dialogues in support of qualitative reasoning

Abstract Do students always interact with computers reflectively on tasks and improve qualitative reasoning? It seems that students often manipulate software without changing existing conceptions or exploring the implications of their conceptions to generate deeper explanations. This undermines the educational value of such interactions — though dialogue with a peer or adult can make the interaction more valuable. However, it is uncertain when and how such dialogues work. If high quality educational interactions with computers are to take place, then it is necessary to understand the situations in which particular dialogue forms are effective and to find ways of modelling these. In this paper a framework for the design of such interactions is proposed based on a dialogue analysis that employs transactional analysis and logical dialogue game theory. The framework is applied to a medical (simulation-based) learning context to illustrate how it may enhance interactions with such systems.     

Compositional reasoning about responsive systems with limited resources

A compositional network proof theory to specify and verify properties of fault-tolerant real-time distributed systems with limited resources is presented. In this theory a conceptual scheduler grants the resource using on-line preemptive priority scheduling where the priority is a function of the initial priority and the time spent waiting for the resource. The method enables reasoning about responsive systems which must respond to external inputs in a timely, dependable, and predictable manner. It allows us to abstract from the precise nature and occurrence of faults and to focus on how they affect the externally visible input and output behaviour. To this end a failure hypothesis is formalized as a relation between the system's normal behaviour (i.e., the behaviour when no faults occur) and its acceptable behaviour, that is, the normal behaviour together with the exceptional behaviour (i.e., the behaviour whose abnormality should be tolerated). The proof theory is compositional to allow reasoning with the specifications of processes while ignoring their implementation details.Supported by the Dutch STW under grant number NWI88.1517: Fault Tolerance: Paradigms, Models, Logics, Construction.     

Nonmonotonic reasoning,nonmonotonic logics and reasoning about change

In this paper we introduce nonmonotonic reasoning and the attempts at formalizing it using nonmonotonic logics. We examine and compare the best known of these. Despite the difference in motivation and technical construction there are strong similarities between these logics which are confirmed when they are finally shown to have a common basis. Finally we consider using nonmonotonic logics to represent reasoning about change.     

Formal reasoning for analyzing goal models that evolve over time

Requirements Engineering - In early-phase requirements engineering, modeling stakeholder goals and intentions helps stakeholders understand the problem context and evaluate tradeoffs, by exploring...     

Designing a toolkit to support dialogue in learning

Whilst the use of dialogue has many pedagogic advantages to offer Higher Education, implementing it effectively in teaching practice is a complex and problematic process that requires a wide range of expertise. This paper describes one strategy for addressing this issue: the development of a toolkit that supports the process of planning and reflection that practitioners must engage in when attempting to use dialogue in their teaching. After identifying and illustrating some of the issues relating to the use of dialogue, the notion of toolkits will be defined and a methodology for their development outlined. This is then exemplified with the specific case of the design of a toolkit for using dialogue in learning. A study is then described in which this prototype toolkit was evaluated, demonstrating its impact both in terms of changing practice and of developing a critical awareness of the issues relating dialogue and learning, before conclusions are drawn about the wider relevance of the work.     

Moral reasoning and automatic risk reaction during driving

Cognition, Technology & Work - Recent advances in autonomous vehicles promise to revolutionize the transportation system. This perspective has led to new research on a number of open questions,...     

可由用户持续发展的几何自动推理平台的推理算法

目前的几何定理证明器都不具有可持续性。提出一种结构具有一般性的知识表示和能够统一处理所有规则的推理算法，初步实现了可由用户持续发展的几何自动推理平台。该推理平台允许用户添加几何知识，如几何对象、谓词和规则，并可以综合使用多种推理算法，如前推搜索法和一部分面积法，它将更适合用于几何教学。     

Human reasoning about artificial intelligence

Abstract

Recently, several authors (Searle, Penrose, Rychlak) have suggested that AI is a doomed undertaking. In his recent book, Artificial Intelligence and Human Reasoning, Joseph Rychlak repeats many of the arguments of the other critics, as well as offering several of his own. In this paper, taking Rychlak as symptomatic of this new anti-computational intellectual movement, we respond to these arguments and defend AI and personal construct theory against some of the misunderstandings and confusions which we find there.     

Temporal reasoning about fuzzy intervals

Traditional approaches to temporal reasoning assume that time periods and time spans of events can be accurately represented as intervals. Real-world time periods and events, on the other hand, are often characterized by vague temporal boundaries, requiring appropriate generalizations of existing formalisms. This paper presents a framework for reasoning about qualitative and metric temporal relations between vague time periods. In particular, we show how several interesting problems, like consistency and entailment checking, can be reduced to reasoning tasks in existing temporal reasoning frameworks. We furthermore demonstrate that all reasoning tasks of interest are NP-complete, which reveals that adding vagueness to temporal reasoning does not increase its computational complexity. To support efficient reasoning, a large tractable subfragment is identified, among others, generalizing the well-known ORD Horn subfragment of the Interval Algebra (extended with metric constraints).     

Towards reasoning about Hoare relations

A logical framework is presented for defining semantics of programs that satisfy Hoare postulates. The two families of logical systems are given: modal systems and relational systems. In the modal systems semantics of Hoare-style programming languages is provided in terms of relations and sets, and in relational systems in terms of relations only. Proof theory for the given logics is presented.     

Formal automatic verification of cache coherence in multiprocessors with relaxed memory models

State-based, formal methods have been successfully applied to the automatic verification of cache coherence in sequentially consistent systems. However, coherence in shared memory multiprocessors under a relaxed memory model is much more complex to verify automatically. With relaxed memory models, incoming invalidations and outgoing updates can be delayed in each cache while processors are allowed to race ahead. This buffering of memory accesses considerably increases the amount of state in each cache and the complexity of protocol interactions. Moreover, because caches can hold inconsistent copies of the same data for long periods of time, coherence cannot be verified by simply checking that cached copies are identical at all times. This paper makes two major contributions. First, we demonstrate how to model and verify cache coherence under a relaxed memory model in the context of state-based verification methods. Frameworks for modeling the hardware and for generating correct memory access sequences driving the hardware model are developed. We also show correctness properties which must be verified on the hardware model. Second, we demonstrate a successful application of a state-based verification tool called SSM for the verification of the delayed protocol, an aggressive protocol for relaxed memory models. SSM is based on an abstraction technique preserving the properties to verify. We show that with classical, explicit approaches the verification of cache coherence is realistically unfeasible because of the state space explosion problem, whereas SSM is able to verify protocols both at both behavioral and message-passing levels.