Proving semantical equivalence of data specifications

DOI10.1016/S0022-4049(96)00168-5MaRDI QIDQ678825zbMATH OpenFDO

Authors Frank Piessens, Eric Steegmans

Publication date 16 July 1997

Published in Journal of Pure and Applied Algebra (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/S0022-4049(96)00168-5

zbMATH Keywords

categories of finite modelsdata specificationequivalence problemessentially algebraic specificationsketchesview integration problem

Mathematics Subject Classification ID

Partial algebras (08A55) Functor categories, comma categories (18A25) Categories admitting limits (complete categories), functors preserving limits, completions (18A35) Theories (e.g., algebraic theories), structure, and semantics (18C10) Database theory (68P15) Abstract data types; algebraic specification (68Q65)

Review text

The paper deals with the problem of determining whether two given data specifications are equivalent. The equivalence is defined by the equivalence of the corresponding categories of finite models. The equivalence problem is undecidable because finite satisfiability in model theory can be reduced to it. There is a stronger concept of equivalence of data specifications which is given by the equivalence of the categories of all (also infinite) models. The authors reduce the strong equivalence problem (via sketches and their theories) to a deduction problem for essentially algebraic specification. Finally, they present a deduction system for these specifications which is claimed to be very suitable for an automated theorem prover. The paper seems to be an interesting application of category theory to computer science.

Recommendations

• Specification and verification for semi-structured data
• Semantic specification and verification of data flow diagrams
• A Proof Procedure for Data Dependencies
• Theorem prover approach to semistructured data design
• Algebraic Methodology and Software Technology
• Towards a Proof-Theoretic Semantics of Equalities
• Equivalence of formal semantics definition methods
• Proofs in parameterized specifications
• On Equality Predicates in Algebraic Specification Languages
• Computer Aided Verification

Cites work

• A completion procedure for conditional equations
• A generalization of the concept of sketch
• Aspects of topoi
• Category theory for computing science
• Completeness results for intuitionistic and modal logic in a categorical setting
• Conditional rewrite rules
• Generalized sketches as a framework for completeness theorems. I-III
• scientific article; zbMATH DE number 3904807 (Why is no real title available?)
• scientific article; zbMATH DE number 3959364 (Why is no real title available?)
• scientific article; zbMATH DE number 4033040 (Why is no real title available?)
• scientific article; zbMATH DE number 3656176 (Why is no real title available?)
• scientific article; zbMATH DE number 193539 (Why is no real title available?)
• scientific article; zbMATH DE number 575948 (Why is no real title available?)
• scientific article; zbMATH DE number 839556 (Why is no real title available?)
• scientific article; zbMATH DE number 918294 (Why is no real title available?)
• Left exact logic
• Orderings for term-rewriting systems

Cited in

(3)

• A decision procedure for semantical equivalence of thin FM specifications
• Relaxed models for rewriting logic
• A diagrammatic logic for object-oriented visual modeling

This page was built for publication: Proving semantical equivalence of data specifications

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