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.     

基于一阶模态逻辑的模糊推理

研究基于可信度的模糊一阶模态逻辑,给出了基于常域的模糊一阶模态逻辑语义以及推理形式系统描述.为有效进行模糊断言间的推理,考虑了模糊约束的概念.模糊约束是一个表达式,其中既有语法成分又包含意义信息.模糊推理形式系统中的基本对象是模糊约束,针对模糊约束引进可满足性概念,研究模糊约束可满足性相关性质.利用模糊约束的概念,模糊断言间的推理可以直接在语义环境下加以考虑,因此,以模糊约束为基本元素的模糊推理形式系统随之建立.主要分析新产生断言有效性与模糊约束集可满足性之间的关系,并在此基础上给出了模糊推理形式系统的推理规则.进一步的工作可探讨模糊推理形式系统的可靠性与完全性,建立推理过程的能行机制.研究结果可在人工智能和计算机科学等领域得以应用.     

Knuth-Bendix Completion for Non-Symmetric Transitive Relations

We extend the Knuth-Bendix completion procedure from equational rewriting to rewriting with non-symmetric transitive relations and quasi-orderings. The main differences are the following: Specification of the general non-ground case seems beyond first-order logic. It is within that realm when terms are linear or functions non-monotonic. The procedure requires critical-pair computations and need not terminate even in the ground case. Simplification is not don't care non-deterministic, but search based. Applications include ordered resolution and ordered chaining calculi, development of rule-based declarative procedures and algorithms, program and reachability analysis (in rewriting logic) and propagation of inequality constraints.     

Automated Refinement of First-Order Horn-Clause Domain Theories

Knowledge acquisition is a difficult, error-prone, and time-consuming task. The task of automatically improving an existing knowledge base using learning methods is addressed by the class of systems performing theory refinement. This paper presents a system, forte (First-Order Revision of Theories from Examples), which refines first-order Horn-clause theories by integrating a variety of different revision techniques into a coherent whole. FORTE uses these techniques within a hill-climbing framework, guided by a global heuristic. It identifies possible errors in the theory and calls on a library of operators to develop possible revisions. The best revision is implemented, and the process repeats until no further revisions are possible. Operators are drawn from a variety of sources, including prepositional theory refinement, first-order induction, and inverse resolution. FORTE is demonstrated in several domains, including logic programming and qualitative modelling.     

语义网的一阶逻辑推理技术支持

研究了一阶逻辑推理工具对语义网的推理支持.语义网的关键推理问题可以化为公式的可满足性判定问题.一阶逻辑的自动定理证明器可以证明不可满足性,而有限模型查找器为可满足的公式在有限域内构造模型.提出在语义网的推理中,同时使用定理证明器和有限模型查找器.实验结果表明,这样可以解决描述逻辑工具的不足,并可以弥补定理证明器对可满足的公式推理的不完备性.     

An Exception Handling of Rule-Based Reasoning Using Case-Based Reasoning

In this paper, we propose the CCAR (Combining Case-based And Rule-based reasoning) model for an exception handling of Rule-based Reasoning using Case-based Reasoning. The central idea of the model proposed in this paper is to represent the exception of a rule as a case, and to utilize the case for a solution to a problem, and then to search the case memory to retrieve a case which violates the conclusion of a rule. If the similarity between a target problem and the selected case is high, the conclusion of a case is applied. Otherwise, the conclusion of rule-based reasoning is applied.     

Learning-Assisted Automated Reasoning with Flyspeck

The considerable mathematical knowledge encoded by the Flyspeck project is combined with external automated theorem provers (ATPs) and machine-learning premise selection methods trained on the Flyspeck proofs, producing an AI system capable of proving a wide range of mathematical conjectures automatically. The performance of this architecture is evaluated in a bootstrapping scenario emulating the development of Flyspeck from axioms to the last theorem, each time using only the previous theorems and proofs. It is shown that 39 % of the 14185 theorems could be proved in a push-button mode (without any high-level advice and user interaction) in 30 seconds of real time on a fourteen-CPU workstation. The necessary work involves: (i) an implementation of sound translations of the HOL Light logic to ATP formalisms: untyped first-order, polymorphic typed first-order, and typed higher-order, (ii) export of the dependency information from HOL Light and ATP proofs for the machine learners, and (iii) choice of suitable representations and methods for learning from previous proofs, and their integration as advisors with HOL Light. This work is described and discussed here, and an initial analysis of the body of proofs that were found fully automatically is provided.     

基于tableau的自动推理技术综述

tableau方法是一种接近于逻辑系统表示的自动推理方法,由于其直观性和通用性,易于计算机实现,成为目前最普及的自动推理方法之一。在提高系统效率方面,主要在相关技术和策略、理论和方法等方面进行了分析,并展望了未来的研究方向。     

基于语义tableau的一阶逻辑自动定理证明

自动推理作为自动定理证明的扩展是人工智能研究的基础工作,许多重要的人工智能系统都是以推理系统为其核心部分,其中的tableau方法,由于具有通用性、直观性及易于计算机实现等特点,至今成为重要的自动推理方法之一。在tableau方法基础上,讨论了一阶逻辑中的自动定理证明理论,提出使用模型存在定理证明其可靠性和完备性的方法。同时也给出了带等词tableau方法的证明过程。     

The Possibilistic Handling of Irrelevance in Exception-Tolerant Reasoning

In nonmonotonic reasoning, the preferential system P is known to provide reasonable but very cautious conclusions, and in particular, preferential inference is blocked by the presence of irrelevant properties. When using Lehmann's rational closure, the inference machinery, which is then more productive, may still remain too cautious. These two types of inference can be represented using a possibility theory-based semantics. To overcome the cautiousness of system P, we first progressively augment preferential inference with two extensions which are in between system P and rational closure. Then, in order to overcome some remaining limitations of rational closure the second half of this paper focuses more particularly on the use of (contextual) independence assumptions of the form: the fact that is true (or is false) does not affect the validity of the rule normally if then . The modelling of such independence assumptions is discussed in the possibilistic framework. Algorithms are provided to jointly handle default rules and independence relations, and to check their multual consistency.     

基于等价类推理的几何自动推理网

为了提高推理引擎的推理效率,将Rete算法和等价类推理技术整合到基于规则的几何自动推理系统中,构造一种新的推理引擎,即基于等价类推理的几何自动推理网.采用Lisp语言实现该推理引擎,并做了50多个非平凡几何定理的实验,实验结果表明该推理引擎具有更高的推理效率.     

一种基于桶树的自动推理问题求解算法

桶消元和连接树推理算法是处理自动推理问题的两种常用的推理算法。针对连接树推理算法中消息传播效率问题,提出了一种能有效进行消息传播的连接树推理算法JTR。针对桶消元推理算法BE处理多任务的自动推理问题效率低下的问题,采用连接树结构和连接树推理算法JTR的消息传播方式对桶消元算法BE进行改进和扩展,提出了一种桶树推理算法BJTR。通过对算法BE、BTE和BJTR的时空性能分析发现:与同类算法BTE相比,算法BJTR在空间略有下降的情况下提高了时间性能;针对多任务的自动推理问题,与桶消元推理算法BE相比,BJTR算法的空间略有下降,时间性能得到明显提高;并通过实例和实验进一步验证了算法BJTR针对多任务的自动推理任务具有良好的时间性能。     

A Framework for Automated Reasoning in Multiple-Valued Logics

The language of signed formulas offers a first-order classical logic framework for automated reasoning in multiple-valued logics. It is sufficiently general to include both annotated logics and fuzzy operator logics. Signed resolution unifies the two inference rules of annotated logics, thus enabling the development of an SLD-style proof procedure for annotated logic programs. Signed resolution also captures fuzzy resolution. The logic of signed formulas offers a means of adapting most classical inference techniques to multiple-valued logics.     

基于SOLe的自动推理算法

研究不确定型数据时,针对宏观上缺失数据和噪声数问题,提出了一种应用于智能决策系统的自动推理方法,可以有效地从不确定型数据中提取知识并完成无监督分类,从而提高整个决策系统的正确性和鲁棒性.通过对非结构化知识的分析,采用二阶逻辑在取值论域内增设集合形式的谓词变量与量词变量,结合指数分布簇的区间参数估计对二阶逻辑进行修正,建立基于扩展二阶逻辑的精度较高的自动推理模型框架.使用UCI机器学习数据集中的数据,通过仿真实验分析验证了算法在正确性和鲁棒性上提升约7%和6.5%,并可以得到准确数据集.在智能决策和专家系统中都将提供一种新的研究方法.     

基于案例推理的工作流异常处理研究

对工作流的异常和案例推理(Case-Based Reasoning,简称CBR)的机制进行了介绍,给出了一个应用CBR技术进行异常处理的工作流模型,并研究了应用CBR方法处理工作流异常的机制。     

分布式环境下事件自动处理机制的实现

提出了一种分布式环境下事件的自动处理机制.该机制基于符合JMS规范的消息中间件完成事件的发布和订阅,采用XML和动态连接库技术实现了一个即插即用的、支持事件定制和事件处理过程自动加载的处理框架.它是一个分布式环境下完整的事件处理解决方案.     

Efficient Transitive Closure Reasoning in a Combined Class/Part/Containment Hierarchy

Class hierarchies form the backbone of many implemented knowledge representation and reasoning systems. They are used for inheritance, classification and transitive closure reasoning. Part hierarchies are also important in artificial intelligence. Other hierarchies, e.g. containment hierarchies, have received less attention in artificial intelligence. This paper presents an architecture and an implementation of a hierarchy reasoner that integrates a class hierarchy, a part hierarchy, and a containment hierarchy into one structure. In order to make an implemented reasoner useful, it needs to operate at least at speeds comparable to human reasoning. As real-world hierarchies are always large, special techniques need to be used to achieve this. We have developed a set of parallel algorithms and a data representation called maximally reduced tree cover for that purpose. The maximally reduced tree cover is an improvement of a materialized transitive closure representation which has appeared in the literature. Our experiments with a medical vocabulary show that transitive closure reasoning for combined class/part/containment hierarchies in near constant time is possible for a fixed hardware configuration. Received 10 January 2000 / Revised 25 November 2000 / Accepted in revised form 9 February 2001     

提高一阶多值逻辑Tableau推理效率的布尔剪枝方法

含有量词的一阶多值Tableau方法具有统一的扩展规则，并由Zabel等人给出了可靠性和完备性的证明，但由于扩展后的分枝随着真值数目的增加而呈指数的增加，因而影响了机器推理执行的效率，该文提出了布尔剪枝方法，将带符号的公式与集合的上集／下集联系起来，使含量词的一阶多值逻辑公式的扩展规则大大简化，进一步，通过对布尔剪枝方法的分析，建立了一类特殊一阶多值逻辑正则公式的更为简洁的Tableau推理方法，该方法使得含量词的一阶多值逻辑Tableau推理类同于经典逻辑Tableau方法。     

Comparing Instance Generation Methods for Automated Reasoning

The clause-linking technique of Lee and Plaisted proves the unsatisfiability of a set of first-order clauses by generating a sufficiently large set of instances of these clauses that can be shown to be propositionally unsatisfiable. In recent years, this approach has been refined in several directions, leading to both tableau-based methods, such as the disconnection tableau calculus, and saturation-based methods, such as primal partial instantiation and resolution-based instance generation. We investigate the relationship between these calculi and answer the question to what extent refutation or consistency proofs in one calculus can be simulated in another one. This work was partly supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS). See for more information.