Simplifying transformations for type-alpha certificates
This paper presents an algorithm for simplifying NDL deductions. An array of simplifying transformations are rigorously defined. They are shown to be terminating, and to respect the formal semantis of the language. We also show that the transformations never increase the size or complexity of a dedu...
Main Author: | Arkoudas, Konstantine |
---|---|
Language: | en_US |
Published: |
2004
|
Subjects: | |
Online Access: | http://hdl.handle.net/1721.1/6680 |
Similar Items
-
Type-alpha DPLs
by: Arkoudas, Konstantine
Published: (2004) -
Type-omega DPLs
by: Arkoudas, Konstantine
Published: (2004) -
Credible Compilation *
by: Rinard, Martin C.
Published: (2003) -
The complexity of quantum disjointness
by: Klauck, Hartmut
Published: (2018) -
A Virtual Machine for a Type-omega Denotational Proof Language
by: III, Teodoro Arvizo
Published: (2004)