Formalization of Laplace Transform in Coq

被引：11

作者：

Wang, Yifei ^{[1
]}

Chen, Gang ^{[2
]}

机构：

[1] Nanjing Univ Aeronaut & Astronaut, Coll Comp Sci Technol, Nanjing 210000, Jiangsu, Peoples R China

[2] Beijing Jinghang Res Inst Comp & Commun, 1 Beiqu Xili, Beijing 100074, Peoples R China

来源：

2017 FOURTH INTERNATIONAL CONFERENCE ON DEPENDABLE SYSTEMS AND THEIR APPLICATIONS (DSA 2017) | 2017年

关键词：

Laplace transform; formalized mathematics; engineering mathematics; Coq; theorem proving; formal verification;

D O I：

10.1109/DSA.2017.12

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

In engineering mathematics, Laplace transform is a widely used tool for solving linear differential equations, particularly in the design and analysis of safety critical control systems. This paper reports a formalization of Laplace transform in Coq. A group of basic properties of Laplace transform are proved, including linear property, frequency shifting and first order differentiation. This work is part of a grand project of formalizing flight control mathematics.

引用

页码：13 / 21

页数：9

共 10 条

[1]

[Anonymous], 1994, AUTOMATED DEDUCTION

[2] Formalization of real analysis: a survey of proof assistants and libraries [J].

Boldo, Sylvie ;

Lelay, Catherine ;

Melquiond, Guillaume .

MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2016, 26 (07) :1196-1233

[3] Coquelicot: A User-Friendly Library of Real Analysis for Coq [J].

Boldo, Sylvie ;

Lelay, Catherine ;

Melquiond, Guillaume .

MATHEMATICS IN COMPUTER SCIENCE, 2015, 9 (01) :41-62

[4]

Gonthier G, 2013, LECT NOTES COMPUT SC, V7998, P163, DOI 10.1007/978-3-642-39634-2_14

[5]

Harrison John, 1996, 36 TUCS

[6]

Rashid A., INT C INT COMP MATH, P319

[7]

Taqdees Syeda Hira, 2013, Logic for Programming, Artificial Intelligence and Reasoning. 19th International Conference, LPAR-19, Proceedings: LNCS 8312, P744, DOI 10.1007/978-3-642-45221-5_50

[8]

Ward B J, 1990, COMPLEX VARIABLES AP, V37, P140

[9]

Wiedijk F., 2008, NOT AM MATH SOC, V55, P1408

[10]

Zhao Gang, 2014, Journal of Chinese Computer Systems, V35, P2177

← 1 →