On mechanizing proofs within a complete proof system for Unity

DOI10.1007/3-540-60043-4_67MaRDI QIDQ5096400zbMATH OpenOpenAlexFDO

Authors Naïma Brown, Abdelillah Mokkedem

Publication date 16 August 2022

Published in Algebraic Methodology and Software Technology (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-60043-4_67

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Eliminating the substitution axiom from UNITY logic
• scientific article; zbMATH DE number 2077135
• Models for the substitution axiom of UNITY logic
• Mechanizing UNITY in Isabelle
• A simple proof of a completeness result for \(leads\)-\(to\) in the UNITY logic

Cites work

• Eliminating the substitution axiom from UNITY logic
• scientific article; zbMATH DE number 50008 (Why is no real title available?)
• scientific article; zbMATH DE number 52331 (Why is no real title available?)
• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• scientific article; zbMATH DE number 194642 (Why is no real title available?)
• On the completeness of modular proof systems
• Proving Liveness Properties of Concurrent Programs
• Soundness and Completeness of an Axiom System for Program Verification
• The \({\mathcal NU}\) system as a development system for concurrent programs: \(\delta{\mathcal NU}\)

Cited in

(5)

• Models for the substitution axiom of UNITY logic
• scientific article; zbMATH DE number 2077135 (Why is no real title available?)
• Mechanical Reasoning about Families of UTP Theories
• A modular coding of \textsc{Unity} in \textsc{Coq}
• Eliminating the substitution axiom from UNITY logic

This page was built for publication: On mechanizing proofs within a complete proof system for Unity

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