Spelling suggestions: "subject:"proof theory automatic theorem proving."" "subject:"proof theory 2automatic theorem proving.""
1 |
Transparency in formal proof /Petschulat, Cap. January 2009 (has links)
Thesis (M.S.)--Boise State University, 2009. / Includes abstract. Includes bibliographical references (leaves 52-53).
|
2 |
Transparency in formal proofPetschulat, Cap. January 2009 (has links)
Thesis (M.S.)--Boise State University, 2009. / Title from t.p. of PDF file (viewed June 15, 2010). Includes abstract. Includes bibliographical references (leaves 52-53).
|
3 |
Mechanizing structural inductionAubin, Raymond January 1976 (has links)
This thesis proposes improved methods for the automatic generation of proofs by structural induction in a formal system. The main application considered is proving properties of programs. The theorem-proving problem divides into two parts: (1) a formal system, and (2) proof generating methods. A formal system is presented which allows for a typed language; thus, abstract data types can be naturally defined in it. Its main feature is a general structural induction rule using a lexicographic ordering based on the substructure ordering induced by type definitions. The proof generating system is carefully introduced in order to convince of its consistency. It is meant to bring solutions to three problems. Firstly, it offers a method for generalizing only certain occurrences of a term in a theorem; this is achieved by associating generalization with the selection of induction variables. Secondly, it treats another generalization problem: that of terms occurring in the positions of arguments which vary within function definitions, besides recursion controlling arguments. The method is called indirect generalization, since it uses specialization as a means of attaining generalization. Thirdly, it presents a sound strategy for using the general induction rule which takes into account all induction subgoals, and for each of them, all induction hypotheses. Only then are the hypotheses retained and instantiated, or rejected altogether, according to their potential usefulness. The system also includes a search mechanism for counter-examples to conjectures, and a fast simplification algorithm.
|
4 |
Length of proofs and unification theoryFarmer, William Michael. January 1900 (has links)
Thesis (Ph. D.)--University of Wisconsin--Madison, 1984. / Typescript. Vita. eContent provider-neutral record in process. Description based on print version record. Includes bibliographical references (leaves 224-228).
|
Page generated in 0.4887 seconds