Rule-based induction (Q1334895)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Rule-based induction |
scientific article |
Statements
Rule-based induction (English)
0 references
26 September 1994
0 references
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.
0 references
software verification
0 references