Theorem Proving in Higher Order Logics

DOI10.1007/11541868MaRDI QIDQ5477666zbMATH OpenOpenAlexFDO

Authors Thomas Tuerk, Klaus Schneider

Publication date 6 July 2006

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11541868

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 1424021
• Executing the formal semantics of the Accellera property specification language by mechanised theorem proving
• Verifying the LTL to Büchi automata translation via very weak alternating automata
• Validating the PSL/Sugar semantics using automated reasoning
• Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL

Cited in

(6)

• Improving translation of live sequence charts to temporal logic
• From Church and Prior to PSL
• scientific article; zbMATH DE number 1424021 (Why is no real title available?)
• From Monadic Logic to PSL
• Executing the formal semantics of the Accellera property specification language by mechanised theorem proving
• Validating the PSL/Sugar semantics using automated reasoning

Describes a project that uses

Uses Software

• HOL
• LTL2BA

This page was built for publication: Theorem Proving in Higher Order Logics

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