用于指针逻辑的自动定理证明器

提出了一种为指针逻辑设计定理证明器的新技术,该项技术主要是基于变换和替代,已在APL 的工具中得以实现.APL 自动定理证明器是完全自动的,且其产生的证明可以被有效地记录和检验.已使用关于单链表、双链表和二叉树的指针程序测试了该自动定理证明器.     

The Watson Theorem Prover

Watson is a general-purpose system for formal reasoning. It is an interactive equational higher-order theorem prover. The higher-order logic supported by the prover is distinctive in being type free (it is a safe variant of Quine's NF). Watson allows the development of automated proof strategies, which are represented and stored by the prover in the same way as theorems. The mathematical foundations of the prover and the way these are presented to a user are discussed. The paper also contains discussions of experiences with the prover and relations of the prover to other systems.     

An extension of the Boyer-Moore Theorem Prover to support first-order quantification

We describe an implementation of an extension to the Boyer-Moore Theorem Prover and logic that allows first-order quantification. The extension retains the capabilities of the Boyer-Moore system while allowing the increased flexibility in specification and proof that is provided by quantifiers. The idea is to Skolemize in an appropriate manner. We demonstrate the power of this approach by describing three successful proof-checking experiments using the system, each of which involves a theorem of set theory as translated into a first-order logic. We also demonstrate the soundness of our approach.This research was supported in part by ONR Contract N00014-88-C-0454. The views and conclusions contained in this document are those of the author and should not be interpreted as representing the official policies, either expressed or implied, of Computational Logic, Inc., the Office of Naval Research or the U.S. Government.     

支持索引式的PPTL定理证明器的实现

定理证明是目前主流的形式化验证方法,拥有强大的抽象和逻辑表达能力,且不存在状态空间爆炸问题,可用于有穷和无穷状态系统,但其不能完全自动化,并且要求用户掌握较强的数学知识.含索引式的命题投影时序逻辑(PPTL)是一种具有完全正则表达能力,并且包含LTL的时序逻辑,具有较强的建模和性质描述能力.目前,一个可靠完备的含索引式的PPTL公理系统已被构建,然而基于该公理系统的定理证明尚未得到良好工具的支持,存在证明自动化程度较低以及证明冗长易错的问题.鉴于此,首先设计了支持索引式的PPTL定理证明器的实现框架,包括公理系统的形式化与交互式定理证明;然后,在Coq中形式化定义了含索引式的PPTL公式、公理与推理规则,完成了框架中公理系统的实现;最后,通过两个实例的交互式证明验证了该定理证明器的可用性.     

GRAMY: A Geometry Theorem Prover Capable of Construction

This study investigates a procedure for proving arithmetic-free Euclidean geometry theorems that involve construction. Construction means drawing additional geometric elements in the problem figure. Some geometry theorems require construction as a part of the proof. The basic idea of our construction procedure is to add only elements required for applying a postulate that has a consequence that unifies with a goal to be proven. In other words, construction is made only if it supports backward application of a postulate. Our major finding is that our proof procedure is semi-complete and useful in practice. In particular, an empirical evaluation showed that our theorem prover, GRAMY, solves all arithmetic-free construction problems from a sample of school textbooks and 86% of the arithmetic-free construction problems solved by preceding studies of automated geometry theorem proving.     

An Interval Algorithm for Bounding the Ranges of Real-Valued Functions of One Real Variable

An interval algorithm FRANGE which determines computationally rigorous bounds on the ranges of functions f : R1 R1 [a, b] c R1 with prescribed over-estimation is described. It is assumed that f C2(D) where D c R1 is an open interval containing [a, b]. The algorithm FRANGE is based on an algorithm due to Rall and offers a choice of four selections of function, derivative and slope evaluations. Numerical results from a Fortran 90 implementation of FRANGE are presented.     

RRTP - A Replacement Rule Theorem Prover

The Replacement Rule Theorem Prover (RRTP) is an instance-based, refutational, first-order clausal theorem prover. The prover is motivated by the idea of selectively replacing predicates by their definitions, and operates by selecting relevant instances of the input clauses. The relevant instances are grounded, if necessary, and tested for unsatisfiability by using a fast propositional calculus decision procedure.     

Theorem Prover for Intuitionistic Logic Based on the Inverse Method

The first-order intuitionistic logic is a formal theory from the family of constructive logics. In intuitionistic logic, it is possible to extract a particular example x = a and a proof of a formula P(a) from a proof of a formula ?xP(x). Owing to this feature, intuitionistic logic has many applications in mathematics and computer science. Many modern proof assistants include automated tactics for the first-order intuitionistic logic, which simplify the task of solving challenging problems, such as formal verification of software, hardware, and protocols. In this paper, a new theorem prover (called WhaleProver) for full first-order intuitionistic logic is presented. Testing on the ILTP benchmarking library has shown that WhaleProver performance is comparable with the state-of-the-art intuitionistic provers. Our prover has solved more than 800 problems from the ILTP version 1.1.2. Some of them are intractable for other provers. WhaleProver is based on the inverse method proposed by S.Yu. Maslov. We introduce an intuitionistic inverse method calculus which is, in turn, a special kind of sequent calculus. It is also described how to adopt for this calculus several existing proof search strategies proposed for different logical calculi by S.Yu. Maslov, V.P. Orevkov, A.A. Voronkov, and others. In addition, a new proof search strategy is proposed that allows one to avoid redundant inferences. The paper includes results of experiments with WhaleProver on the ILTP library. We believe that Whale- Prover can be used as a test bench for different inference procedures and strategies, as well as for educational purposes.     

CLIN-S - A Semantically Guided First-Order Theorem Prover

CLIN-S is an instance-based, clause-form first-order theorem prover. CLIN-S employs three inference procedures: semantic hyper-linking, which uses semantics to guide the proof search and performs well on non-Horn parts of the proofs involving small literals, rough resolution, which removes large literals in the proofs, and UR resolution, which proves the Horn parts of the proofs. A semantic structure for the input clauses is given as input. During the search for the proof, ground instances of the input clauses are generated and new semantic structures are built based on the input semantics and a model of the ground clause set. A proof is found if the ground clause set is unsatisfiable. In this article, we describe the system architecture and major inference rules used in CLIN-S.     

Social and Semiotic Analyses for Theorem Prover User Interface Design 1

We describe an approach to user interface design based on ideas from social science, narratology (the theory of stories), cognitive science, and a new area called algebraic semiotics. Social analysis helps to identify certain roles for users with their associated requirements, and suggests ways to make proofs more understandable, while algebraic semiotics, which combines semiotics with algebraic specification, provides rigorous theories for interface functionality and for a certain technical notion of quality. We apply these techniques to designing user interfaces for a distributed cooperative theorem proving system, whose main component is a website generation and proof assistance tool called Kumo. This interface integrates formal proving, proof browsing, animation, informal explanation, and online background tutorials, drawing on a richer than usual notion of proof. Experience with using the interface is reported, and some conclusions are drawn. Received November 1998 / Accepted in revised form June 1999     

Integrating a SAT Solver with an LCF-style Theorem Prover

This paper describes the integration of a leading SAT solver with Isabelle/HOL, a popular interactive theorem prover. The SAT solver generates resolution-style proofs for (instances of) propositional tautologies. These proofs are verified by the theorem prover. The presented approach significantly improves Isabelle's performance on propositional problems, and furthermore exhibits counterexamples for unprovable conjectures.     

出具证明编译器中线性整数命题证明的自动生成

近年来,出具证明编译器作为构建高可信软件的重要途径,逐渐成为编译器理论和形式化验证的研究热点.在其理论框架中,编译器需要借助自动定理证明技术,自动地证明验证条件并生成机器可检查的证明项,因此好的自动定理证明器对出具证明编译器至关重要.本文基于Simplex算法在出具证明编译器的框架内设计并实现了一个支持线性整数命题求解的自动定理证明器,并且提出一套证明项构造方法,将其应用于自动定理证明器中可生成Coq可检查的证明.     

一个用于指针程序验证的自动定理证明器的设计与实现

对高可信软件需求的增加使得指针程序的验证成为近期的研究热点.指针逻辑作为Hoare逻辑的扩展,可以对指针程序进行精确的分析.介绍一个针对指针逻辑的自动定理证明器的设计和实现,描述了一些算法.实验结果表明,该定理证明器可以完全自动的证明用类C语言编写的关于单链表,双链表和二叉树的指针程序的验证条件,并生成机器可检查的证明.     

Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover

This paper is a report about the use of Matita, an interactive theorem prover under development at the University of Bologna, for the solution of the POPLmark Challenge, part 1a. We provide three different formalizations, including two direct solutions using pure de Bruijn and locally nameless encodings of bound variables, and a formalization using named variables, obtained by means of a sound translation to the locally nameless encoding. According to this experience, we also discuss some of the proof principles used in our solutions, which have led to the development of a generalized inversion tactic for Matita.     

Can Finite Samples Detect Singularities of Real-Valued Functions?

Commonly, in learning theory, the task of the learner is to identify an unknown target object. We consider a variant of this basic task in which the learner is required only to decide whether the unknown target has a certain property. We allow an infinite learning process in which the learner is required to eventually arrive at the correct answer. We say that a problem for which such a learning algorithm exists is Decidable In the Limit (DIL). We analyze the class of DIL problems and provide a necessary and sufficient condition for the membership of a decision problem in this class. We offer an algorithm for any DIL problem, and apply it to several types of learning tasks. We introduce an extension of the usual Inductive Inference learning model—Inductive Inference with a Cheating Teacher. In this model the teacher may choose to present to the learner, not only a language belonging to the agreed-upon family of languages, but also an arbitrary language outside this family. In such a case we require that the learner will be able to eventually detect the faulty choice made by the teacher. We show that such a strong type of learning is possible, and there exist learning algorithms that will fail only on arbitrarily small sets of faulty languages. Furthermore, if an a priori probability distribution P , according to which f is being chosen, is available to the algorithm, then it can be strengthened into a finite algorithm. More precisely, for many distributions P , there exists a polynomial function, l , such that, for every 0 < δ < 1 , there is an algorithm using at most l(log(δ)) many probes that succeeds on more than (1-δ) of the f 's (as measured by P ). We believe that the new approach presented here will be found useful for many further applications. Received February 14, 1997; revised July 6, 1997, and July 18, 1997.     

A New Algebraic Tool for Automatic Theorem Provers

The concepts of implicates and implicants are widely used in several fields of Automated Reasoning. Particularly, our research group has developed several techniques that allow us to reduce efficiently the size of the input, and therefore the complexity of the problem. These techniques are based on obtaining and using implicit information that is collected in terms of unitary implicates and implicants. Thus, we require efficient algorithms to calculate them. In classical propositional logic it is easy to obtain efficient algorithms to calculate the set of unitary implicants and implicates of a formula. In temporal logics, contrary to what we see in classical propositional logic, these sets may contain infinitely many members. Thus, in order to calculate them in an efficient way, we have to base the calculation on the theoretical study of how these sets behave. Such a study reveals the need to make a generalization of Lattice Theory, which is very important in Computational Algebra. In this paper we introduce the multisemilattice structure as a generalization of the semilattice structure. Such a structure is proposed as a particular type of poset. Subsequently, we offer an equivalent algebraic characterization based on non-deterministic operators and with a weakly associative property. We also show that from the structure of multisemilattice we can obtain an algebraic characterization of the multilattice structure. This paper concludes by showing the relevance of the multisemilattice structure in the design of algorithms aimed at calculating unitary implicates and implicants in temporal logics. Concretely, we show that it is possible to design efficient algorithms to calculate the unitary implicants/implicates only if the unitary formulae set has the multisemilattice structure.