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.     

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.     

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.     

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.     

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.     

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可检查的证明.     

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.     

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.     

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.     

An Algorithm for the Exact Numerical Integration of a Special Class of Functions

The classical Gaussian quadrature rules yield very inaccurate results when they are used for the integration of functions of the form f(x)=P(x,\cos(cx+d))\exp(-a^{2}x^{2}+bx) over the infinite interval (-\infty, \infty) , where a\gt 0, b, c, d are real numbers and P is a polynomial. In this paper we propose a new algorithm that computes this type of integrals without error in the machine precision. The algorithm can also be used for the multiple integrals. We give some numerical examples to compare the results obtained by the new algorithm and those obtained by some other methods including the classical Gauss-Hermite integration rules.     

Automatic Theorem Proving and Fuzzy Situational Search for Decisions

The use of automatic theorem proving is considered as a methodological basis of fuzzy situational search for decisions.