Constructor-based observational logic

DOI10.1016/J.JLAP.2005.09.002zbMath1088.68112OpenAlexW2113351814MaRDI QIDQ2369030

Michel Bidoit, Rolf Hennicker

Publication date: 28 April 2006

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlap.2005.09.002

zbMATH Keywords

ObservabilityReachabilityAlgebraic specificationInstitutionProof techniques

Mathematics Subject Classification ID

Logic in computer science (03B70) Abstract data types; algebraic specification (68Q65)

Related Items (26)

Observational logic, constructor-based logic, and their duality. ⋮ Circular Coinduction: A Proof Theoretical Foundation ⋮ Constructor-Based Institutions ⋮ Quasi-Boolean encodings and conditionals in algebraic specification ⋮ Dynamic Logic with Binders and Its Application to the Development of Reactive Systems ⋮ A short overview of Hidden Logic ⋮ Foundations for structuring behavioural specifications ⋮ Coinduction for preordered algebra ⋮ Stability of termination and sufficient-completeness under pushouts via amalgamation ⋮ Refinement by Interpretation in a General Setting ⋮ Observational interpretations of hybrid dynamic logic with binders and silent transitions ⋮ Parchments for CafeOBJ Logics ⋮ An Institution for Imperative RSL Specifications ⋮ On Automation of OTS/CafeOBJ Method ⋮ Behavioral abstraction is hiding information ⋮ Object oriented institutions to specify symbolic computation systems ⋮ A logic for the stepwise development of reactive systems ⋮ Behavioural and abstractor specifications revisited ⋮ Generic constructions for behavioral specifications ⋮ Towards Behavioral Maude ⋮ The Foundational Legacy of ASL ⋮ Logical systems for structured specifications. ⋮ On institutions for modular coalgebraic specifications. ⋮ Omitting types theorem in hybrid dynamic first-order logic with rigid symbols ⋮ Logical foundations of CafeOBJ ⋮ Refinement in hybridised institutions

Uses Software

• LARCH
• PVS
• CafeOBJ

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Behavioural theories and the proof of behavioural properties
• On behavioural abstraction and behavioural satisfaction in higher-order logic
• Architectural specifications in CASL
• Institution morphisms
• On observational equivalence and algebraic specification
• Specifications in an arbitrary institution
• Context induction: A proof principle for behavioural abstractions and algebraic implementations
• Algebraic methodology and software technology. 7th international conference, AMAST '98, Amazonia, Brazil, January 4--8, 1999. Proceedings
• CASL user manual. Introduction to using the Common Algebraic Specification Language. With chapters by Till Mossakowski, Donald Sannella, and Andrzej Tarlecki. With CD-ROM.
• CASL: the Common Algebraic Specification Language.
• Logical systems for structured specifications.
• Relating CASL with other specification languages: the institution level.
• Observational logic, constructor-based logic, and their duality.
• CASL reference manual. The complete documentation of the common algebraic specification language.
• Behavioural and abstractor specifications
• Model theory for infinitary logic. Logic with countable conjunctions and finite quantifiers
• Proof of correctness of data representations
• Institutions: abstract model theory for specification and programming
• Recent Trends in Algebraic Development Techniques

This page was built for publication: Constructor-based observational logic