Data Compression for Proof Replay

We describe a compressing translation from SAT solver generated propositional resolution refutation proofs to classical natural deduction proofs. The resulting proof can usually be checked quicker than one that simply simulates the original resolution proof. We use this result in interactive theorem provers, to speed up reconstruction of SAT solver generated proofs. The translation is fast and scales up to large proofs with millions of inferences.     

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.     

SMELS: Satisfiability Modulo Equality with Lazy Superposition

We consider the problem of checking satisfiability of quantified formulae in First Order Logic with Equality. We propose a new procedure for combining SAT solvers with Superposition Theorem Provers to handle quantified formulae in an efficient and complete way. In our procedure, the input formula is converted into CNF as in traditional first order logic theorem provers. The ground clauses are given to the SAT solver, which runs a DPLL method to build partial models. The partial model is reduced, and then passed to a Superposition procedure, along with justifications of literals. The Superposition procedure then performs an inference rule, which we call Justified Superposition, between the ground literals and the nonground clauses, plus usual Superposition rules with the nonground clauses. Any resulting ground clauses are provided to the DPLL engine. We prove the completeness of our procedure, using a nontrivial modification of the Bachmair and Ganzinger’s model generation technique. We have implemented a theorem prover based on this idea by reusing state-of-the-art SAT solver and Superposition Theorem Prover. Our theorem prover inherits the best of both worlds: a SAT solver to handle ground clauses efficiently, and a Superposition theorem prover which uses powerful orderings to handle the nonground clauses. Experimental results are promising, and hereby confirm the viability of our method.     

Predicate Abstraction of ANSI-C Programs Using SAT

Predicate abstraction is a major method for verification of software. However, the generation of the abstract Boolean program from the set of predicates and the original program suffers from an exponential number of theorem prover calls as well as from soundness issues. This paper presents a novel technique that uses an efficient SAT solver for generating the abstract transition relations of ANSI-C programs. The SAT-based approach computes a more precise and safe abstraction compared to existing predicate abstraction techniques.     

Optimization techniques for propositional intuitionistic logic and their implementation

This paper presents some techniques which bound the proof search space in propositional intuitionistic logic. These techniques are justified by Kripke semantics and are the backbone of a tableau based theorem prover (PITP) implemented in C++. PITP and some known theorem provers are compared using the formulas of ILTP benchmark library. It turns out that PITP is, at the moment, the propositional prover that solves most formulas of the library.     

Automated proofs of equality problems in Overbeek's competition

This paper reports the detailed computer proofs of nine equality problems in Overbeek's competition obtained by Herky, a completion-based theorem prover developed by the author. Advanced techniques implemented in Herky made it a high-performance theorem prover for equational reasoning. Herky is able to prove the first nine of the ten equality problems in the competition (the tenth is an open problem). These equality problems are likely to serve as good exercises for theorem provers based on different approaches, and the proofs of these problems may help people to solve them using their own theorem provers.     

针对教学场景的ZFC集合论Coq形式化

离散数学是计算机类专业的基础课程之一,命题逻辑、一阶逻辑与公理集合论是其重要组成部分.教学实践表明,初学者准确理解语法、语义、推理系统等抽象概念是有一定难度的.近年来,已有一些学者开始在教学中引入交互式定理证明工具,以帮助学生构造形式化证明,更透彻地理解逻辑系统.然而,现有的定理证明器有较高上手门槛,直接使用会增加学生的学习负担.鉴于此,在Coq中开发了针对教学场景的ZFC公理集合论证明器.首先,形式化了一阶逻辑推理系统和ZFC公理集合论;之后,开发了数条自动化推理规则证明策略.学生可以在与教科书风格相同的简洁证明环境中使用自动化证明策略完成定理的形式化证明.该工具被用在了大一新生离散数学课程的教学中,没有定理证明经验的学生使用该工具可以快速完成数学归纳法和皮亚诺算术系统等定理的形式化证明,验证了该工具的实际效果.     

A theorem prover for verifying iterative programs over integers

An implementation of a rule-based theorem prover for verifying iterative programs over integers is presented. The authors emphasize the overall proof construction strategy of the prover which has been able to construct the correctness proofs of all iterative programs taken from the literature. Two performance measures for the prover are proposed, and its proof construction for an array-sorting program is evaluated using these measures     

An experiment with the Boyer-Moore theorem prover: A proof of Wilson's theorem

This paper describes the use of the Boyer-Moore theorem prover in mechanically generating a proof of Wilson's theorem: for any prime p, (p-1)! and p-1 are congruent modulo p. The input to the theorem prover consists of a sequence of three function definitions and forty-two propositions to be proved. The proofs generated by the system are based on a library of lemmas relating to list manipulation and number theory, including Fermat's theorem.     

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.     

Analytica – An Experiment in Combining Theorem Proving and Symbolic Computation

Analytica is an automatic theorem prover for theorems in elementary analysis. The prover is written in the Mathematica language and runs in the Mathematica environment. The goal of the project is to use a powerful symbolic computation system to prove theorems that are beyond the scope of previous automatic theorem provers. The theorem prover is also able to deduce the correctness of certain simplification steps that would otherwise not be performed. We describe the structure of Analytica and explain the main techniques that it uses to construct proofs. Analytica has been able to prove several nontrivial theorems. In this paper, we show how it can prove a series of lemmas that lead to the Bernstein approximation theorem.     

Coq Formalization of ZFC Set Theory for Teaching Scenarios

Discrete mathematics is a foundation course for computer-related majors, and propositional logic, first-order logic, and the axiomatic set theory are important parts of this course. Teaching practice shows that beginners find it difficult to accurately understand abstract concepts, such as syntax, semantics, and reasoning system. In recent years, some scholars have begun introducing interactive theorem provers into teaching to help students construct formal proofs so that they can understand logic systems more thoroughly. However, directly employing the existing theorem provers will increase students'' learning burden since these tools have a high threshold for getting started with them. To address this problem, we develop a prover for the Zermelo-Fraenkel set theory with the axiom of Choice (ZFC) in Coq for teaching scenarios. Specifically, the first-order logical reasoning system and the axiomatic set theory ZFC are formalized, and several automated proof tactics specific to reasoning rules are then developed. Students can utilize these automated proof tactics to construct formal proofs of theorems in a textbook-style concise proving environment. This tool has been introduced into the teaching of the course of discrete mathematics for freshmen. Students with no prior theorem-proving experience can quickly construct formal proofs of theorems including mathematical induction and Peano arithmetic with this tool, which verifies the practical effectiveness of this tool.     

Towards mechanical metamathematics

Metamathematics is a source of many interesting theorems and difficult proofs. This paper reports the results of an experiment to use the Boyer-Moore theorem prover to proof-check theorems in metamathematics. We describe a First Order Logic due to Shoenfield and outline some of the theorems that the prover was able to prove about this logic. These include the tautology theorem which states that every tautology has a proof. Such proofs can be used to add new proof procedures to a proof-checking program in a sound and efficient manner.     

Frame rule for mutually recursive procedures manipulating pointers

Using a predicate transformer semantics of programs, we introduce statements for heap operations and separation logic operators for specifying programs that manipulate pointers. We prove a powerful Hoare total correctness rule for mutually recursive procedures manipulating pointers. The rule combines earlier proof rules for (mutually) recursive procedures with the frame rule for pointer programs. The theory, including the proofs, is implemented in the theorem prover PVS. In this implementation program variables and addresses can store values of almost any type of the theorem prover.     

Limitations of restricted branching in clause learning

The techniques for making decisions, that is, branching, play a central role in complete methods for solving structured instances of constraint satisfaction problems (CSPs). In this work we consider branching heuristics in the context of propositional satisfiability (SAT), where CSPs are expressed as propositional formulas. In practice, there are cases when SAT solvers based on the Davis-Putnam-Logemann-Loveland procedure (DPLL) benefit from limiting the set of variables the solver is allowed to branch on to so called input variables which provide a strong unit propagation backdoor set to any SAT instance. Theoretically, however, restricting branching to input variables implies a super-polynomial increase in the length of the optimal proofs for DPLL (without clause learning), and thus input-restricted DPLL cannot polynomially simulate DPLL. In this paper we settle the case of DPLL with clause learning. Surprisingly, even with unlimited restarts, input-restricted clause learning DPLL cannot simulate DPLL (even without clause learning). The opposite also holds, and hence DPLL and input-restricted clause learning DPLL are polynomially incomparable. Additionally, we analyze the effect of input-restricted branching on clause learning solvers in practice with various structured real-world benchmarks. This is an extended version of a paper [27] presented at the 13th International Conference on Principles and Practice of Constraint Programming (CP 2007) in Providence, RI, USA. The first author gratefully acknowledges financial support from Helsinki Graduate School in Computer Science and Engineering, Academy of Finland (grants #211025 and #122399), Emil Aaltonen Foundation, Jenny and Antti Wihuri Foundation, Finnish Foundation for Technology Promotion TES, and Nokia Foundation. The second author gratefully acknowledges the financial support from Academy of Finland (grant #112016).     

Proving Ramsey's theorem by the cover set induction: A case and comparison study

An experiment of the cover set induction method inRRL is presented with a mechanical proof of Ramsey's theorem in graph theory. The proof is similar to the proof obtained by Kaufmann using the Boyer-Moore theorem prover. We show that this similarity is not unusual, because there is a close relationship between the Boyer-Moore logic and the algebraic specification of abstract data types on which the cover set induction method is based. (This implies that many proofs done by the Boyer-Moore theorem prover can be reproduced byRRL.) Our experiment shows thatRRL can automatically prove all the lemmas in Ramsey's theorem, while the Boyer-Moore theorem prover needs several user's hints and takes much longer (CPU time) to finish.Partially supported by National Science Foundation Grants Nos. CCR-9202838 and INT-9016100.     

Computer proofs in Group Theory

This paper reports the results of an experiment in using the Boyer-Moore Theorem Prover in seeking computer-checked proofs in Group Theory. Starting from the axioms for groups and elementary list and number theory, the theorem prover was led to the proofs of two basic theorems in Elementary Group Theory by a sequence of lemmas suggested by the author. The computer proofs illustrate the effective use of the Boyer-Moore Theorem Prover in Group Theory.     

Verifying the SRT Division Algorithm Using Theorem Proving Techniques

We verify the correctness of an SRT division circuit similar to the one in the Intel Pentium processor. The circuit and its correctness conditions are formalized as a set of algebraic relations on the real numbers. The main obstacle to applying theorem proving techniques for hardware verification is the need for detailed user guidance of proofs. We overcome the need for detailed proof guidance in this example by using a powerful theorem prover called Analytica. Analytica uses symbolic algebra techniques to carry out the proofs in this paper with much less guidance than existing general purpose theorem provers require for algebraic reasoning.