Skip to content

smart_induct for IJCAR2020

Pre-release
Pre-release
Compare
Choose a tag to compare
@yutakang yutakang released this 26 Jan 23:25
· 620 commits to master since this release
v0.1.5-alpha
d77fc23
This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Learn about vigilant mode.

smart_induct

Dear IJCAR reviewers.
Our running example explained in the paper resides in PSL/Smart_Induct/Example/Induction_Demo.thy.

To use smart_induct in your own file,
you only have to use import Smart_Induct.thy in this directory using the imports keyword of Isabelle/HOL.
It is important to set the path to Smart_Induct.thy correctly.

The evaluation files reside in the Evaluation directory.
If you open the following files using Isabelle2019, you can see smart_induct at work:

  • PSL/Smart_Induct/Evaluation/Depth-First-Search/DFS.thy
  • PSL/Smart_Induct/Evaluation/KD_Tree/Nearest_Neighbor.thy
  • PSL/Smart_Induct/Evaluation/Priority_Search_Trees/PST_RBT.thy.

Enjoy!

System requirements:

  • Isabelle2019 (The vastest official version of Isabelle at the time of release.)
  • A modern computer that can handle Isabelle/HOL will do. For example, you might want to have 16 GB of memory.
Assets 2
Loading