As functions which further the state of a proof in automated theorem proving, tactics are an important development in automated deduction. This thesis describes a method to tackle the problem of tactic formation. Tactics must currently be developed by hand, which can be a complicated and time-consuming process. A method is presented for the automatic production of useful tactics. The method presented works on the principle that commonly occurring patterns within proof corpora may have some significance and could therefore be exploited to provide novel tactics. These tactics are discovered using a three step process. Firstly a suitable corpus is chosen and processed. One example of a suitable corpus is that of the Isabelle theorem prover. A number of possible abstractions are presented for this corpus. Secondly, machine learning techniques are used to data-mine each corpus and find sequences of commonly occurring proof steps. The specifics of a proof step are defined by the specified abstraction. The formation of these tactics is completed using evolutionary techniques to combine these patterns into compound tactics. These new tactics are applied using a naive prover as well as undergoing manual evalutation. The tactics show favourable results across a selection of tests, justifying the claim that this project provides a novel method of automatically producing tactics which are both viable and useful.

Thesis (M.A.)--Boston University / PLEASE NOTE: Boston University Libraries did not receive an Authorization To Manage form for this thesis or dissertation. It is therefore not openly accessible, though it may be available by request. If you are the author or principal advisor of this work and would like to request open access for it, please contact us at open-help@bu.edu. Thank you. / As is so often true in history, the importance of an event cannot fully be judged or appreciated unless it is being weighed in light of the prevailing situation of the period. Godel's discovery came at a time when mathematicians generally were looking for a means by which they might fully axiomatize arithmetic, as we have done with geometry. They hoped to be able to find an assvrance that the proof of any arithmetic fact might he proven using only the axioms and rules of inference that had been set up for the system. Those primarily concerned in this endeavor were a group known as the Formalists (since they wished to completely formalize basic mathematics) and David Hilbert. In addition to showing the complete axiomatization of our arithmetic system, they hoped further to exact a proof of the consistency of the axiomatized system [TRUNCATED]. / 2031-01-01

No description available.

Let S be a collection of convex sets in Rd with the property that any subcollection of d − 1 sets has a nonempty intersection. Helly’s Theorem states that ∩s∈S S is nonempty. In a forthcoming paper, Berg et al. (Forthcoming) interpret the one dimensional version of Helly’s Theorem in the context of voting in a society. They look at the effect that different intersection properties have on the proportion of a society that must agree on some point or issue. In general, we define a society as some underlying space X and a collection S of convex sets on the space. A society is (k, m)-agreeable if every m-element subset of S has a k-element subset with a nonempty intersection. The agreement number of a society is the size of the largest subset of S with a nonempty intersection. In my work I focus on the case where X is a tree and the convex sets in S are subtrees. I have developed a reduction method that makes these tree societies more tractable. In particular, I have used this method to show that the agreement number of (2, m)-agreeable tree societies is at least 1 |S | and 3 that the agreement number of (k, k + 1)-agreeable tree societies is at least |S|−1.

No description available.

Thesis (Ph. D.)--University of Oregon, 2006. / Typescript. Includes vita and abstract. Includes bibliographical references (leaf 77). Also available for download via the World Wide Web; free to University of Oregon users.

Academic Thesis--Amsterdam. / Without thesis statement. Bibliography: p. 59-60.

Thesis (M. Sc.)--York University, 1999. Graduate Programme in Computer Science. / Typescript. Includes bibliographical references (leaves 76-77). Also available on the Internet. MODE OF ACCESS via web browser by entering the following URL: http://wwwlib.umi.com/cr/yorku/fullcit?pMQ39193.

This paper investigates whether it is reasonable to bestow credit to one person or group for the famed theorem that relates to the side lengths of any right-angled triangle, a theorem routinely referred to as the “Pythagorean Theorem”. The author investigates the first-documented occurrences of the theorem, along with its first proofs. In addition, proofs that stem from different branches of mathematics and science are analyzed in an effort to display that credit for the development of the theorem should be shared amongst its many contributors rather than crediting the whole of the theorem to one man and his supporters.

No description available.