A calculational approach to mathematical induction

DOI10.1016/S0304-3975(96)00154-5zbMath0901.68124OpenAlexW2099163661WikidataQ56874028 ScholiaQ56874028MaRDI QIDQ1391737

Jaap van der Woude, Henk Doornbos, Roland C. Backhouse

Publication date: 22 July 1998

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(96)00154-5

zbMATH Keywords

variable-free relation algebra

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Related Items

Formal derivation of greedy algorithms from relational specifications: a tutorial ⋮ Algebraic coherent confluence and higher globular Kleene algebras ⋮ Automated Reasoning in Higher-Order Regular Algebra ⋮ Components and acyclicity of graphs. An exercise in combining precision with concision ⋮ Jumping and escaping: modular termination and the abstract path ordering ⋮ Programming from metaphorisms ⋮ Programming from Galois connections ⋮ Left omega algebras and regular equations ⋮ Complete Lattices and Up-To Techniques ⋮ A relation-algebraic approach to the ``Hoare logic of functional dependencies ⋮ Relational characterisations of paths ⋮ Modal Tools for Separation and Refinement ⋮ Embedding mappings and splittings with applications ⋮ Unnamed Item ⋮ Extended Static Checking by Calculation Using the Pointfree Transform ⋮ On Distributive Fixed-Point Expressions ⋮ Datatype-generic termination proofs ⋮ Nondeterministic semantics of compound diagrams ⋮ Abstract abstract reduction

Cites Work

• Fixed-point calculus
• The joy of formula manipulation
• Reductivity
• On theories with a combinatorial definition of 'equivalence'
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Regular Algebra Applied to Path-finding Problems
• Demonic operators and monotype factors
• Two Complete Axiom Systems for the Algebra of Regular Events
• Non-Commutative Residuated Lattices
• Relations binaires, fermetures, correspondances de Galois
• Galois Connexions
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item