On mechanizing proofs within a complete proof system for Unity
DOI10.1007/3-540-60043-4_67zbMath1496.68101OpenAlexW2123718183MaRDI QIDQ5096400
Abdelillah Mokkedem, Naïma Brown
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
Logic in computer science (03B70) 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) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formalization of mathematics in connection with theorem provers (68V20)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- 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}\)
- Proving Liveness Properties of Concurrent Programs
- Soundness and Completeness of an Axiom System for Program Verification
This page was built for publication: On mechanizing proofs within a complete proof system for Unity
