Mechanized Reasoning for Continuous Problem Domains (Extended Abstract)

1st International Workshop on Practical Aspects of Automated Reasoning

R.D. Arthan

Others  :  http://CEUR-WS.org/Vol-373/invited-2.pdf
PID  :  46906

来源: CEUR

【 摘 要 】

Specification and verification in continuous problem domains are key topics for the practical application of formal methods and mechanized reasoning. I discuss one approach to linear continuous control systems and consider the challenges and opportunities raised for mechanized reasoning. These include practical implementation and integration issues, algorithms in computational real algebraic geometry and hard open questions such as the Schanuel conjecture. I conclude with an overview of some recent new results on decidability and undecidabil ity for vector spaces and related theories.