Rule-based induction
type: Item
instance of: scholarly article
title: Rule-based induction
zbMATH Open document ID: 0810.68114
DOI: 10.1007/BF01384232
author: Holger Busch
published in: Formal Methods in System Design
publication date: 1994-09-26T00:00:00Z
review text: 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.
reviewed by: Daniele Mundici
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 644670
zbMATH Keywords: software verification
describes a project that uses: Oyster
MaRDI profile type: Publication
cites work: Rippling: A heuristic for guiding inductive proofs
cites work: Q3992669
cites work: Q4028154
cites work: Edinburgh LCF. A mechanized logic of computation
cites work: Q3753927
cites work: Q4255517
description: scientific article; zbMATH DE number 644670