No description available.

Automated reasoning, and in particular automated theorem proving, has become a very important research field within the world of mathematics. Besides being used to verify proofs of theorems, it has also been used to discover proofs of theorems which were previously open problems. In this thesis, an automated reasoning assistant based on Godel's class theory is used to deduce several theorems.

This thesis was motivated by a case study involving the formalisation of arguments that simplify the verification of tree-oriented multicast protocols. As well as covering the case study itself, it discusses our solution to problems we encountered concerning expressivity and automation. The expressivity problems related to the need for theory interpretation. We found the existing Locale and axiomatic type class mechanisms provided by the Isabelle theorem prover we were using to be inadequate. This led us to develop a new prototype implementation of theory interpretation. To support this implementation, we developed a novel system of proof terms for the HOL logic that we also describe in this thesis. We found existing automation to perform poorly, which led us to experiment with additional kinds of automation. We describe our approach, focusing on features that make automation suitable for interactive use. Our presentation of the case study starts with our formalisation of an abstract theory of distributed systems, covering state transition systems, forward and backward simulation relations, and related properties of LTL (linear temporal logic). We then summarise proofs of simulation relations holding for particular abstract multicast protocols. We discuss the mechanisation styles we experimented with in the case study. We also discuss the methodology behind our proofs. We cover aspects such as how to discover and construct proofs, and how to explore the space of proofs, how to make good definitions and lemmas, how to increase modularity, reuse, stability and malleability of proofs, and reduce maintenance of proofs, and the gap between intuitively understood proofs and their formalisation.

Developing logic in machines has always been an area of concern for scientists. Automated Theorem Proving is a field that has implemented the concept of logical consequence to a certain level. However, if the number of available axioms is very large then the probability of getting a proof for a conjecture in a reasonable time limit can be very small. This is where the ability to learn from previously proved theorems comes into play. If we see in our own lives, whenever a new situation S(NEW) is encountered we try to recollect all old scenarios S(OLD) in our neural system similar to the new one. Based on them we then try to find a solution for S(NEW) with the help of all related facts F(OLD) to S(OLD). Similar is the concept in this research. The thesis deals with developing a solution and finally implementing it in a tool that tries to prove a failed conjecture (a problem that the ATP system failed to prove) by extracting a sufficient set of axioms (we call it Refined Axiom Set (RAS)) from a large pool of available axioms. The process is carried out by measuring the similarity of a failed conjecture with solved theorems (already proved) of the same domain. We call it "process1", which is based on syntactic selection of axioms. After process1, RAS may still have irrelevant axioms, which motivated us to apply semantic selection approach on RAS so as to refine it to a much finer level. We call this approach as "process2". We then try to prove failed conjecture either from the output of process1 or process2, depending upon whichever approach is selected by the user. As for our testing result domain, we picked all FOF problems from the TPTP problem domain called SWC, which consisted of 24 broken conjectures (problems for which the ATP system is able to show that proof exists but not able to find it because of limited resources), 124 failed conjectures and 274 solved theorems. The results are produced by keeping in account both the broken and failed problems. The percentage of broken conjectures being solved with respect to the failed conjectures is obviously higher and the tool has shown a success of 100 % on the broken set and 19.5 % on the failed ones.

Thesis (M.S.)--Mathematics, Georgia Institute of Technology, 2005. / Belinfante, Johan, Committee Chair ; Green, William, Committee Member ; Manolios, Panagiotis, Committee Member. Includes bibliographical references.

Our work focuses on bringing the first-order reasoning closer to practicalapplications, particularly in software and hardware verification. The aim is to develop techniques that make first-order reasoners more scalablefor large problems and suitable for the applications. In pursuit of this goal the work focuses in three main directions. First, wedevelop an algorithm for an efficient pre-selection of axioms. This algorithmis already being widely used by the community and enables off-the-shelf theoremprovers to work with problems having millions of axioms that would otherwisebe overwhelming for them. Secondly, we focus on the saturation algorithm itself, and develop anew calculus for separate handling of propositional predicates. We also do anextensive research on various ways of clause splitting within the saturationalgorithm. The third main block of our work is focused on the use of saturation basedfirst-order theorem provers for software verification, particularly forgenerating invariants and computing interpolants. We base our work on theoretical results of Kovacs and Voronkov published in2009 on the CADE and FASE conferences. We develop a practical implementationwhich embraces all the extensions of the basic resolution and superposition calculus that are contained in the theorem prover Vampire. We have also developed a unique proof transforming algorithm which optimizes the computed interpolantswith respect to a user specified cost function.

We have previously argued that the syntactic structure of natural language can be exploited to construct powerful polynomial time inference procedures. This paper supports the earlier arguments by demonstrating that a natural language based polynomial time procedure can solve Schubert's steamroller in a single step.

In this thesis we explore a number of ways in which combinatorial games can be used to help prove results in the area of propositional proof complexity. The results in this thesis can be divided into two sets, the first being dedicated to the study of Resolution space (memory) requirements, whereas the second is centered on formalizing the notion of `dangerous' reductions. The first group of results investigate Resolution space measures by asking questions of the form, `Given a formula F and integer k, does F have a [Type of Resolution] proof with [Type of Resource] at most k?'. We refer to this as a proof complexity resource problem, and provide comprehensive results for several forms of Resolution as well as various resources. These results include the PSPACE-Completeness of Tree Resolution clause space (and the Prover/Delayer game), the PSPACE-Completeness of Input Resolution derivation total space, and the PSPACE-Hardness of Resolution variable space. This research has theoretical as well as practical motivations: Proof complexity research has focused on the size of proofs, and Resolution space requirements are an interesting new theoretical area of study. In more practical terms, the Resolution proof system forms the underpinnings of all modern SAT-solving algorithms, including clause learning. In practice, the limiting factor on these algorithms is memory space, so there is a strong motivation for better understanding it as a resource. With the second group of results in this thesis we investigate and formalize what it means for a reduction to be `dangerous'. The area of SAT-solving necessarily employs reductions in order to translate from other domains to SAT, where the power of highly-optimized algorithms can be brought to bear. Researchers have empirically observed that it is unfortunately possible for reductions to map easy instances from the input domain to hard SAT instances. We develop a non-Hamiltonicity proof system and combine it with additional results concerning the Prover/Delayer game from the first part of this thesis as well as proof complexity results for intuitionistic logic in order to provide the first formal examples of harmful and beneficial reductions, ultimately leading to the development of a framework for studying and comparing translations from one language to another.

In this thesis we explore a number of ways in which combinatorial games can be used to help prove results in the area of propositional proof complexity. The results in this thesis can be divided into two sets, the first being dedicated to the study of Resolution space (memory) requirements, whereas the second is centered on formalizing the notion of `dangerous' reductions. The first group of results investigate Resolution space measures by asking questions of the form, `Given a formula F and integer k, does F have a [Type of Resolution] proof with [Type of Resource] at most k?'. We refer to this as a proof complexity resource problem, and provide comprehensive results for several forms of Resolution as well as various resources. These results include the PSPACE-Completeness of Tree Resolution clause space (and the Prover/Delayer game), the PSPACE-Completeness of Input Resolution derivation total space, and the PSPACE-Hardness of Resolution variable space. This research has theoretical as well as practical motivations: Proof complexity research has focused on the size of proofs, and Resolution space requirements are an interesting new theoretical area of study. In more practical terms, the Resolution proof system forms the underpinnings of all modern SAT-solving algorithms, including clause learning. In practice, the limiting factor on these algorithms is memory space, so there is a strong motivation for better understanding it as a resource. With the second group of results in this thesis we investigate and formalize what it means for a reduction to be `dangerous'. The area of SAT-solving necessarily employs reductions in order to translate from other domains to SAT, where the power of highly-optimized algorithms can be brought to bear. Researchers have empirically observed that it is unfortunately possible for reductions to map easy instances from the input domain to hard SAT instances. We develop a non-Hamiltonicity proof system and combine it with additional results concerning the Prover/Delayer game from the first part of this thesis as well as proof complexity results for intuitionistic logic in order to provide the first formal examples of harmful and beneficial reductions, ultimately leading to the development of a framework for studying and comparing translations from one language to another.

This paper describes the proof calculus LD for clausal propositional logic, which is a linearized form of the well-known DPLL calculus extended by clause learning. It is motivated by the demand to model how current SAT solvers built on clause learning are working, while abstracting from decision heuristics and implementation details. The calculus is proved sound and terminating. Further, it is shown that both the original DPLL calculus and the conflict-directed backtracking calculus with clause learning, as it is implemented in many current SAT solvers, are complete and proof-confluent instances of the LD calculus. / Dieser Artikel beschreibt den Beweiskalkül LD für aussagenlogische Formeln in Klauselform. Dieser Kalkül ist eine um Klausellernen erweiterte linearisierte Variante des bekannten DPLL-Kalküls. Er soll dazu dienen, das Verhalten von auf Klausellernen basierenden SAT-Beweisern zu modellieren, wobei von Entscheidungsheuristiken und Implementierungsdetails abstrahiert werden soll. Es werden Korrektheit und Terminierung des Kalküls bewiesen. Weiterhin wird gezeigt, dass sowohl der ursprüngliche DPLL-Kalkül als auch der konfliktgesteuerte Rücksetzalgorithmus mit Klausellernen, wie er in vielen aktuellen SAT-Beweisern implementiert ist, vollständige und beweiskonfluente Spezialisierungen des LD-Kalküls sind.