On mechanizing proofs within a complete proof system for Unity

DOI10.1007/3-540-60043-4_67zbMATH Open1496.68101OpenAlexW2123718183MaRDI QIDQ5096400FDOQ5096400

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

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

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Soundness and Completeness of an Axiom System for Program Verification
• Proving Liveness Properties of Concurrent Programs
• Title not available (Why is that?)
• Eliminating the substitution axiom from UNITY logic
• On the completeness of modular proof systems
• The \({\mathcal NU}\) system as a development system for concurrent programs: \(\delta{\mathcal NU}\)

Cited In (4)

• Models for the substitution axiom of UNITY logic
• Title not available (Why is that?)
• Mechanical Reasoning about Families of UTP Theories
• 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)