Dissertations, Theses, and Capstone Projects
Date of Degree
2009
Document Type
Dissertation
Degree Name
Ph.D.
Program
Computer Science
Advisor
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.
Recommended Citation
Novak, Natalia, "Computer-Aided Reasoning about Knowledge and Justifications" (2009). CUNY Academic Works.
https://academicworks.cuny.edu/gc_etds/1708
Comments
Digital reproduction from the UMI microform.