Combining WS1S and HOL

MaRDI QIDQ2782479zbMATH OpenFDO

Authors Stefan Friedrich, David Basin

Publication date 22 July 2002

zbMATH Keywords

combination of logicsdecision procedurehigher-order logictheorem provingweak monadic second-order logic of one successor

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 1841832
• Combining logic programs and monadic second order logics by program transformation
• scientific article; zbMATH DE number 1773084
• A comprehensive combination framework
• Deciding Combinations of Theories

Cited in

(6)

• Integrating external deduction tools with ACL2
• Formalizing the Logic-Automaton Connection
• Linear Arithmetic with Stars
• Combining theories with shared set operations
• Verified decision procedures for MSO on words based on derivatives of regular expressions
• Verifying a signature architecture: a comparative case study

This page was built for publication: Combining WS1S and HOL

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