{'fraction_non_alphanumeric': 0.029442148760330578, 'fraction_numerical': 0.01859504132231405, 'mean_word_length': 4.799401197604791, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Towards a Logical Analysis of Adjusted Winner Extended

It is often convenient to view a computational procedure, or a program, as a relation on a set of states, where a state can be thought of as a function that assigns a value to every possible variable and a truth value to all propositions. This idea was proposed by Pratt (Pratt 1976) and extends the work of of Floyd (Floyd 1967) and Hoare (Hoare 1969). Harel, Kozen and Tiuryn ((Harel, Kozen, and Tiuryn 2000)) provide a very thorough discussion of computational procedures from this point of view. In (Parikh 1995), Parikh suggests that a similar framework can be developed for studying social procedures, such as fair division algorithms or voting protocols. In fact, the first example of such an analysis can be found in an earlier paper of Parikh (Parikh 1985). In (Parikh 1985), a PDL-style logic, called game logic, is developed for reasoning about multi-agent strategic situations. It is then used to show that the BanachKnaster last diminisher procedure to fairly divide a cake is “correct”. Here “correct” means that each agent has a strategy to ensure that it receives a piece of the cake that is fair from its point of view. See (Parikh 1985; Pauly and Parikh 2003) for a discussion of this result and the current state of affairs of game logic. Recently, there have been a number of attempts to answer Parikh’s challenge to develop logical methods for studying social procedures. The different approaches can roughly be divided into two categories. The first category makes use of model checking techniques to verify that a given game-theoretic mechanism satisfies a particular specification. The idea is to draw an analogy with the formal verification of computer systems via model checking techniques where the desired specifications are expressed in some temporal logic. In the game-theoretic setting, modal strategy logics, such as alternating temporal logic (see