SATCHMORE: SATCHMO with RElevancy

We introduce a relevancy detection algorithm to be used in conjunction with the SATCHMO prover. The version of SATCHMO considered here is essentially a bidirectional prover, utilizing Prolog (back chaining) on Horn clauses and forward chaining on non-Horn clauses. Our extension, SATCHMORE (SATCHMO with RElevancy), addresses the major weakness of SATCHMO: the uncontrolled use of forward chaining. By marking potentially relevant clause head literals, and then requiring that all the head literals be marked relevant (be totally relevant) before a clause is used for forward chaining, SATCHMORE is able to guide the use of these rules. Furthermore, the relevancy testing is performed without extending the proof search beyond what is done in SATCHMO. A simple implementation of the extended SATCHMO can be written in Prolog. We describe our relevancy testing approach, present the implementation, prove soundness and completeness, and provide examples that demonstrate the power of relevancy testing.This research was partially supported by NSF Grants IRI-8805696 and CCR-9116203. This paper is a major revision of Wilson and Loveland (1989).     

SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy

SATCHMORE was introduced as a mechanism to integrate relevancy testing with the model-generation theorem prover SATCHMO. This made it possible to avoid invoking some clauses that appear in no refutation, which was a major drawback of the SATCHMO approach. SATCHMORE relevancy, however, is driven by the entire set of negative clauses and no distinction is accorded to the query negation. Under unfavorable circumstances, such as in the presence of large amounts of negative data, this can reduce the efficiency of SATCHMORE. In this paper we introduce a further refinement of SATCHMO called SATCHMOREBID: SATCHMORE with BIDirectional relevancy. SATCHMOREBID uses only the negation of the query for relevancy determination at the start. Other negative clauses are introduced on demand and only if a refutation is not possible using the current set of negative clauses. The search for the relevant negative clauses is performed in a forward chaining mode as opposed to relevancy propagation in SATCHMORE which is based on backward chaining. SATCHMOREBID is shown to be refutationally sound and complete. Experiments on a prototype SATCHMOREBID implementation point to its potential to enhance the efficiency of the query answering process in disjunctive databases. Donald Loveland, Ph.D.: He is Emeritus Professor of Computer Science at Duke University. He received his Ph.D. in mathematics from New York University and taught at NYU and CMU prior to joining Duke in 1973. His research in automated deduction includes defining the model elimination proof procedure and the notion of linear resolution. He is author of one book and editor/co-editor of two other books on automated theorem proving. He has done research in the areas of algorithms, complexity, expert systems and logic programming. He is an AAAI Fellow, ACM Fellow and winner of the Herbrand Award in Automated Reasoning. Adnan H. Yahya, Ph.D.: He is an associate professor at the Department of Electrical Engineering, Birzeit University, Palestine. He received his Diploma and PhD degrees from St. Petersburg Electrotechnical University and Nothwestern University in 1979 and 1984 respectively. His research interests are in Artificial Intelligence in general and in the areas of Deductive Databases, Logic Programming and Nonmonotonic Reasoning in particular. He had several visiting appointments at universities and research labs in the US, Germany, France and the UK. Adnan Yahya is a member of the ACM, IEEE and IEEE Computer Society.     

I—SATCHMORE：An Improvement of A—SATCHMORE

This paper presents an improvement of A-SATCHMORE (SATCHMORE with Availability).A-SATCHMORE incorporates relevancy testing and availability checking into SATCHMO to prune away irrelevant forward chaining.However ,considering every consequent atom of those non-Horn clauses being derivable,A-SATCHMORE may suffer from a potential explosion of the search space when some of such consequent atoms are actually underivable.This paper introduces a solution for this problem and shows its correctness.     

Modeling and Verifying Graph Transformations in Proof Assistants

This paper takes first steps towards a formalization of graph transformations in a general setting of interactive theorem provers, which will form the basis for proofs of correctness of graph transformation systems. Whereas graph rewriting is usually performed by mapping a pattern graph into a source graph by means of a graph morphism and then carrying out operations on the image node and edge set, this article generalises the notion of pattern graph to path expressions, which are formulae in a fragment of first-order logic. We examine the correspondence with traditional graph rewriting and show that this interpretation is beneficial when formally reasoning about model transformations with the aid of proof assistants.     

Towards formalising AADL in Proof Assistants

This paper presents first steps towards a formalisation of the Architecture Analysis and Design Language, mainly concentrating on a representation of its data model. For this, we contrast two approaches: one set-based (using the B modelling framework) and one in a higher-order logic (using the Isabelle proof assistant). We illustrate a transformation on a simplified part of the AADL metamodel concerning flows.     

CSP-CASL-Prover: A Generic Tool for Process and Data Refinement

The specification language Csp-Casl allows one to model processes as well as data of distributed systems within one framework. In our paper, we describe how a combination of the existing tools Hets and Csp-Prover can solve the challenges that Csp-Casl raises on integrated theorem proving for processes and data. For building this new tool, the automated generation of theorems and their proofs in Isabelle/HOL plays a fundamental role. A case study of industrial strength demonstrates that our approach scales up to complex problems.     

Bounded Model Generation for Isabelle/HOL

A translation from higher-order logic (on top of the simply typed λ-calculus) to propositional logic is presented, such that the resulting propositional formula is satisfiable iff the HOL formula has a model of a given finite size. A standard SAT solver can then be used to search for a satisfying assignment, and such an assignment can be transformed back into a model for the HOL formula. The algorithm has been implemented in the interactive theorem prover Isabelle/HOL, where it is used to automatically generate countermodels for non-theorems.     

归纳法推理中若干问题的探讨

归纳法推理是人工智能领域中富有挑战性的研究方向,它是一种难度较大但较有前途的自动定理证明方法。文章对近年来归纳法推理的主要研究成果进行了综述,并分析国内外的研究现状,讨论了归纳法推理研究中的推理效率、理论的不完备性、自动推理机制和构造实用的定理证明器等问题。     

A Proof Environment for Teaching Mathematics

The EPGY Theorem Proving Environment is a computer program used by students to write mathematical proofs in a selection of computer-based, proof-intensive mathematics courses at the high-school and university level. The system allows easy input of mathematical expressions, application of standard proof strategies and logical inference rules, application of mathematical rules, and verification of logical inference. Each course has its own language, database of theorems, and mathematical rules. The system uses a combination of automated reasoning and symbolic computation to verify individual proof steps. The proof environment has been used by over 170 students who have taken the EPGY high-school geometry course. In addition to providing a general overview of the system, we describe what we have learned from student use of the Theorem Proving Environment in the EPGY geometry course.     

基于Isabelle的证明信息系统设计

Isabelle定理证明器中的证明步骤和证明状态是非常具有参考价值的证明信息。然而目前没有工具可以有效管理这些信息。本文给出一个基于Isabelle的信息系统设计方案。利用该系统的实现,用户可以提取、保存和搜索这两种证明信息。     

Compiling a default reasoning system into Prolog

Artificial intelligence researchers have been designing representation systems for default and abductive reasoning. Logic Programming researchers have been working on techniques to improve the efficiency of Horn clause deduction systems This paper describes how one such default and abductive reasoning system (namelyTheorist) can be translated into Horn clauses (with negation as failure), so that we can use the clarity of abductive reasoning systems and the efficiency of Horn clause deduction systems. We thus show how advances in expressive power that artificial intelligence workers are working on can directly utilise advances in efficiency that logic programming researchers are working on. Actual code from a running system is given.     

State-rich model checking

In this paper we survey the area of formal verification techniques, with emphasis on model checking due to its wide acceptance by both academia and industry. The major approaches and their characteristics are presented, together with the main problems faced while trying to apply them. With the increased complexity of systems, as well as interest in software correctness, the demand for more powerful automatic techniques is pushing the theories and tools towards integration. We discuss the state of the art in combining formal methods tools, mainly model checking with theorem proving and abstract interpretation. In particular, we present our own recent contribution on an approach to integrate model checking and theorem proving to handle state-rich systems specified using a combination of Z and CSP.     

Extracting a formally verified, fully executable compiler from a proof assistant

Compilers that have been formally verified in theorem provers are often not directly usable because the formalization language is not a general-purpose programming language or the formalization contains non-executable constructs. This paper takes a comprehensive, even though simplified model of Java, formalized in the Isabelle proof assistant, as starting point and shows how core functions in the translation process (type checking and compilation) are defined and proved correct. From these, Isabelle's program extraction facility generates ML code that can be directly interfaced with other, possibly “unsafe” code.     

A Certifying Code Generation Phase

Guaranteeing correctness of compilation is a vital precondition for correct software. Code generation can be one of the most error-prone tasks in a compiler. One way to achieve trusted compilation is certifying compilation. A certifying compiler generates for each run a proof that it has performed the compilation run correctly. The proof is checked in a separate theorem prover. If the theorem prover is content with the proof one can be sure that the compiler produced correct code. This paper reports on the construction of a certifying code generation phase for a compiler. It is part of a larger project aimed at guaranteeing the correctness of a complete compiler. We emphasize on demonstrating the feasibility of the certifying compilation approach to code generation and focus on the implementation and practical issues. It turns out that the checking of the certificates is the actual bottleneck of certifying compilation. We present a proof schema to overcome this bottleneck. Hence we show the applicability of the certifying compilation approach for small sized programs processed by a compiler's code generation phase.     

Globally linear connection method

To model in a formal system the remarkable ability of human agents to reason about situations, actions, and causality has always been a major research goal in Intellectics. Most of the work towards this goal is based on the situation calculus which, however, has the disadvantage that it requires either to state frame axioms or to use non-monotonic logic and a commonsense law of inertia. A deductive approach which does not show this disadvantage is the linear connection method whose key idea is to treat facts about a situation as resources which can be consumed and produced by actions. It was shown that this approach properly handles planning problems which only allow deterministic actions, i.e. actions which are not allowed to have several alternative effects. In this paper we extend and revise the linear connection method to overcome this restriction. Stefan Brüning, Ph.D.: He received a M. Sc. in Computer Science from the Technical University of Darmstadt in 1992. From 1992 to present he has been a research officer in the Intellectics group at the same university where he received his Ph. D. in 1995. His thesis was entitled “Techniques for Avoiding Redundancy in Theorem Proving Based on the Connection Method”. His current research interests are in the development of efficient calculi for different kinds of deductive tasks, such as deductive planning or default reasoning.     

高可用性系统技术研究

主要从如何减少系统的平均修复时间MTTR和增加系统的平均无故障时间MTTF两方面来提高系统可用性。首先据可信性的定义公式提出提高可信性的措施,如自主运算、面向恢复计算等。最后,深入研究高可用性系统的关键技术,数据存储技术、系统软件技术、进程检查点和迁移技术、故障检测技术、冗余和备份技术。     

Makespan minimization for two parallel machines scheduling with a periodic availability constraint

A two parallel machines scheduling problem where one machine is periodically unavailable with the objective of minimizing makespan is considered. It is showed that the worst-case ratio of the classical LPT algorithm and the competitive ratio of the LS algorithm are 3/2 and 2, respectively, for the offline version and the online version of the problem.     

An approximation scheme for two-machine flowshop scheduling with setup times and an availability constraint

This paper studies the two-machine permutation flowshop scheduling problem with anticipatory setup times and an availability constraint imposed only on the first machine. The objective is to minimize the makespan. Under the assumption that interrupted jobs can resume their operations, we present a polynomial-time approximation scheme for this problem.