Theory of Knowledge in Isabelle
Overview
Theory of Knowledge in Isabelle.
A model in isabelle contributing to X-Logic architecture and the design of XL-Glue. This version includes the use of signatures.
X-Logic metamodel no.2
A model in isabelle contributing to X-Logic architecture and the design of XL-Glue. This version includes the use of signatures.
Introduction
This second in a series of models in which the metatheory of X-Logic is developed, improves on the first model by allowing that programs read and write multiple documents, and by introducing the use of digital signatures to provide degrees of confidence in the truth of documents and the soundness of programs.
Abstract Syntax
The abstract syntax of our metalanguage is defined using a datatype in isabelle HOL.
Semantics
The semantics of sentences and judgements is defined as truth valuations relative to appropriate interpretations.
Proof Rules
Soundness, Monotonicity and Safety

up quick index © RBJ

$Id: index.xml,v 1.1.1.1 2000/12/04 17:23:22 rbjones Exp $