scientific article; zbMATH DE number 1302503

MaRDI QIDQ4249033zbMATH OpenFDO

Authors Jürgen Avenhaus, Klaus Madlener

Publication date 31 August 1999

zbMATH Keywords

semanticsHorn clauseinductive theorem provingalgebraic specification languageinductive validityconditional specifications over built-in algebras

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70)

Recommendations

• scientific article; zbMATH DE number 1008505
• A calculus for conditional inductive theorem proving
• scientific article; zbMATH DE number 4090849
• Inductive theorem proving based on tree grammars
• Inductive theorem proving by consistency for first-order clauses
• Inductive theorem proving for design specifications
• scientific article; zbMATH DE number 1300967
• scientific article; zbMATH DE number 3965464
• A proof system for conditional algebraic specifications

Cited in

(8)

• Inductive theorem proving based on tree grammars
• Inductive theorem proving for design specifications
• On notions of inductive validity for first-order equational clauses
• Focused Inductive Theorem Proving
• A calculus for conditional inductive theorem proving
• scientific article; zbMATH DE number 671941 (Why is no real title available?)
• scientific article; zbMATH DE number 3876565 (Why is no real title available?)
• Conditional equational specifications of data types with partial operations for inductive theorem proving

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 Q4249033)