The Logic of U ·(TP)2

DOI10.1007/978-3-642-35705-3_6zbMath1452.68261OpenAlexW2205741543MaRDI QIDQ3455647

Andrew Butterfield

Publication date: 11 December 2015

Published in: Unifying Theories of Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-35705-3_6

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (7)

An Axiomatic Value Model for Isabelle/UTP ⋮ UTPCalc — A Calculator for UTP Predicates ⋮ Angelic processes for CSP via the UTP ⋮ The geometry of reduction: compound reduction and overlapping state space domains ⋮ Isabelle/UTP: A Mechanised Theory Engineering Framework ⋮ UTP2 ⋮ The interpretation of string-theoretic dualities

Uses Software

• Coq
• Isabelle/HOL
• PVS
• ProofPower
• Saoithin
• Isabelle/Circus

Cites Work

• A UTP semantics for \textsf{Circus}
• Isabelle/HOL. A proof assistant for higher-order logic
• On the Soundness and Completeness of Equational Predicate Logics
• Saoithín: A Theorem Prover for UTP
• Unifying Theories in Isabelle/HOL
• Encoding Circus Programs in ProofPowerZ
• Unifying Theories in ProofPower-Z

This page was built for publication: The Logic of U ·(TP)2