This thesis is about automated reasoning in quantified modal and temporal logics, with an application to formal methods. Quantified modal and temporal logics are extensions of classical first-order logic in which the notion of truth is extended to take into account its necessity or equivalently, in the temporal setting, its persistence through time. Due to their high complexity, these logics are less widely known and studied than their propositional counterparts. Moreover, little so far is known about their mechanisability and usefulness for formal methods. The relevant contributions of this thesis are threefold: firstly, we devise a sound and complete set of sequent calculi for quantified modal logics; secondly, we extend the approach to the quantified temporal logic of linear, discrete time and develop a framework for doing automated reasoning via Proof Planning in it; thirdly, we show a set of experimental results obtained by applying the framework to the problem of Feature Interactions in telecommunication systems. These results indicate that (a) the problem can be concisely and effectively modeled in the aforementioned logic, (b) proof planning actually captures common structures in the related proofs, and (c) the approach is viable also from the point of view of efficiency.

In “Proof-Theoretic Justification of Logic”, building on work by Dummett and Prawitz, I show how to construct use-based meaning-theories for the logical constants. The assertability-conditional meaning-theory takes the meaning of the logical constants to be given by their introduction rules; the consequence-conditional meaning-theory takes the meaning of the logical constants to be given by their elimination rules. I then consider the question: given a set of introduction (elimination) rules \(\mathcal{R}\), what are the strongest elimination (introduction) rules that are validated by an assertability (consequence) conditional meaning-theory based on \(\mathcal{R}\)? I prove that the intuitionistic introduction (elimination) rules are the strongest rules that are validated by the intuitionistic elimination (introduction) rules. I then prove that intuitionistic logic is the strongest logic that can be given either an assertability-conditional or consequence-conditional meaning-theory. In “Grounding Grounding” I discuss the notion of grounding. My discussion revolves around the problem of iterated grounding-claims. Suppose that \(\Delta\) grounds \(\phi\); what grounds that \(\Delta\) grounds that \(\phi\)? I argue that unless we can get a satisfactory answer to this question the notion of grounding will be useless. I discuss and reject some proposed accounts of iterated grounding claims. I then develop a new way of expressing grounding, propose an account of iterated grounding-claims and show how we can develop logics for grounding. In “Is the Vagueness Argument Valid?” I argue that the Vagueness Argument in favor of unrestricted composition isn’t valid. However, if the premisses of the argument are true and the conclusion false, mereological facts fail to supervene on non-mereological facts. I argue that this failure of supervenience is an artifact of the interplay between the necessity and determinacy operators and that it does not mean that mereological facts fail to depend on non-mereological facts. I sketch a deflationary view of ontology to establish this. / Philosophy

In this dissertation it is shown that abstract data types (ADTs) can be specified by the Classified Model (CM) specification language - a first-order Horn language with equality and sort "classification" assertations. It is shown how these sort assertations generalize the traditional syntactic signatures of ADT specifications, resulting in all of the specification capability of traditional equational specifications, but with the improved expressibility of the Horn-with-equality language and additional theorem proving applications such as program synthesis. This work extends corresponding results from Many Sorted Algebra (MSA), Order Sorted Algebra (OSA) and Order Sorted Model (OSM) specification techniques by promoting their syntactic signatures to assertions in the Classified Model Specification language, yet retaining sorted quantification. It is shown how this solves MSA problems such as error values, polymorphism and subtypes in a way different from the OSA and OSM solutions. However, the CM technique retains the MSA and order sorted approach to parameterization. The CS generalization also suggests the use of CM specifications to axiomatize modules as a generalization of variables within Hoare Logic, with application to a restricted, but safe, use of procedures as state changing operations and functions as value returning operations of a module. CM proof theory and semantics are developed, including theorems for soundness, completeness and the existence of a free model.

Inference systems Τ and search strategies E for T are distinguished from proof procedures β = (T,E) The completeness of procedures is studied by studying separately the completeness of inference systems and of search strategies. Completeness proofs for resolution systems are obtained by the construction of semantic trees. These systems include minimal α-restricted binary resolution, minimal α-restricted M-clash resolution and maximal pseudo-clash resolution. Certain refinements of hyper-resolution systems with equality axioms are shown to be complete and equivalent to refinements of the pararmodulation method for dealing with equality. The completeness and efficiency of search strategies for theorem-proving problems is studied in sufficient generality to include the case of search strategies for path-search problems in graphs. The notion of theorem-proving problem is defined abstractly so as to be dual to that of and" or tree. Special attention is given to resolution problems and to search strategies which generate simpler before more complex proofs. For efficiency, a proof procedure (T,E) requires an efficient search strategy E as well as an inference system T which admits both simple proofs and relatively few redundant and irrelevant derivations. The theory of efficient proof procedures outlined here is applied to proving the increased efficiency of the usual method for deleting tautologies and subsumed clauses. Counter-examples are exhibited for both the completeness and efficiency of alternative methods for deleting subsumed clauses. The efficiency of resolution procedures is improved by replacing the single operation of resolving a clash by the two operations of generating factors of clauses and of resolving a clash of factors. Several factoring methods are investigated for completeness. Of these the m-factoring method is shown to be always more efficient than the Wos-Robinson method.

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.

Thesis (Ph. D.)--University of Texas at Austin, 2008. / Vita. Includes bibliographical references.

Habilitationsschrift--Bonn. / Includes bibliographical references (p. 93).

Habilitationsschrift--Bonn. / Includes bibliographical references (p. 93).

Thesis (M. Ed.)--University of Hong Kong, 1995. / Includes bibliographical references (leaf 90-99).

Thesis (M.S.)--Missouri State University, 2008. / "August 2008." Includes bibliographical references (leaf 53). Also available online.