Complex sentence: The Barcan formula is most often used when adding quantifiers to the S5 modal logic of the Kripke system, and was first proposed by Ruth Barcan Marcus.
Split into simpler sentences: The Barcan formula is used in S5 modal logic of the Kripke system. The formula was first proposed by Ruth Barcan Marcus.