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

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) 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

• 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?)
• Eliminating the substitution axiom from UNITY logic
• 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)

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

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)