具体的なハイブリッドシステムの微分的な洗練のための統一的な置換

本論文は、微分的な洗練論理(dRL)のための統一的な置換計算を導入する。dRLは、ハイブリッドシステムの性質と関係を同時に推論できるように、微分動的論理(dL)を拡張したものである。洗練は、抽象的なハイブリッドシステムから、より簡単に性質を証明できる具体的なシステムに関係付けることで、証明を簡略化するのに有用である。統一的な置換は、証明計算の中核部分の簡素化のための鍵となる。これにより、音響性に関する副条件が散在する axiom schemata の代わりに、単一の axiom 式を文字通り使うことができる。