Rule-based induction (Q1334895)

Induction is increasingly being mechanized in systems for the formal approach to hardware and software verification. The author presents a method of proof by induction using the expressive power of higher-order logic, as well as the higher order facilities of LAMBDA, an interactive proof system that finds use in the design and verification of digital systems. The system also features functions for the splitting of goals into subgoals, as well as libriaries of common logic definitions and rules. Induction schemes are taken care of rather concisely by rules containing instantiable meta-variables.