scientific article; zbMATH DE number 139989

MaRDI QIDQ4028349zbMATH OpenFDO

Authors Ulrich Fraus, Heinrich Hussmann

Publication date 28 March 1993

zbMATH Keywords

development of formally verified softwareequational axiomatic specificationsinductioninteractive generation of inductive proofsnarrowingterm rewriting

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Narrowing based inductive proof search
• Narrowing, Abstraction and Constraints for Proving Properties of Reduction Relations
• Automatic proofs by induction in theories without constructors
• Inductive proofs by specification transformations
• scientific article; zbMATH DE number 4074541

Cited in

(8)

• Inductive proof search modulo
• The equational part of proofs by structural induction
• An improved general path order
• Higher-order proof construction based on first-order narrowing
• TIP: tools for inductive provers
• Narrowing, Abstraction and Constraints for Proving Properties of Reduction Relations
• Narrowing based inductive proof search
• On the connection between narrowing and proof by consistency

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4028349)