核心概念
연역 시스템을 사용하면 안정성 증명을 기계적으로 검증할 수 있으며, 이를 통해 증명의 일반화, 재사용성 및 정확성을 높일 수 있다.
摘要
이 논문은 리아푸노프 정리를 사용하여 제어 시스템의 안정성을 증명하는 과정을 다룹니다.
먼저 리아푸노프 안정성 이론과 차분 동적 논리(differential dynamic logic, dL)에 대해 소개합니다. 그리고 역진자 시스템을 예로 들어 안정성 조건을 도출합니다.
이어서 KeYmaera X 도구를 사용하여 리아푸노프 정리의 기계적 증명 과정을 설명합니다. 이 과정은 크게 세 부분으로 나뉩니다:
- 안정성(stability)과 끌림성(attractivity)으로 나누어 증명하는 과정
- 평형점의 도달가능성(reachability)을 증명하는 과정
- 평형점의 안정성(stability)을 증명하는 과정
이를 통해 연역 시스템을 사용하면 수학적 증명을 기계적으로 검증할 수 있고, 증명의 일반화, 재사용성 및 정확성을 높일 수 있음을 보여줍니다.
統計資料
역진자 시스템의 동역학은 ˙
x = (ω, dθ + bω)로 표현된다.
리아푸노프 함수는 V = ml^2/2 * (-d - bp12)θ^2 + 2p12θω + ω^2 로 정의된다.
안정성 조건은 p11 > p12^2 ∧ p12 > 0 ∧ -p11/p12 < b < -p12 이다.
引述
"연역 시스템을 사용하면 안정성 증명을 기계적으로 검증할 수 있으며, 이를 통해 증명의 일반화, 재사용성 및 정확성을 높일 수 있다."
"수학적 증명을 기계적으로 검증하고 증명의 일반화, 재사용성 및 정확성을 높이는 것이 중요하다."