Higher-order logic and theorem proving for structured specifications

DOI10.1007/978-3-540-44616-3_23MaRDI QIDQ2722041zbMATH OpenFDO

Authors Tomasz Borzyszkowski

Publication date 11 July 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-44616-3_23

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Abstract data types; algebraic specification (68Q65)

Recommendations

• Logical systems for structured specifications.
• Inductive datatypes in HOL -- lessons learned in formal-logic engineering
• Higher-order equational logic for specification, simulation and testing
• Isabelle/HOL. A proof assistant for higher-order logic
• scientific article; zbMATH DE number 234014

Cited in

(11)

• Carnap, Goguen, and the hyperontologies: logical pluralism and heterogeneous structuring in ontology design
• Ultraproducts and possible worlds semantics in institutions
• Stratified institutions and elementary homomorphisms
• Twenty Years of Theorem Proving for HOLs Past, Present and Future
• Higher-order equational logic for specification, simulation and testing
• Algebraic Methodology and Software Technology
• Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic
• Using lattice theory in higher order logic
• Categorical foundations for structured specifications in \(\mathsf{Z}\)
• The higher-order-logic Formath
• Saturated models in institutions

Describes a project that uses

Uses Software

• ETPS
• Isabelle
• CASL

This page was built for publication: Higher-order logic and theorem proving for structured specifications

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