Using PVS for Interval Temporal Logic proofs, part 1: The syntactic and semantic encoding

De Montfort University Open Research Archive

Show simple item record

dc.contributor.author Cau, A. (Antonio)
dc.contributor.author Moszkowski, B. C.
dc.date.accessioned 2005-05-23T20:41:26Z
dc.date.available 2005-05-23T20:41:26Z
dc.date.created 2005-05-12
dc.date.issued 2005-05-23T20:41:26Z
dc.identifier.uri http://hdl.handle.net/2086/8
dc.description.abstract Interval temporal logic (ITL) is a logic that is used to specify and reason about systems. The logic has a powerful proof system but rather than doing proofs by hand, which is tedious and error prone, we want a tool that can check each proof step. Instead of developing a new tool we will use the existing prototype verification system (PVS) as a basic tool. The specification language of PVS is used to encode interval temporal logic semantically and syntactically. With this we can encode the ITL proof system within PVS. Several examples of proofs in ITL that are done per hand are checked with PVS. en
dc.description.sponsorship Funded by EPSRC Research Grant GR/K25922 en
dc.format.extent 81097 bytes
dc.format.mimetype application/pdf
dc.language.iso en en
dc.relation.ispartofseries STRL internal monograph en
dc.subject interval temporal logic en
dc.subject tempura
dc.subject.lcsh Proof theory
dc.title Using PVS for Interval Temporal Logic proofs, part 1: The syntactic and semantic encoding en
dc.type Technical Report en
dc.researchgroup Software Technology Research Laboratory (STRL)


Files in this item

This item appears in the following Collection(s)

Show simple item record