The title of my dissertation is "confirmation theory & confirmation logic", and it consists of five Parts. The motivation of the dissertation was to construct an adequate confirmation theory that could solve "the paradoxes of confirmation" discovered by Carl G. Hempel. In Part One I try mainly to do the three things, (i) introduce the fundamentals of Hempel's theory of qualitative confirmation as the common background for subsequent discussions, (ii) review the major views of the paradoxes of confirmation, (iii) present a new view, which is more radical than other known views, and argue that a solution to the paradoxes of confirmation may require a change of logic. In Part Two I construct a number of promising three-valued logics. I employ these "quasi confirmation logics" as the underlying logics of some new confirmation theories which, I had hoped, would solve the paradoxes of confirmation. I consider three-valued logics instead of any other many-valued logics as the underlying logic for any promising confirmation theory, because I believe that there is some intimate relationship or, even, a one-to-one correspondence between the (controversial) three truth-values of "truth", "falsity" and "neither truth nor falsity" and, respectively, the (non-controversial) three confirmation-statuses of "confirmation", "disconfirmation" and "neutrality". Unfortunately, these theories were found to be semantically inadequate. This became clear after a complete semantics for them had been developed. Thus, one negative result of Part Two is that our syntactical approach to confirmation theory is wrong from the very beginning. However, from this negative result we learn a positive lesson: a semantical approach is more fundamental and decisive than a syntactical one, at least this is so for constructing an adequate theory of confirmation. It is rewarding to note that the three-valued semantics worked out in Part Two is simple, complete and the first of its kind. In fact, the new three-valued semantics is in the spirit of Frege, although the line of thought is much neglected (even by Frege himself). In Part Three I shift the search for a confirmation logic and an adequate theory of confirmation from a syntactical to a semantical approach because of the lesson learned in Part Two. After a systematic search through several promising three-valued logics I come, at last, to a plausible confirmation logic and to a confirmation theory that could solve all known paradoxes of confirmation. The promising three-valued confirmation theory is called "the internal confirmation theory". In Part Four I review and appraise the adequacy conditions laid down by Hempel as the necessary conditions for any adequate confirmation theory. Under the criticisms of Carnap, Goodman and, especially, with the help of Hanen's thorough studies, I come to almost an identical conclusion to Hanen's we should not impose a priori in a theory of qualitative confirmation any adequacy conditions laid down by Hempel except perhaps the Entailment Condition, although the internal confirmation theory also adopts the Equivalence Condition for some intrinsic reasons. In the last Part Five I try to appraise the three most important confirmation theories discussed and/or constructed in this dissertation. They are Hempel's theory of confirmation, Goodman's and Scheffler's theory of selective confirmation and the internal confirmation theory. After some more vigorous criticisms are made and some new paradoxes of confirmation are unexpectedly derived in both the theory of selective confirmation and the internal confirmation theory, I arrive at, perhaps reluctantly, this more reasonable conclusion under the present situation when there is no obvious way to overcome the new difficulties the best thing that we can do is to dissolve (i.e. to live with) all new and old paradoxes of confirmation, for Hempel may be after all right to say that the paradoxes of confirmation are not genuine and to think otherwise is to have psychological illusions as Hempel says. / Arts, Faculty of / Philosophy, Department of / Graduate

No description available.

Thesis (M.A.)--University of Wyoming, 2008. / Title from PDF title page (viewed on Mar. 23, 2010). Includes bibliographical references (p. 93-94).

Thesis (Ph. D.)--University of Wisconsin--Madison, 1973. / Typescript. Vita. eContent provider-neutral record in process. Description based on print version record. Bibliography: leaves 262-263.

Thesis (Ph. D.)--University of Texas at Austin, 1999. / Vita. Includes bibliographical references (leaves 141-155). Available also in a digital version from Dissertation Abstracts.

Thesis (M.A.)--University of Wyoming, 2007. / Title from PDF title page (viewed on Dec. 3, 2008). Includes bibliographical references (p. 76-79).

This thesis studies how to eliminate syntactic complexity in Lμ, the modal μ calculus. Lμ is a verification logic in which a least fixpoint operator μ, and its dual v, add recursion to a simple modal logic. The number of alternations between μ and v is a measure of complexity called the formula’s index: the lower the index, the easier a formula is to model-check. The central question of this thesis is a long standing one, the Lμ index problem: given a formula, what is the least index of any equivalent formula, that is to say, its semantic index? I take a syntactic approach, focused on simplifying formulas. The core decidability results are (i) alternative, syntax-focused decidability proofs for ML and Pμ 1 , the low complexity classes of μ; and (ii) a proof that Ʃμ 2 , the fragment of Lμ with one alternation, is decidable for formulas in the dual class Pμ 2 . Beyond its algorithmic contributions, this thesis aims to deepen our understanding of the index problem and the tools at our disposal. I study disjunctive form and related syntactic restrictions, and how they affect the index problem. The main technical results are that the transformation into disjunctive form preserves Pμ 2 -indices but not μ 2 -indices, and that some properties of binary trees are expressible with a lower index using disjunctive formulas than non-deterministic automata. The latter is part of a thorough account of how the Lμ index problem and the Rabin–Mostowski index problem for parity automata are related. In the final part of the thesis, I revisit the relationship between the index problem and parity games. The syntactic index of a formula is an upper bound on the descriptive complexity of its model-checking parity games. I show that the semantic index of a formula Ψ is bounded above by the descriptive complexity of the model-checking games for Ψ. I then study whether this bound is strict: if a formula Ψ is equivalent to a formula in an alternation class C, does a formula of C suffice to describe the winning regions of the model-checking games of Ψ? I prove that this is the case for ML, Pμ 1 , Ʃμ 2 , and the disjunctive fragment of any alternation class. I discuss the practical implications of these results and propose a uniform approach to the index problem, which subsumes the previously described decision procedures for low alternation classes. In brief, this thesis can be read as a guide on how to approach a seemingly complex Lμ formula. Along the way it studies what makes this such a difficult problem and proposes novel approaches to both simplifying individual formulas and deciding further fragments of the alternation hierarchy.

No abstract available. / Thesis (M.A.) - University of KwaZulu-Natal, Pietermaritzburg, 2007.

This dissertation shows that satisfiability procedures are abstract interpreters. This insight provides a unified view of program analysis and satisfiability solving and enables technology transfer between the two fields. The framework underlying these developments provides systematic recipes that show how intuition from satisfiability solvers can be lifted to program analyzers, how approximation techniques from program analyzers can be integrated into satisfiability procedures and how program analyzers and satisfiability solvers can be combined. Based on this work, we have developed new tools for checking program correctness and for solving satisfiability of quantifier-free first-order formulas. These tools outperform existing approaches. We introduce abstract satisfaction, an algebraic framework for applying abstract interpre- tation to obtain sound, but potentially incomplete satisfiability procedures. The framework allows the operation of satisfiability procedures to be understood in terms of fixed point computations involving deduction and abduction transformers on lattices. It also enables satisfiability solving and program correctness to be viewed as the same algebraic problem. Using abstract satisfaction, we show that a number of satisfiability procedures can be understood as abstract interpreters, including Boolean constraint propagation, the dpll and cdcl algorithms, St ̊almarck’s procedure, the dpll(t) framework and solvers based on congruence closure and the Bellman-Ford algorithm. Our work leads to a novel understand- ing of satisfiability architectures as refinement procedures for abstract analyses and allows us to relate these procedures to independent developments in program analysis. We use this perspective to develop Abstract Conflict-Driven Clause Learning (acdcl), a rigorous, lattice-based generalization of cdcl, the central algorithm of modern satisfiability research. The acdcl framework provides a solution to the open problem of lifting cdcl to new prob- lem domains and can be instantiated over many lattices that occur in practice. We provide soundness and completeness arguments for acdcl that apply to all such instantiations. We evaluate the effectiveness of acdcl by investigating two practical instantiations: fp-acdcl, a satisfiability procedure for the first-order theory of floating point arithmetic, and cdfpl, an interval-based program analyzer that uses cdcl-style learning to improve the precision of a program analysis. fp-acdcl is faster than competing approaches in 80% of our benchmarks and it is faster by more than an order of magnitude in 60% of the benchmarks. Out of 33 safe programs, cdfpl proves 16 more programs correct than a mature interval analysis tool and can conclusively determine the presence of errors in 24 unsafe benchmarks. Compared to bounded model checking, cdfpl is on average at least 260 times faster on our benchmark set.

The subject of this thesis is to study available security protocols and tools for their verification. The first part is devoted to briefly describe the concepts related to the area of security protocols and verification logics. The second part directly lists various protocols, along with attacks and errors found in design. Next chapter describes the most important tools for automatic analysis of security protocols in more detail. The main part deals with verification of security protocols selected in the chosen tool called Scyther. In conclusion, examples of multiprotocol attacks along with a summary table are displayed.