Table of Contents 

KeYmaera X Usage
 KeYmaera X Documentation
 Start KeYmaera X and browse the Help menu
 Cheat Sheet for KeYmaera X
 Cheat Sheet for Differential Dynamic Logic
Old: KeYmaera 3 Usage
Previous instances of this course were using KeYmaera, the precursor of the more advanced theorem prover KeYmaera X. Your mileage from the KeYmaera documentation may vary, because it is thorough, but not adapted to KeYmaera X.Starring KeYmaera on YouTube Channel
 Tutorial: Install KeYmaera
 Tutorial: Open KeYmaera Using Java Web Start
 Tutorial: Find a Counterexample
 Tutorial: Loop Invariants with KeYmaera
 Tutorial: Simple Train Control
 Tutorial: Discover Constraints Using KeYmaera
 Tutorial: Differential Cuts, Invariants, and Weakening
 Tutorial: Abbreviate Rule
 Tutorial: Modeling Discrete Steering
 Tutorial: Differential Auxiliaries / Differential Ghosts
Typesetting Proofs
You are encouraged to typeset your theory homework solutions. Scans of handwritten homework solutions of a similarly high quality will be accepted. But if we cannot decipher your homework, we cannot give you any points for it.
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 top1,2,3
proof trees to obtainconclusion
.
\LeftLabel{lab}
adds a label to the next proof step.  mathpartir.sty

LKproof/proof.sty
[examples]
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 cyberphysical 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.

André Platzer.
Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics.
Springer, 2010. 426 pages. ISBN 9783642145087.
[bib  doi  book  web]
Ordinary Differential Equations
 Course notes from 21122 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 9780387984599
 Jörn Loviscach and Miriam Swords Kalk. Differential equations in action.
 Khan Academy. First order differential equations. (very basic, image quality issues)
FirstOrder 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 178.
 André Platzer.
Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics.
Springer, 2010.
Appendix A (advanced)  Mordechai BenAri. 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).