Date of Degree

2009

Document Type

Dissertation

Degree Name

Ph.D.

Program

Computer Science

Advisor(s)

Sergei Artemov

Committee Members

Melvin Fitting

Robert Milnikel

Subash Shankar

Subject Categories

Computer Sciences

Abstract

In the first Chapter we compare two well-known type-based computer frameworks for computer aided logical reasoning and verification: MetaPRL and Coq. In particular, we implement in MetaPRL the Calculus of Inductive Constructions which is the theoretical base for Coq. This work has shown the common points of MetaPRL and Coq, and revealed their principal methodological differences. A possible application of this work is a possibility to perform re-validation in MetaPRL of the existing library of Coq proofs which could help to build more trust in the latter.

Chapter 2 is the main contribution of the dissertation. It contains the description and testing results of an implementation of realization algorithm in epistemic modal logic that converts cut-free derivations in multi-agent epistemic modal logic into derivations in the corresponding Justification Logic where witnesses of knowledge (justification terms) are recovered for all instances of common knowledge. We also apply this algorithms to several well-known epistemic puzzles, such as Muddy Children, Wise Men, Wise Girls, etc.

Comments

Digital reproduction from the UMI microform.

Share

COinS
 
 

To view the content in your browser, please download Adobe Reader or, alternately,
you may Download the file to your hard drive.

NOTE: The latest versions of Adobe Reader do not support viewing PDF files within Firefox on Mac OS and if you are using a modern (Intel) Mac, there is no official plugin for viewing PDF files within the browser window.