15-424: Logical Foundations of Cyber-Physical Systems (Fa'21)

KeYmaera X Usage

• KeYmaera X Documentation
• KeYmaera X Tutorial
• Start KeYmaera X and browse the Help menu
• Cheat Sheet for KeYmaera X
• Cheat Sheet for Differential Dynamic Logic

Typesetting Proofs

Different packages exist for typesetting proofs in LaTeX. They have different advantages and downsides so it may be a matter of personal preference which one works best for you.

• bussproofs.sty provides a stack machine for programming proof typesetting (i.e. the state is a stack of proof trees).
  \AxiomC{axiom} adds a leaf to the stack.
  \UnaryInfC{conclusion}, \BinaryInfC{conclusion}, \TrinaryInfC{conclusion} combine the top 1,2,3 proof trees to obtain conclusion.
  \LeftLabel{lab} adds a label to the next proof step.
• mathpartir.sty
  Displaymath with several formulas in a row including lines for proof steps
• LKproof/proof.sty
  Package for LK proof diagrams and other proofs
  [examples]
• My TeX logic packages
  Provides fairly flexible proof layout styles and separate declaration of rule name references. Unfortunately, the only documentation is in the logic-template.tex file and the source code comments.

Further Reading

This course will make heavy use of differential equations, logic and theorem proving. While each of those topics will be discussed in this course, you are expected to be able to get up to speed quickly. Depending on your prior background and how well you remember this material from other courses, we recommend that you look at some of the following resources before the semester starts. This will make it easier for you to get going in cyber-physical systems. You may also find these resources helpful for extra reading throughout the semester.

You should feel very comfortable with the elementary background material, e.g., what a differential equation is, before the course begins. We also include advanced materials for interested students.

We will also add further reading material as the course progresses.

1. André Platzer.
   Logical Foundations of Cyber-Physical Systems.
   Springer, Cham, 2018. 659 pages. ISBN 978-3-319-63587-3.
   [bib | ⧉ | doi | slides | video | book | web | errata | abstract]
   
   
2. André Platzer.
   Logical Analysis of Hybrid Systems:
      Proving Theorems for Complex Dynamics.
   Springer, Heidelberg, 2010. 426 pages. ISBN 978-3-642-14508-7.
   [bib | ⧉ | doi | book | web | errata | abstract]
   
   

1. [e-book in CMU Library]

Ordinary Differential Equations

• Course notes from 21-122 Integration, Differential Equations, and Approximation
• André Platzer. Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, 2010.
  Appendix B
• Nykamp DQ. Ordinary differential equation examples. From Math Insight.
• Nykamp DQ. An introduction to ordinary differential equations. From Math Insight.
• Wolfgang Walter. Ordinary Differential Equations. Springer, 1998. ISBN 978-0387984599
• Carmen Chicone. Ordinary Differential Equations with Applications. Springer, 2006. ISBN 978-0-387-30769-5
• Jörn Loviscach and Miriam Swords Kalk. Differential equations in action.
• Khan Academy. First order differential equations. (very basic, image quality issues)

First-Order Logic

• Explore the sequent calculus directly in KeYmaera X
• Interactive Tutorial of the Sequent Calculus
• Samuel R. Buss. An Introduction to Proof Theory in Handbook of Proof Theory. Elsevier, 1998. pp 1-78.
• André Platzer. Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, 2010.
  Appendix A (advanced)
• Mordechai Ben-Ari. Mathematical Logic for Computer Science. Springer, 2012.
  Chapters 1, 2, 3.2, 7, 8.1 (focus is on tableaux calculus instead of sequent calculus, though, which causes quite some notational differences).