Using crucial literals to select better theories

When Horn clause theories are combined with integrity constraints to produce potentially refutable theories, Seki and Takeuchi have shown how crucial literals can be used to discriminate two mutually incompatible theories. A literal is crucial with respect to two theories if only one of the two theories supports the derivation of that literal. In other words, actually determining the truth value of the crucial literal will refute one of the two incompatible theories. This paper presents an integration of the idea of crucial literal with Theorist, a logic-based system for hypothetical reasoning. Theorist is a goal-directed nonmonotonic reasoning system that classifies logical formulas as possible hypotheses, facts, and observations. As Theorist uses full clausal logic, it does not require Seki and Takeuchi's notion of integrity constraint to define refutable theories. In attempting to deduce observation sentences, Theorist identifies instances of possible hypotheses as nomological explanations: consistent sets of hypothesis instances required to deduce observations. As multiple and mutually incompatible explanations are possible, the notion of crucial literal provides the basis for proposing experiments that distinguish competing explanations. We attempt to make three contributions. First, we adapt Seki and Takeuchi's method for Theorist. To do so, we incrementally use crucial literals as experiments, whose results are used to reduce the total number of explanations generated for a given set of observations. Next, we specify an extension which incrementally constructs a table of all possible crucial literals for any pair of theories. This extension is more efficient and provides the user with greater opportunity to conduct experiments to eliminate falsifiable theories. A prototype is implemented in CProlog, and several examples of diagnosis are considered to show its empirical efficiency. Finally, we point out that assumption-based truth maintenance systems (ATMS), as used in the multiple fault diagnosis system of de Kleer and Williams, are interesting special cases of this more general method of distinguishing explanatory theories.     

ASSUMPTION-BASED REASONING AND CLAUSE MANAGEMENT SYSTEMS

A truth maintenance system is a subsystem that manages the utilization of assumptions in the reasoning process of a problem solver. Doyle's original motivation for creating a truth maintenance system was to augment a reasoning system with a control strategy for activities concerning its nonmonotonic state of beliefs. Hitherto, much effort has been invested in designing and implementing the concept of truth maintenance, and little effort has been dedicated to the formalization that is essential to understanding it. This paper provides a complete formalization of the principle of truth maintenance. Motivated by Reiter and de Kleer's preliminary report on the same subject, this paper extends their study and gives a formal account of the concept of truth maintenance under the general title of assumption-based reasoning. The concept of assumption-based theory is defined, and the notions of explanation and direct consequence are presented as forms of plausible conclusions with respect to this theory. Additionally, the concepts of extension and irrefutable sentences are discussed together with other variations of explanation and direct consequence. A set of algorithms for computing these conclusions for a given theory are presented using the notion of prime implicates. Finally, an extended example on Boolean circuit diagnosis is shown to exemplify these ideas.     

溯因推理问题的碰集求解方法

溯因推理为归纳与演绎推理之外的另一种重要的推理形式,在人工智能等领域有着广泛的应用.通俗地讲,溯因推理是从观察(结果)去推断原因的推理过程.不同于以往的研究思路,通过使用本原蕴含式和素蕴含,证明了可以把命题逻辑和命题模态逻辑系统S5中求溯因问题的极小解释转化为求对应集合的极小碰集问题.给出了求解溯因问题的一种新方法.     

Checking the consistency of a hybrid knowledge base system

This paper concerns a method to verify the consistency of a hybrid knowledge base system. We assume the knowledge base of the verified system supports the representation of production rules and frame taxonomies. Moreover, the knowledge base can also be used to represent non-monotonic and uncertain reasoning. For the purpose of the verification, an ATMS like theory is created by simulating the deductive process needed to deduce an inconsistency. Next, the ATMS like theory is processed to compute a specification of the initial fact base that allows for the execution of a deductive tree that leads to the inconsistency.     

Computing prime implicants via transversal clauses

In this paper, the notion of transversal clauses is introduced and subsequently a new algorithm for computing prime implicants is developed. Opposed to the common approach of computing prime implicants of a dnf, the proposed algorithm uses a cnf representation of a propositional formula. The same algorithm applied on a dnf representation yields the set of prime implicates of a formula. Besides its suitability for implementation in a parallel environment and as an incremental algorithm, it has been found to work faster in case, the number of prime implicants is large.     

扩展AL-log挖掘日志本体的ILP方法

为发现Web使用记录中所蕴涵的用户访问模式,在深入分析日志本体中事件间的抽象关系后,提出适用于原子事件和复合事件间整分关系推理的ALC传播规则扩展已有的推理模式,并在此基础上提出一种挖掘日志本体的ILP方法.该方法结合描述逻辑和Horn规则在知识表示和推理过程中互补的特点,采用AL-log混合系统构建知识库,利用约束SLD-反驳消解和扩展ALC传播规则从日志本体中学习用户访问模式,达到站点商业智能和个性化的目的.最后给出验证该方法的实例,实验结果表明了该方法的可行性和有效性.     

A generic, object-oriented case-knowledge representation scheme, and its integration into a wider information management scenario

Abstract: A knowledge base management system (KBMS) realises a combination of techniques found in database management systems and knowledge-based systems. At the data model and knowledge representation level, many systems of this kind constitute a marriage of the relational data model and the rule-based reasoning. Experience has shown that either approach is restricted in the way it can express the demanding information and knowledge structures required for applications like decision support systems. Two new technologies offer an exciting new integrated approach to knowledge management. Object-oriented database management systems (OODBMS) provide an object model that supports powerful abstraction mechanisms to facilitate the modelling of highly structured information. Whereas case-based reasoning (CBR) systems are knowledge bases which organise their capabilities around a memory of past cases and the notion of similarity. Both types of system are built upon two fundamental concepts: 1) the retrieval of entities with potentially complex structure, called objects in the former, and cases in the latter type of system; 2) the organisation of those entities in collections with common characteristics. In an OODBMS such collections are termed extents, and in CBR they are usually called categories. In either system, the conceptual meta notion to represent both, objects as well as extents, and cases as well as categories, is the class.
Revolving around a Conceptual Case Class and extending a standard object model, this paper proposes a novel and general approach to represent case-knowledge and to build KBMSs. The work presented here is a spin-off of the design of an object query language within the ESPRIT project Lynx.     

基于MiniSAT的命题极小模型计算方法

计算命题公式的极小模型在人工智能推理系统中是一项必不可少的任务.然而,即使是正CNF(conjunctive normal form)公式,其极小模型的计算和验证都不是易处理的.当前,计算CNF公式极小模型的主要方法之一是将其转换为析取逻辑程序后用回答集程序(answer set programming, ASP)求解器计算其稳定模型/回答集.针对计算CNF公式的极小模型的问题,提出一种基于可满足性问题(satisfiability problem, SAT)求解器的计算极小模型的方法MMSAT;然后结合最近基于极小归约的极小模型验证算法CheckMinMR,提出了基于极小模型分解的计算极小模型方法MRSAT;最后对随机生成的大量的3CNF公式和SAT国际竞赛上的部分工业基准测试用例进行测试.实验结果表明：MMSAT和MRSAT对随机3CNF公式和SAT工业测试用例都是有效的,且计算极小模型的速度都明显快于最新版的clingo,并且在SAT工业实例上发现了clingo有计算出错的情况,而MMSAT和MRSAT则更稳定.     

Algorithmic Debugging and Hypothetical Reasoning

This paper presents a generalization of Shapiro style algorithmic debugging for generalized Horn clause intuitionistic logic. This logic offers hypothetical reasoning and negation is defined not by failure but by inconsistency. We extend Shapiro's notion of intended interpretation, symptoms and errors and give formal results paralleling those known for definite clauses. We also show how a corresponding diagnosis module for RISC- a logic programming system for generalized Horn clause intuitionistic logic-can be defined by meta interpretation. In contrast to Shapiro's PROLOG modules ours work independently of the specific computation rule that in RISC may be specified by the user.     

CNF and DNF Considered Harmful for Computing Prime Implicants/Implicates

Several methods to compute the prime implicants and the prime implicates of a negation normal form (NNF) formula are developed and implemented. An algorithm PI is introduced that is an extension to negation normal form of an algorithm given by Jackson and Pais. A correctness proof of the PI algorithm is given. The PI algorithm alone is sufficient in a computational sense. However, it can be combined with path dissolution, and it is shown empirically that this is often an advantage. None of these variations rely on conjunctive normal form or on disjunctive normal form. A class of formulas is described for which reliance on CNF or on DNF results in an exponential increase in the time required to compute prime implicants/implicates. The possibility of avoiding this problem with efficient structure preserving clause form translations is examined briefly and appears unfavorable.     

一阶子句搜索方法

子句集的可满足性判定是自动证明领域的热点之一.提出了子句搜索方法判定命题子句集Φ的可满足性,该方法查找Φ中子句的一个公共不可扩展子句C,当且仅当找到C时Φ可满足,此时C中各文字的补构成一个模型.结合部分实例化方法将子句搜索方法提升至一阶.一阶子句搜索方法可以判定子句集的M可满足性,具备终止性、正确性和完备性,是一种判定子句集可满足性的有效方法.     

命题模态归结的一种变型

本文给出了模态子句集的标准子句集概念，提出了一种基于标准子句集的模态归结方法的变型，称之为标准模态归结，证明了任意模态子句集恒假当且仅当存在从它的标准子句集出发，使用标准模态归结推出空子句的演绎，从而证明了对于不可满足标准子句集、标准模态归结是完备的，这种标准模态归结，揄规则简单、直观且容易实现。     

Quantitative deduction and its fixpoint theory

Logic programming provides a model for rule-based reasoning in expert systems. The advantage of this formal model is that it makes available many results from the semantics and proof theory of first-ordet predicate logic. A disadvantage is that in expert systems one often wants to use, instead of the usual two truth values, an entire continuum of “uncertainties” in between. That is, instead of the usual “qualitative” deduction, a form of “quantitative” deduction is required. We present an approach to generalizing the Tarskian semantics of Horn clause rules to justify a form of quantitative deduction. Each clause receives a numerical attenuation factor. Herbrand interpretations, which are subsets of the Herbrand base, are generalized to subsets which are fuzzy in the sense of Zadeh. We show that as result the fixpoint method in the semantics of Horn clause rules can be developed in much the same way for the quantitative case. As for proof theory, the interesting phenomenon is that a proof should be viewed as a two-person game. The value of the game turns out to be the truth value of the atomic formula to be proved, evaluated in the minimal fixpoint of the rule set. The analog of the PROLOG interpreter for quantitative deduction becomes a search of the game tree ( = proof tree) using the alpha-beta heuristic well known in game theory.     

面向开放文本的逻辑推理知识抽取与事件影响推理探索

开放文本中蕴含着大量的逻辑性知识,以刻画事物之间逻辑传导关系的逻辑类知识库是推动知识推理发展的重要基础,研发大规模逻辑推理知识库有助于支持由实体或事件等传导驱动的决策任务。该文围绕逻辑推理知识库,论述了知识库的概念、类别和基本构成,提出了一种面向大规模开放文本的实体描述、事件因果逻辑知识快速抽取方法;面向金融领域,探索了一套基于逻辑推理知识库的可解释性路径推理方法和金融实体影响生成系统。算法模型和系统均取得了不错的效果。