A Hybrid Logic for Reasoning about Knowledge and Topology

We extend Moss and Parikh’s bi-modal system for knowledge and effort by means of hybrid logic. In this way, some additional concepts from topology related to knowledge can be captured. We prove the soundness and completeness as well as the decidability of the extended system. Special emphasis will be placed on algebras.     

Reasoning About Truth in First-Order Logic

First, we describe a psychological experiment in which the participants were asked to determine whether sentences of first-order logic were true or false in finite graphs. Second, we define two proof systems for reasoning about truth and falsity in first-order logic. These proof systems feature explicit models of cognitive resources such as declarative memory, procedural memory, working memory, and sensory memory. Third, we describe a computer program that is used to find the smallest proofs in the aforementioned proof systems when capacity limits are put on the cognitive resources. Finally, we investigate the correlation between a number of mathematical complexity measures defined on graphs and sentences and some psychological complexity measures that were recorded in the experiment.     

A Default Logic Based Framework for Context-Dependent Reasoning with Lexical Knowledge

Lexical knowledge is increasingly important in information systems—for example in indexing documents using keywords, or disambiguating words in a query to an information retrieval system, or a natural language interface. However, it is a difficult kind of knowledge to represent and reason with. Existing approaches to formalizing lexical knowledge have used languages with limited expressibility, such as those based on inheritance hierarchies, and in particular, they have not adequately addressed the context-dependent nature of lexical knowledge. Here we present a framework, based on default logic, called the dex framework, for capturing context-dependent reasoning with lexical knowledge. Default logic is a first-order logic offering a more expressive formalisation than inheritance hierarchies: (1) First-order formulae capturing lexical knowledge about words can be inferred; (2) Preferences over formulae can be based on specificity, reasoning about exceptions, or explicit priorities; (3) Information about contexts can be reasoned with as first-order formulae formulae; and (4) Information about contexts can be derived as default inferences. In the dex framework, a word for which lexical knowledge is sought is called a query word. The context for a query word is derived from further words, such as words in the same sentence as the query word. These further words are used with a form of decision tree called a context classification tree to identify which contexts hold for the query word. We show how we can use these contexts in default logic to identify lexical knowledge about the query word such as synonyms, antonyms, specializations, meronyms, and more sophisticated first-order semantic knowledge. We also show how we can use a standard machine learning algorithm to generate context classification trees.     

A Logic for Reasoning about Generic Judgments

This paper presents an extension of a proof system for encoding generic judgments, the logic FOλ^Δ of Miller and Tiu, with an induction principle. The logic FOλ^Δ is itself an extension of intuitionistic logic with fixed points and a “generic quantifier”, , which is used to reason about the dynamics of bindings in object systems encoded in the logic. A previous attempt to extend FOλ^Δ with an induction principle has been unsuccessful in modeling some behaviours of bindings in inductive specifications. It turns out that this problem can be solved by relaxing some restrictions on , in particular by adding the axiom B≡x.B, where x is not free in B. We show that by adopting the equivariance principle, the presentation of the extended logic can be much simplified. Cut-elimination for the extended logic is stated, and some applications in reasoning about an object logic and a simply typed λ-calculus are illustrated.     

A Logic for Conditional Local Strategic Reasoning

Journal of Logic, Language and Information - We consider systems of rational agents who act and interact in pursuit of their individual and collective objectives. We study and formalise the...     

Reasoning About Agent Types and the Hardest Logic Puzzle Ever

In this paper, we first propose a simple formal language to specify types of agents in terms of necessary conditions for their announcements. Based on this language, types of agents are treated as ‘first-class citizens’ and studied extensively in various dynamic epistemic frameworks which are suitable for reasoning about knowledge and agent types via announcements and questions. To demonstrate our approach, we discuss various versions of Smullyan’s Knights and Knaves puzzles, including the Hardest Logic Puzzle Ever (HLPE) proposed by Boolos (in Harv Rev Philos 6:62–65, 1996). In particular, we formalize HLPE and verify a classic solution to it. Moreover, we propose a spectrum of new puzzles based on HLPE by considering subjective (knowledge-based) agent types and relaxing the implicit epistemic assumptions in the original puzzle. The new puzzles are harder than the previously proposed ones in the literature, in the sense that they require deeper epistemic reasoning. Surprisingly, we also show that a version of HLPE in which the agents do not know the others’ types does not have a solution at all. Our formalism paves the way for studying these new puzzles using automatic model checking techniques.     

基于描述逻辑的电机故障诊断知识表示与推理

针对传统电机故障诊断专家系统中知识表示方法的不足,提出一种基于描述逻辑的电机故障诊断领域知识描述方法,并在此基础上对所构建的电机故障知识库进行了逻辑检错推理.通过对电机故障诊断领域知识进行表示和推理,可以有效地表示电机故障知识之间的关系,检测知识逻辑体系错误.在实验过程中,利用本体编辑工具Protégé采用OWL语言对其进行了实现,并通过TABLEAU算法实现了逻辑检错推理.     

一种带缺省推理的描述逻辑

该文提出了一种新的带缺省推理的描述逻辑,它以描述逻辑为主要框架,对单调逻辑和非单调逻辑进行了整合,但又避免了一般缺省逻辑的困难．基于带缺省推理的描述逻辑,构建了一种同时具有Tbox,Abox和缺省规则的知识库系统,研究了带缺省推理的描述逻辑的可满足性、缺省可满足性、概念包含、缺省包含以及实例检测等推理问题,提出了一种用来检测可满足性和缺省可满足性的Tableau—D算法,并得到了缺省可满足性和缺省包含的转换定理．     

Reasoning Processes in Propositional Logic

We conducted a computer-based psychological experiment in which a random mix of 40 tautologies and 40 non-tautologies were presented to the participants, who were asked to determine which ones of the formulas were tautologies. The participants were eight university students in computer science who had received tuition in propositional logic. The formulas appeared one by one, a time-limit of 45 s applied to each formula and no aids were allowed. For each formula we recorded the proportion of the participants who classified the formula correctly before timeout (accuracy) and the mean response time among those participants (latency). We propose a new proof formalism for modeling propositional reasoning with bounded cognitive resources. It models declarative memory, visual memory, working memory, and procedural memory according to the memory model of Atkinson and Shiffrin and reasoning processes according to the model of Newell and Simon. We also define two particular proof systems, T and NT, for showing propositional formulas to be tautologies and non-tautologies, respectively. The accuracy was found to be higher for non-tautologies than for tautologies (p < .0001). For tautologies the correlation between latency and minimum proof length in T was .89 and for non-tautologies the correlation between latency and minimum proof length in NT was .87.     

Informational Logic as a Tool for Automated Reasoning

A logical entropy-based Informational Logic is presented which provides new tools for probabilistic automated reasoning and knowledge representation. Applications in automated theorem proving are examined, and a decision theory for probabilistic theorems is proposed.     

一个基于实例推理的软件过程知识复用方法

过程资产库的建立和基于过程资产的项目过程定义是一个组织的软件能力成熟度达到已定义级的关键标志,传统的过程资产库中存储的过程往往是通过文字描述和使用者判断其适用性,用于项目过程的建立。本文提出了一种基于实例推理(CBR)的过程知识复用方法,通过过程特征的刻画和实例相似度计算,实现过程实例的提取和复用。实践证明,该方法有助于提高过程知识复用的准确度和自动化程度,为软件过程改进中的过程建立提供有效手段。     

A Logic with Relative Knowledge Operators

We study a knowledge logic that assumes that to each set of agents, an indiscernibility relation is associated and the agents decide the membership of objects or states up to this indiscernibility relation. Its language contains a family of relative knowledge operators. We prove the decidability of the satisfiability problem, we show its EXPTIME-completeness and as a side-effect, we define a complete Hilbert-style axiomatization.     

Abductive Knowledge Base Updates for Contextual Reasoning

We show in this paper how procedures that update knowledge bases can naturally be adapted to a number of problems related to contextual reasoning. The fact that the update procedures are abductive in nature is favourably exploited to tackle problems related to human-computer dialogue systems. We consider as examples aspects of pronoun resolution,goal formulation , and the problem of restoring the consistency of a knowledge base after some knowledge update is carried out. We state these problems in terms of the update problem and abductive reasoning and show how procedures that update knowledge bases yield some interesting results. We also explain how these procedures can naturally be used to model various forms of hypothetical reasoning such as hypothesizing inconsistencies and performing some look ahead form of reasoning.We do not claim thaT the problems presented here are solved entirely within the update framework. However, we believe that the flexibility of the representation and of the problem-solving approach suggest that the problems could be solved by adding more details about each problem. What is most interesting in our understanding is that all the aforementioned problems are expressed and tackled within the same framework.     

Reasoning in a Restricted Temporal Logic

We consider RTL, a linear time propositional temporal logic whose only modalities are the [formula] (eventually) operator and its dual [formula] (always). Although less expressive than the full temporal logic, RTL is the fragment of temporal logic that is used most often and in many verification systems. Indeed, many properties of distributed systems discussed in the literature are RTL properties. Another advantage of RTL over the full temporal logic is in the decidability procedure; while deciding satisfiability of a formula in full temporal logic is a PSPACE complete procedure, doing so for an RTL formula is in NP. We characterize the class of ω-regular languages that are definable in RTL and show simple translations between ω-regular sets and RTL formulae that define them. We explore the applications of RTL in reasoning about communication systems. Finally, we relate variants of RTL (when interpreted over a real line segments) to several fragments of Interval Modal Logic and show that the satisfiability problem for RTL when interpreted over a real line is NP-complete.     

基于常识的亲属关系推理模型

常识知识的研究与发展得到了人工智能界的很大重视。文章建立了一个基于常识的人物亲属关系推理模型,研究了亲属关系常识以及人物信息的表示与存储。此外,对实际所要解决的问题进行了总结。     

Multi-Dimensional Modal Logic as a Framework for Spatio-Temporal Reasoning

In this paper we advocate the use of multi-dimensional modal logics as a framework for knowledge representation and, in particular, for representing spatio-temporal information. We construct a two-dimensional logic capable of describing topological relationships that change over time. This logic, called PSTL (Propositional Spatio-Temporal Logic) is the Cartesian product of the well-known temporal logic PTL and the modal logic S4_u, which is the Lewis system S4 augmented with the universal modality. Although it is an open problem whether the full PSTL is decidable, we show that it contains decidable fragments into which various temporal extensions (both point-based and interval based) of the spatial logic RCC-8 can be embedded. We consider known decidability and complexity results that are relevant to computation with multi-dimensional formalisms and discuss possible directions for further research.