Combining WS1S and HOL.
David Basin · 1998
We investigate the combination of the weak second-order monadic logic of one successor (WS1S) with higher-order logic (HOL). We show how these two logics can be combined, how theorem provers based on them can be safely integrated, and how the result can be used. In particular, we present an embedding of the semantics of WS1S in HOL that provides a basis for coupling the MONA system, a decision procedure for WS1S, with an implementation of HOL in the Isabelle system. Afterwards, we describe methods that reduce problems formalized in HOL to problems in the language of WS1S. We present applications to arithmetic reasoning and proving properties of parameterized sequential systems. 1 Introduction We investigate the combination of two logics and the integration of two powerful and complementary theorem proving systems for these logics: ffl a decision procedure for WS1S (the weak monadic second-order logic of one successor) implemented in the MONA system, and ffl an implementation of HOL...