Narrow Results

We investigate a simple motion pursuit-evasion differential game of one Pursuer and one Evader. Maximal speeds of the players are equal. The Evader moves along a given curve without self-intersection. There is no phase constraint for the Pursuer. Necessary and sufficient conditions to complete pursuit from both fixed initial position and all initial positions are obtained.

We consider pursuit and evasion differential game problems described by an infinite system of differential equations with countably many Pursuers in Hilbert space. Integral constraints are imposed on the controls of players. In this paper an attempt has been made to solve an evasion problem under the condition that the total resource of the Pursuers is less then that of the Evader and a pursuit problem when the total resource of the Pursuers greater than that of the Evader. The strategy of the Evader is constructed.

The compensation received by economic agents reflects their performance. Usually compensation reflects performance measured cardinally, but sometimes ordinal considerations play a role. It is well established that rewards — cardinal or ordinal — can rationally motivate contestants to put forth increased effort. We ask whether rewards, and in particular their cardinal or ordinal nature, can affect agents' strategies. Specifically, if level of effort is fixed and degree of difficulty is the only choice, what strategy is optimal? For example, in a high-jump competition, level of effort is not a meaningful variable; what is of interest is the choice of strategy — the height attempted, or degree of difficulty. We study how optimal strategies reflect reward structure, assuming that rewards may depend on level of difficulty, and go only to successful candidates, or only to candidates who succeed at more difficult tasks. Basing our conclusions in part on simple probabilistic models in which optimal choices can be determined analytically, we show how the structure of competitive rewards alters contestants' rational choices. We adopt a contest-design framework: What combinations of fixed and variable prizes cause contestants to select degrees of difficulty that maximize the contest designer's expected payoff? Our general conclusion is that competition can affect strategic choices, in magnitudes and even directions that are difficult to predict.

The term automated reasoning (first introduced in 1980) accurately describes the objective of the field, the automation of logical reasoning. This article introduces scientists to the field and then briefly describes the papers found in this special issue.

When given a set of properties or conditions (say, three) that are claimed to be equivalent, the claim can be verified by supplying what we call a circle of proofs. In the case in point, one proves the second property or condition from the first, the third from the second, and the first from the third. If the proof that 1 implies 2 does not rely on 3, then we say that the proof is pure with respect to 3, or simply say the proof is pure. If one can renumber the three properties or conditions in such a way that one can find a circle of three pure proofs—technically, each proof pure with respect to the condition that is neither the hypothesis nor the conclusion—then we say that a circle of pure proofs has been found. Here we study the specific question of the existence of a circle of pure proofs for the thirteen shortest single axioms for equivalential calculus, subject to the requirement that condensed detachment be used as the rule of inference. For an indication of the difficulty of answering the question, we note that a single application of condensed detachment to the (shortest single) axiom known as P4 (also known as U M) with itself yields the (shortest single) axiom P5 (also known as X G F), and two applications of condensed detachment beginning with P5 as hypothesis yields P4. Therefore, except for P5, one cannot find a pure proof of any of the twelve shortest single axioms when using P4 as hypothesis or axiom, for the first application of condensed detachment must focus on two copies of P4, which results in the deduction of P5, forcing P5 to be present in all proofs that use P4 as the only axiom. Further, the close proximity in the proof sense of P4 when using as the only axiom P5 threatens to make impossible the discovery of a circle of pure proofs for the entire set of thirteen shortest single axioms. Perhaps more important than our study of pure proofs, and of a more general nature, we also present the methodology used to answer the cited specific question, a methodology that relies on various strategies and features offered by W. McCune's automated reasoning program OTTER The strategies and features of OTTER we discuss here offer researchers the needed power to answer deep questions and solve difficult problems. We close this article (in the last two sections) with some challenges and some topics for research and (in the Appendix) with a sample input file and some proofs for study.