Rule-based induction

Induction is indispensable for reasoning about parameterized logical models, as they arise in the context of hardware and software verification. Sophisticated heuristics for mechanizing induction proofs exist and have been successfully implemented in theorem provers for first-order logic. This article is a presentation of a complementary induction method that makes extensive use of the expressiveness of higher-order logic and higher-order unification facilities ofLAMBDA. Rather than hard-coded routines, rules are used that incarnate induction schemes in a concise way. By means of instantiatable meta-variables, these rules are more general and preserve the flexibility to gradually specify an induction scheme throughout a proof process, as more and more information is available, rather than fully determining the induction scheme right at the beginning. Safe inference mechanisms and general-purpose proof automation utilities in the proof checkerLAMBDA are well-suited for an interactive induction assistant that integrates automatic induction heuristics and at they same time accepts human guidance.     

Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures

Recently Lee and Plaisted proposed a theorem-proving method, the hyperlinking proof procedure, to eliminate duplication of instances of clauses during the process of inference. A theorem prover, CLIN, which implements the procedure was also constructed. In this implementation, redundant work on literal unification checking, partial unification checking, and duplicate instance checking is performed repetitively, resulting in a large overhead when many rounds of hyperlinking are needed for an input problem. We propose a technique that maintains information across rounds in shared network structures, so that the redundant work in each hyperlinking round can be avoided. Empirical performance comparison has been done between CLIN and CLIN-net, which is the theorem prover with shared network structures, and some results are shown. Problems related to memory overhead and literal ordering are discussed.Supported by National Science Council under grants NSC 81-0408-E-110-509 and NSC-82-0408-E-110-045. A preliminary version of this paper appeared in Proceedings of International Conference on Computing and Information (Sudbury, Ontario Canada, May 1993).     

证明开发环境中的元语言设计

本文通过对数型赋予操作解释，将ＬＦ的逻辑定义风格的λＰｒｏｌｏｇ的逻辑程序设计风格融于一体，提出了旨在对定理证明过程进行元级编程的元语言ＴＭＬ及其抽象解释器，然后，利用项推理过程给出了ＴＭＬ元程序的正确性检查算法。     

Substitutions into propositional tautologies

We prove that there is a polynomial time substitution (y₁,…,yn):=g(x₁,…,xk) with k?n such that whenever the substitution instance A(g(x₁,…,xk)) of a 3DNF formula A(y₁,…,yn) has a short resolution proof it follows that A(y₁,…,yn) is a tautology. The qualification “short” depends on the parameters k and n.     

Resolution theorem proving in reified modal logics

This paper is concerned with the application of the resolution theorem proving method to reified logics. The logical systems treated include the branching temporal logics and logics of belief based on K and its extensions. Two important problems concerning the application of the resolution rule to reified systems are identified. The first is the redundancy in the representation of truth functional relationships and the second is the axiomatic reasoning about modal structure. Both cause an unnecessary expansion in the search space. We present solutions to both problems which allow the axioms defining the reified logic to be eliminated from the database during theorem proving hence reducing the search space while retaining completeness. We describe three theorem proving methods which embody our solutions and support our analysis with empirical results.Much of the research reported in this paper was supported by DTI IED SERC grant No. GR/F 35968, and was carried out whilst Han Reichgelt was at the University of Nottingham.     

Accelerating tableaux proofs using compact representations

In this article a modified form of tableau calculus, calledTableau Graph Calculus, is presented for overcoming the well-known inefficiencies of the traditional tableau calculus to a large extent. This calculus is based on a compact representation of analytic tableaux by using graph structures calledtableau graphs. These graphs are obtained from the input formula in linear time and incorporate most of the rule applications of normal tableau calculus during the conversion process. The size of this representation is linear with respect to the length of the input formula and the graph closely resembles the proof tree of tableau calculi thus retaining the naturalness of the proof procedure. As a result of this preprocessing step, tableau graph calculus has only a single rule which is repeatedly applied to obtain a proof. Many optimizations for the applications of this rule, to effectively prune the search space, are presented as well. Brief details of an implemented prover called FAUST, embedded within the higher-order theorem prover called HOL, are also given. Applications of FAUST within a hardware verification context are also sketched.This work has been partly financed by german national grant under the project Automated System Design, SFB No. 358.     

A Compared Study of Two Correctness Proofs for the Standardized Algorithm of ABR Conformance

The ABR conformance protocol is a real-time program that controls dataflow rates on ATM networks. A crucial part of this protocol is the dynamical computation of the expected rate of data cells. We present here a modelling of the corresponding program with its environment, using the notion of (parametric) timed automata. A fundamental property of the service provided by the protocol to the user is expressed in this framework and proved by two different methods. The first proof relies on inductive invariants, and was originally verified using theorem-proving assistant COQ. The second proof is based on reachability analysis, and was obtained using model-checker HYTECH. We explain and compare these two proofs in the unified framework of timed automata.     

Middle-out reasoning for synthesis and induction

We develop two applications of middle-out reasoning in inductive proofs: logic program synthesis and the selection of induction schemes. Middle-out reasoning as part of proof planning was first suggested by Bundy et al. Middle-out reasoning uses variables to represent unknown terms and formulae. Unification instantiates the variables in the subsequent planning, while proof planning provides the necessary search control. Middle-out reasoning is used for synthesis by planning the verification of an unknown logic program: The program body is represented with a meta-variable. The planning results both in an instantiation of the program body and a plan for the verification of that program. If the plan executes successfully, the synthesized program is partially correct and complete. Middle-out reasoning is also used to select induction schemes. Finding an appropriate induction scheme during synthesis is difficult because the recursion of the program, which is unknown at the outset, determines the induction in the proof. In middle-out induction, we set up a schematic step case by representing the constructors that are applied to induction variables with meta-variables. Once the step case is complete, the instantiated variables correspond to an induction appropriate to the recursion of the program. We have implemented these techniques as an extension of the proof planning system CL ^A M, called Periwinkle, and synthesized a variaety of programs fully automatically. Supported by the Swiss National Science Foundation and ARC Project BC/DAAD Grant 438. The work described in this paper was carried out while the first author was at the Department of Artificial Intelligence of the University of Edinburgh. Supported by the German Ministry for Research and Technology (BMFT) under grant ITS 9102 and ARC Project BC/DAAD Grant 438. Responsibility for the contents of this publication lies with the authors. Supported by SERC grant GR/J/80702, ESPRIT BRP grant 6810, ESPRIT BRP grant EC-US 019-76094, and ARC Project BC/DAAD Grant 438.     

The Propositional Formula Checker HeerHugo

HeerHugo is a propositional formula checker that determines whether a given formula is satisfiable or not. The underlying algorithm is based on a specific breadth-first search procedure, with several enhancements including unit resolution and 2-satisfiability tests. Its main ingredient is the branch/merge rule inspired by an algorithm proposed by Stållmarck, which is protected by a software patent. In this paper, the main elements of the algorithm are discussed, and its remarkable effectiveness is illustrated with some examples and computational results.     

Hierarchical deduction

This paper describes an hierarchical deduction proof procedure. This procedure proves a theorem by searching for a proof acceptable to an hierarchical deduction structire; those derivations which are irrelevant to this proof are limited by means of a set of completeness-preserving refinements of the basic procedure, such as constraints on framed literals and on common tails, a proper reduction refinement, a global subsumption constraint, and a level subgoal reordering refinement, etc. In addition to this basic algorithm, we will present a partial set of support strategy and a semantically guided hierarchical deduction for the incorporation of semantics and human factors. The paper concludes with proofs concerning the completeness of the basic algorithm and the results of a computer implementation applied to some nontrivial problems.This work was supported in part by NSF grant MCS-8313499.     

Constructing the real numbers in HOL

This paper describes a construction of the real numbers in the HOL theorem-prover by strictly definitional means using a version of Dedekind's method. It also outlines the theory of mathematical analysis that has been built on top of it and discusses current and potential applications in verification and computer algebra.     

Short proofs of the pigeonhole formulas based on the connection method

Quadratic proofs of pigeonhole formulas are presented using connection method proof techniques. The interest of this result derives from the fact that for this class of formulas exponential lower bounds are known for the length of resolution refutations.     

重写对策在基于HOL的形式化证明中的应用

讨论了重写对策在基于高阶逻辑定理证明系统HOL的形式化证明过程中的应用.通过REWRITE_ TAC对策、ASM_ REWRITE_ TAC对策和RW_ TAC对策,详细分析了重写对策的功能、应用方法、应用环境、应用中可能出现的问题以及解决办法,给出了DB.match搜索和DB.find搜索等重写对策的定理参数的选择方法,并进行了分析与比较.进一步说明了重写对策在基于HOL系统的形式化证明中的重要性,以期对HOL系统用户提供一些帮助与启发,促进HOL系统的进一步发展与完善,使形式化方法能够解决更多的实际问题.     

The HOL logic extended with quantification over type variables

The HOL system is an LCF-style mechanized proof assistant for conducting proofs in higher-order logic. This paper discusses a proposal to extend the primitive basis of the logic underlying the HOL system with a very simple form of quantification over types. It is shown how certain practical problems with using the definitional mechanisms of HOL would be solved by the additional expressive power gained by making this extension.     

Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite

This paper is a case study in combining theorem provers. We define a derived rule in HOL-Light, CVC_PROVE, which calls CVC Lite and translates the resulting proof object back to HOL-Light. As a result, we obtain a highly trusted proof-checker for CVC Lite, while also fundamentally expanding the capabilities of HOL-Light.     

Set theory in first-order logic: Clauses for Gödel's axioms

In this paper we present a set of clauses for set theory, thus developing a foundation for the expression of most theorems of mathematics in a form acceptable to a resolution-based automated theoren prover. Because Gödel's formulation of set theory permits presentation in a finite number of first-orde formulas, we employ it rather than that of Zermelo-Fraenkel. We illustrate the expressive power of thi formulation by providing statements of some well-known open questions in number theory, and give some intuition about how the axioms are used by including some sample proofs. A small set of challeng problems is also given.