A Sequent Calculus for First-Order Dynamic Logic with Trace Modalities

The modalities of Dynamic Logic refer to the final state of a program execution and allow to specify programs with pre- and postconditions. In this paper, we extend Dynamic Logic with additional trace modalities "throughout" and "at least once", which refer to all the states a program reaches. They allow one to specify and verify invariants and safety constraints that have to be valid throughout the execution of a program. We give a sound and (relatively) complete sequent calculus for this extended Dynamic Logic.

• Type: Conference
• Year: 2001
• Where: CADE
• Authors: Bernhard Beckert, Steffen Schlager
• Keywords: Additional Trace Modalities, Automated Reasoning, CADE 2001, Complete Sequent Calculus, Dynamic Logic