Automated Reasoning About Classical Mechanics

In recent years, researchers in artificial intelligence have become interested in replicating human physical reasoning talents in computers. One of the most important skills in this area is predicting how physical systems will behave. This thesis discusses an implemented program that generates algebraic descriptions of how systems of rigid bodies evolve over time. Discussion about the design of this program identifies a physical reasoning paradigm and knowledge representation approach based on mathematical model construction and algebraic reasoning. This paradigm offers several advantages over methods that have become popular in the field, and seems promising for reasoning about a wide variety of classical mechanics problems.

Automated Reasoning II

Resolution over FOPL

Kanger's Choices in Automated Reasoning

This article explains these choices and their place in modern automated deduction.

Reasoning with multimedia information using symbolic projection

In many multimedia application systems, it is not the final goal to retrieve the relevant multimedia information from different multimedia information sources. Rather, post-processing of the retrieved multimedia information is needed. For example, the retrieved information is used as “known facts”. The systems will do some reasoning to obtain further conclusions based on these multimedia form “known facts”. We call this reasoning with multimedia information. Most current research work in multimedia information processing is focused on multimedia information retrieval, but post-processing the retrieved information is more or less ignored. This paper explores the way to tackle this problem by using symbolic projection. A case study of reasoning with still image information is presented. Some extensions to symbolic projection- introducing auxiliary pictorial objects in symbolic pictures that need to be processed-are discussed. We expect this paper will stimulate further research on this important but ignored topic.

Ontology-based automated support for goal–use case model analysis

Combining goal-oriented and use case modeling has been proven to be an effective method in requirements elicitation and elaboration. To ensure the quality of such modeled artifacts, a detailed model analysis needs to be performed. However, current requirements engineering approaches generally lack reliable support for automated analysis of consistency, correctness and completeness (3Cs problems) between and within goal models and use case models. In this paper, we present a goal–use case integration framework with tool support to automatically identify such 3Cs problems. Our new framework relies on the use of ontologies of domain knowledge and semantics and our goal–use case integration meta-model. Moreover, functional grammar is employed to enable the semiautomated transformation of natural language specifications into Manchester OWL Syntax for automated reasoning. The evaluation of our tool support shows that for representative example requirements, our approach achieves over 85 % soundness and completeness rates and detects more problems than the benchmark applications.

Virtual design process : design validation tool schematic approach in car carrier

An important aspect of designing any product is validation. Virtual design process (VDP) is an alternative to hardware prototyping in which analysis of designs can be done without manufacturing physical samples. In recent years, VDP have been generated either for animation or filming applications. This paper proposes a virtual reality design process model on one of the applications when used as a validation tool. This technique is used to generate a complete design guideline and validation tool of product design. To support the design process of a product, a virtual environment and VDP method were developed that supports validation and an initial design cycle performed by a designer. The product model car carrier is used as illustration for which virtual design was generated. The loading and unloading sequence of the model for the prototype was generated using automated reasoning techniques and was completed by interactively animating the product in the virtual environment before complete design was built. By using the VDP process critical issues like loading, unloading, Australian Design rules (ADR) and clearance analysis were done. The process would save time, money in physical sampling and to large extent in complete math generation. Since only schematic models are required, it saves time in math modelling and handling of bigger size assemblies due to complexity of the models. This extension of VDP process for design evaluation is unique and was developed, implemented successfully. In this paper a Toll logistics and J Smith and Sons car carrier which is developed under author’s responsibility has been used to illustrate our approach of generating design validation via VDP.

A model for computer profiling

This paper discusses the use of models in automatic computer forensic analysis, and proposes and elaborates on a novel model for use in computer profiling, the computer profiling object model. The computer profiling object model is an information model which models a computer as objects with various attributes and inter-relationships. These together provide the information necessary for a human investigator or an automated reasoning engine to make judgements as to the probable usage and evidentiary value of a computer system. The computer profiling object model can be implemented so as to support automated analysis to provide an investigator with the information needed to decide whether manual analysis is required.

Partial instantiation methods for inference in first-order logic

Satisfiability algorithms for propositional logic have improved enormously in recently years. This improvement increases the attractiveness of satisfiability methods for first-order logic that reduce the problem to a series of ground-level satisfiability problems. R. Jeroslow introduced a partial instantiation method of this kind that differs radically from the standard resolution-based methods. This paper lays the theoretical groundwork for an extension of his method that is general enough and efficient enough for general logic programming with indefinite clauses. In particular we improve Jeroslow's approach by (1) extending it to logic with functions, (2) accelerating it through the use of satisfiers, as introduced by Gallo and Rago, and (3) simplifying it to obtain further speedup. We provide a similar development for a "dual" partial instantiation approach defined by Hooker and suggest a primal-dual strategy. We prove correctness of the primal and dual algorithms for full first-order logic with functions, as well as termination on unsatisfiable formulas. We also report some preliminary computational results.

basic research in computer science and software engineering at sklcs

The State Key Laboratory of Computer Science (SKLCS) is committed to basic research in computer science and software engineering. The research topics of the laboratory include: concurrency theory, theory and algorithms for real-time systems, formal specifications based on context-free grammars, semantics of programming languages, model checking, automated reasoning, logic programming, software testing, software process improvement, middleware technology, parallel algorithms and parallel software, computer graphics and human-computer interaction. This paper describes these topics in some detail and summarizes some results obtained in recent years.

constructing finite algebras with falcon

The generation of models and counterexamples is an important form of reasoning. In this paper, we give a formal account of a system, called FALCON, for constructing finite algebras from given equational axioms. The abstract algorithms, as well as some implementation details and sample applications, are presented. The generation of finite models is viewed as a constraint satisfaction problem, with ground instances of the axioms as constraints. One feature of the system is that it employs a very simple technique, called the least number heuristic, to eliminate isomorphic (partial) models, thus reducing the size of the search space. The correctness of the heuristic is proved. Some experimental data are given to show the performance and applications of the system.

语义Web中的自动推理和主动规则终止性分析

语义Web是现有Web的一个语义延伸，目标是使Web的应用具有一定的智能，能够进行更准确的信息搜索和一定的决策支持，帮助用户自动完成一些任务。语义Web的实现需要人工智能、数据库等领域的技术支持，需要对已有的技术进行改进和扩展，也需要对现有技术本身如ECA规则进行更深入的研究从而进一步将其扩展到语义Web。自动推理技术是语义Web实现的基础之一，而ECA规则可以为系统增加反应性行为能力，本文围绕自动推理和ECA规则，主要进行了如下研究：（1） 一阶逻辑推理技术对语义Web的推理支持。分析了语义Web语言需要的表达能力，对现有描述逻辑工具、一阶逻辑工具的能力进行了考察。现有的描述逻辑工具不足以处理应用所需要的更丰富的语言成分、任意的一阶逻辑规则等，而一阶逻辑自动定理证明工具和有限模型查找工具有分别都有较好的研究成果。把语义Web的推理问题化成可满足性判定问题后，本文给出了一阶逻辑定理证明器和有限模型查找器形成的并发过程进行可满足性判定的方法。这样既可以解决描述逻辑工具的不足，并可弥补定理证明器对可满足的公式推理的不完备性。（2） ECA规则(主动规则)的终止性分析。终止性是主动规则最重要的行为性质，不终止是由于主动规则的级联触发造成的，意味着定义错误。终止性检查通常是不可判定的。有效的静态分析方法是主动规则得以实际应用的保证。静态分析的关键是合适的数据库状态描述，本文给出用约束表示数据库状态的方法，通过模拟规则执行，使用约束求解进行条件计算和重复状态检查，判断主动规则集合是否终止。用约束精确表示了数据库状态，在规则处理中考虑了执行语义，从而得到更精确的终止性结论。