System description: inka 5.0-a logic voyager

摘要

Originally developed as an automatic inductive theorem prover [2] based on resolution and paramodulation, the inka system was redesigned in inka 4.0 in the early '90s [8] to meet the requirements arising from its designated use in formal methods. Meanwhile several large industrial applications of the verification support environment (VSE) [7] have been performed which gave rise to thousands of proof obligations to be tackled by its underlying deductive system inka.