Theorem Proving in Higher Order Logics

DOI10.1007/11541868zbMATH Open1152.68536OpenAlexW2484880499MaRDI QIDQ5477666FDOQ5477666

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

Recommendations

• Publication:4945211
• 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

Mathematics Subject Classification ID

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

Cited In (5)

• Title not available (Why is that?)
• Validating the PSL/Sugar semantics using automated reasoning
• From Church and Prior to PSL
• From Monadic Logic to PSL
• Executing the formal semantics of the Accellera property specification language by mechanised theorem proving

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)