Proof assistants, such as Isabelle HOL, offer tools to facilitate inductive theorem proving. Isabelle experts know how to use these tools effectively; however they did not have a systematic way to encode their expertise. To address this problem, we present our domain-specific language, LiFtEr. LiFtEr allows experienced Isabelle users to encode their induction heuristics in a style independent of any problem domain. LiFtEr's interpreter mechanically checks if a given application of induction tool matches the heuristics, thus transferring experienced users' expertise to new Isabelle users.
Taking the same approach as , Nagashima attempted to build a recommendation tool, @cite_7 , to automatically suggest promising arguments for the |induct| method without completing a proof: they wrote many assertions in Isabelle ML. Unfortunately, encoding induction heuristics as assertions directly in Isabelle ML caused an immense amount of code-clutter, and they could not encode even the notion of depth in syntax tree due to the problem discussed in Section . Therefore, we developed , expecting that serves as a l anguage for f eature e xtraction.
@cite_7
1571434026 2905394895 2135625884 1819951499
Isabelle, which is available from http: isabelle.in.tum.de , is a generic framework for interactive theorem proving. The Isabelle Puremeta-logic allows the formalization of the syntax and inference rules of a broad range of object-logics following the general idea of natural deduction [32,33]. The logical core is implemented according to the well-known "LCF approach" of secure inferences as abstract datatype constructors in ML [16]; explicit proof terms are also available [8]. Isabelle Isarprovides sophisticated extra-logical infrastructure supporting structured proofs and specifications, including concepts for modular theory development. Isabelle HOLis a large application within the generic framework, with plenty of logic-specific add-on tools and a large theory library. Other notable object-logics are Isabelle ZF(Zermelo-Fraenkel set-theory, see [34,36] and Isabelle HOLCF[26] (Scott's domain theory within HOL). Users can build further formal-methods tools on top, e.g. see [53]. Mathematical induction lies at the heart of mathematics and computer science. However, automated theorem proving of inductive problems is still limited in its power. In this abstract, we first summarize our progress in automating inductive theorem proving for Isabelle HOL. Then, we present MiLkMaId, our approach to suggesting promising applications of mathematical induction without completing a proof search. 1. Summary In Part I, four ostensibly different theoretical models of induction are presented, in which the problem dealt with is the extrapolation of a very long sequence of symbols—presumably containing all of the information to be used in the induction. Almost all, if not all problems in induction can be put in this form. Some strong heuristic arguments have been obtained for the equivalence of the last three models. One of these models is equivalent to a Bayes formulation, in which a priori probabilities are assigned to sequences of symbols on the basis of the lengths of inputs to a universal Turing machine that are required to produce the sequence of interest as output. Though it seems likely, it is not certain whether the first of the four models is equivalent to the other three. Few rigorous results are presented. Informal investigations are made of the properties of these models. There are discussions of their consistency and meaningfulness, of their degree of independence of the exact nature of the Turing machine used, and of the accuracy of their predictions in comparison to those of other induction methods. In Part II these models are applied to the solution of three problems—prediction of the Bernoulli sequence, extrapolation of a certain kind of Markov chain, and the use of phrase structure grammars for induction. Though some approximations are used, the first of these problems is treated most rigorously. The result is Laplace's rule of succession. The solution to the second problem uses less certain approximations, but the properties of the solution that are discussed, are fairly independent of these approximations. The third application, using phrase structure grammars, is least exact of the three. First a formal solution is presented. Though it appears to have certain deficiencies, it is hoped that presentation of this admittedly inadequate model will suggest acceptable improvements in it. This formal solution is then applied in an approximate way to the determination of the “optimum” phrase structure grammar for a given set of strings. The results that are obtained are plausible, but subject to the uncertainties of the approximation used. A generic tableau prover has been implemented and integrated with Isabelle (Paulson, 1994). Compared with classical first-order logic provers, it has numerous extensions that allow it to reason with any supplied set of tableau rules. It has a higherorder syntax in order to support user-defined binding operators, such as those of set theory. The unification algorithm is first-order instead of higher-order, but it includes modifications to handle bound variables. The proof, when found, is returned to Isabelle as a list of tactics. Because Isabelle verifies the proof, the prover can cut corners for efficiency’s sake without compromising soundness. For example, the prover can use type information to guide the search without storing type information in full. Categories: F.4, I.1