ImandraX examples and code samples. These are meant to be run in the ImandraX VS Code extension.
To get started with ImandraX, install the ImandraX VS Code extension and follow the instructions it gives you for setting up an Imandra Universe API key.
Once you have ImandraX installed, each of these examples may be run by opening the corresponding
.iml file and pressing Save (e.g., CMD+S) to check all definitions in the file.
Be sure to use the VS Code command ImandraX: Open Goal State to view the goals as they
are proved. This is also useful when constructing your own interactive proofs.
This repo currently includes the following examples proved in ImandraX:
- Insertion sort
- Merge sort
- Quick sort
- Cantor's pairing function
- A simple expression compiler
- A stack machine and loop program
- Mutilated Chessboard Theorem
- Pigeon Hole Principle
- Permutations
- Bags (Multisets)
- Gilbreath's Card Trick
- Ackermann's Function
- Ripple carry adder
- Simple autonomous vehicle controller
- 3s and 5s coin change theorem
- Towers of Hanoi player
- Boyer-Moore Majority Voting Algorithm
- A tautology checker (SAT solver) based on if-normalization
- Some theorems on summations
- Farkas' Lemma
Plus some other misc. examples to help users learn about ImandraX's tactic language.
If you need help, join our community forum at www.imandra.ai!