We present some new decision and comparison problems of unusually high computational complexity. Most of the problems are strictly combinatorial in nature; others involve basic logical notions. Their complexities range from iterated exponential time completeness to (0 time completeness to ((((,0) time completeness to ((((,,0) time completeness. These three ordinals are well known ordinals from proof theory, and their associated com- plexity classes represent new levels of computational complexity for natural decision problems. Proofs will appear in an (...) extended version of this manuscript to be published elsewhere. (shrink)

The “wisdom of the crowd” phenomenon refers to the finding that the aggregate of a set of proposed solutions from a group of individuals performs better than the majority of individual solutions. Most often, wisdom of the crowd effects have been investigated for problems that require single numerical estimates. We investigate whether the effect can also be observed for problems where the answer requires the coordination of multiple pieces of information. We focus on combinatorial problems such as the planar (...) Euclidean traveling salesperson problem, minimum spanning tree problem, and a spanning tree memory task. We develop aggregation methods that combine common solution fragments into a global solution and demonstrate that these aggregate solutions outperform the majority of individual solutions. These case studies suggest that the wisdom of the crowd phenomenon might be broadly applicable to problem-solving and decision-making situations that go beyond the estimation of single numbers. (shrink)

In this paper we define the concept of a system function language which is a language generated by a system function. We identify system function languages with recursively enumerable sets which are non-simple and co-infinite. We then define restricted system function languages and identify them with recursive sets which are co-infinite. Finally we state and prove some independence and dependence relationships between system function languages and some of the more well-known decision problems. MSC: 03D05, 03D20, 03D25.

Some investigations into the algebraic constructive aspects of a decision procedure for various fragments of Relevant Logics are presented. Decidability of these fragments relies on S. Kripke's gentzenizations and on his combinatorial lemma known as Kripke's lemma that B. Meyer has shown equivalent to Dickson's lemma in number theory and to his own infinite divisor lemma, henceforth, Meyer's lemma or IDP. These investigations of the constructive aspects of the Kripke's-Meyer's decision procedure originate in the development of Paul (...) Thistlewaite's “Kripke” theorem prover that had been devised to tackle the decision problem of the Relevant Logic R. A. Urquhart's pen and paper solution that relies on a sophisticated algebraic and geometric treatment of the problem shows the usefulness of an algebraic approach in Logic. Here, the study of the constructive aspects of the Kripke-Meyer decision procedure relies on various algebraic constructive results in the theory of polynomials rings. (shrink)

We consider scenarios with distributed decision processes, e.g., coupled majorities and personal union in parliament chambers, supranational decisions and supervisory boards. When computing the adoption rate for reaching a decision in these scenarios, multiple linear inequality restrictions in combinatorial countings are present. These rates cannot be computed in closed form. We introduce a general method for incorporating multiple inequality conditions in multiple majority decisions, which significantly reduces the number of involved summations and removes restrictions on the summation (...) indices. Exact solutions are provided through integral representations which can be evaluated numerically, and unrestricted, contracted sums over discrete events. Further, we provide methods to reduce the number of necessary summations by splitting or recurring the original problem to easier sub-problems. For five dedicated scenarios, full results are given which indeed require a single unrestricted summation only. (shrink)

The decision problem for provability logic remains PSPACE-complete even if the number of propositional atoms is restricted to one.

The still unsettled decision problem for the restricted purely universal formulae 0-formulae) of the first order set-theoretic language based over =, ∈ is discussed in relation with the adoption or rejection of the axiom of foundation. Assuming the axiom of foundation, the related finite set-satisfiability problem for the very significant subclass of the 0-formulae consisting of the formulae involving only nested variables of level 1 is proved to be semidecidable on the ground of a reflection property over (...) the hereditarily finite sets, and various extensions of this result are obtained. When variables are restricted to range only over sets, in universes with infinitely many urelements the set-satisfiability problem is shown to be solvable provided the axiom of foundation is assumed; if it is not, then the decidability of a related derivability problem still holds. That, in turn, suggests the alternative adoption of an antifoundation axiom under which the set-satisfiability problem is also solvable . Turning to set theory without urelements, assuming a form of Boffa's antifoundation axiom, the complement of the set-satisfiability problem for the full class of Δ0-formulae is shown to be semidecidable; a result that is known not to hold, for the set-satisfiability problem itself, even for a very restricted subclass of the Δ0-formulae. (shrink)

The “somewhat vague, intuitive” notion from computability theory of an effective procedure (method) or algorithm can be fairly precisely defined even if it is not sufficiently formal and precise to belong to mathematics proper (in a narrow sense)—and even if (as many have asserted) for that reason the Church–Turing thesis is unprovable. It is proved logically that the class of effective procedures is not decidable, i.e., that no effective procedure is possible for ascertaining whether a given procedure is effective. This (...) undecidability result is proved directly from the notion itself of an effective procedure, without reliance on any (partly) mathematical lemma, conjecture, or thesis invoking recursiveness or Turing-computability. In fact, there is no reliance on anything very mathematical. The proof does not even appeal to a precise definition of ‘effective procedure’. Instead, it relies solely and entirely on a basic grasp of the intuitive notion of an effective procedure. Though the result that effectiveness is undecidable is not surprising, it is also not without significance. It has the consequence, for example, that the solution to a decision problem, if it is to be complete, must be accompanied by a separate argument that the proposed ascertainment procedure invariably terminates with the correct verdict. (shrink)

We focus on two formal methods contexts which generate investigations into decision problems for finite strings.

This work presents a systematic study of decision problems for equational theories of algebras of binary relations (relation algebras). For example, an easily applicable but deep method, based on von Neumann's coordinatization theorem, is developed for establishing undecidability results. The method is used to solve several outstanding problems posed by Tarski. In addition, the complexity of intervals of equational theories of relation algebras with respect to questions of decidability is investigated. Using ideas that go back to Jonsson and Lyndon, (...) the authors show that such intervals can have the same complexity as the lattice of subsets of the set of the natural numbers. Finally, some new and quite interesting examples of decidable equational theories are given. The methods developed in the monograph show promise of broad applicability. They provide researchers in algebra and logic with a new arsenal of techniques for resolving decision questions in various domains of algebraic logic. (shrink)

In this paper, we are concerned with the arithmetical definability of certain notions of integers and rationals in terms of other notions. The results derived will be applied to obtain a negative solution of corresponding decision problems.In Section 1, we show that addition of positive integers can be defined arithmetically in terms of multiplication and the unary operation of successorS(whereSa=a+ 1). Also, it is shown that both addition and multiplication can be defined arithmetically in terms of successor and the (...) relation of divisibility | (wherex|ymeansxdividesy). (shrink)

Linear logic, introduced by Girard, is a refinement of classical logic with a natural, intrinsic accounting of resources. This accounting is made possible by removing the ‘structural’ rules of contraction and weakening, adding a modal operator and adding finer versions of the propositional connectives. Linear logic has fundamental logical interest and applications to computer science, particularly to Petri nets, concurrency, storage allocation, garbage collection and the control structure of logic programs. In addition, there is a direct correspondence between polynomial-time computation (...) and proof normalization in a bounded form of linear logic. In this paper we show that unlike most other propositional logics, full propositional linear logic is undecidable. Further, we prove that without the modal storage operator, which indicates unboundedness of resources, the decision problem becomes PSPACE-complete. We also establish membership in NP for the multiplicative fragment, NP-completeness for the multiplicative fragment extended with unrestricted weakening, and undecidability for fragments of noncommutative propositional linear logic. (shrink)

We argue that in extensive decision problems (extensive games with a single player) with imperfect recall care must be taken in interpreting information sets and strategies. Alternative interpretations allow for different kinds of analysis. We address the following issues: 1. randomization at information sets; 2. consistent beliefs; 3. time consistency of optimal plans; 4. the multiselves approach to decision making. We illustrate our discussion through an example that we call the ‘‘paradox of the absentminded driver.’’ Journal of Economic (...) Literature Classification Numbers: C7, D0. 1997 Academic Press. (shrink)

This book offers a comprehensive treatment of the classical decision problem of mathematical logic and of the role of the classical decision problem in modern computer science. The text presents a revealing analysis of the natural order of decidable and undecidable cases and includes a number of simple proofs and exercises.

We show the algorithmic unsolvability of a number of decision procedures in ordinary two dimensional Euclidean geometry, involving lines and integer points. We also consider formulations involving integral domains of characteristic 0, and ordered rings. The main tool is the solution to Hilbert's Tenth Problem. The limited number of facts used from recursion theory are isolated at the beginning.

We show undecidability for lattices over a group ring ${\vec Z} \, G$ where $G$ has a cyclic subgroup of order $p^3$ for some odd prime $p$ . Then we discuss the decision problem for ${\vec Z} \, G$ -lattices where $G$ is a cyclic group of order 8, and we point out that a positive answer implies – in some sense – the solution of the “wild $\Leftrightarrow$ undecidable” conjecture.

In the propositional modal treatment of two-variable first-order logic equality is modelled by a ‘diagonal’ constant, interpreted in square products of universal frames as the identity relation. Here we study the decision problem of products of two arbitrary modal logics equipped with such a diagonal. As the presence or absence of equality in two-variable first-order logic does not influence the complexity of its satisfiability problem, one might expect that adding a diagonal to product logics in general is (...) similarly harmless. We show that this is far from being the case, and there can be quite a big jump in complexity, even from decidable to the highly undecidable. Our undecidable logics can also be viewed as new fragments of first-order logic where adding equality changes a decidable fragment to undecidable. We prove our results by a novel application of counter machine problems. While our formalism apparently cannot force reliable counter machine computations directly, the presence of a unique diagonal in the models makes it possible to encode both lossy and insertion-error computations, for the same sequence of instructions. We show that, given such a pair of faulty computations, it is then possible to reconstruct a reliable run from them. (shrink)

In this paper I study two ways of transforming decision problems on the basis of previously adopted intentions, ruling out incompatible options and imposing a standard of relevance, with a particular focus on situations of strategic interaction. I show that in such situations problems arise which do not appear in the single-agent case, namely that transformation of decision problems can leave the agents with no option compatible with what they intend. I characterize conditions on the agents’ intentions which (...) avoid such problematic scenarios, in a way that requires each agent to take account of the intentions of others. (shrink)

We make use of a Theorem of Burris-McKenzie to prove that the only decidable variety of diagonalizable algebras is that defined by 0=1. Any variety containing an algebra in which 01 is hereditarily undecidable. Moreover, any variety of intuitionistic diagonalizable algebras is undecidable.

I argue that medieval solutions to the limit decision problem imply four-dimensionalism, i.e. the view according to which substances that persist through time are extended through time as well as through space, and have different temporal parts at different times.

Why do we ask questions? Because we want tohave some information. But why this particular kind ofinformation? Because only information of this particularkind is helpful to resolve the decision problemthat the agent faces. In this paper I argue thatquestions are asked because their answers help toresolve the questioner's decision problem, and that thisassumption helps us to interpret interrogativesentences. Interrogative sentences are claimed to have asemantically underspecified meaning and thisunderspecification is resolved by means of the decisionproblem.

The problem of combinatorial optimization is considered in relation to the choice of the location of the location of power supplies when solving the problem of the development of urban distribution networks of power supply. Two methods have been developed for placing power supplies and assigning consumers to them to solve this problem. The first developed method consists in placing power supplies of the same standard sizes, and the second - of different standard sizes. The fundamental (...) difference between the created methods and the existing ones is that the proposed methods take into account all the material of the problem and have specialized methods for coding possible solutions, modified operators of crossing and selection. The proposed methods effectively solve the problem of low inheritance, topological unfeasibility of the found solutions, as a result of which the execution time is significantly reduced and the accuracy of calculations is increased. In the developed methods, the lack of taking into account the restrictions on the placement of new power supplies is realized, which made it possible to solve the problem of applying the methods for a narrow range of problems. A comparative analysis of the results obtained by placing power supplies of the same standard sizes and known methods was carried out, and it was found that the developed method works faster than the known methods. It is shown that the proposed approach ensures stable convergence of the search process by an acceptable number of steps without artificial limitation of the search space and the use of additional expert information on the feasibility of possible solutions. The results obtained allow us to propose effective methods to improve the quality of decisions made on the choice of the location of power supply facilities in the design of urban electrical. (shrink)

The paper deals with multiple decision problems, which are similar to the task of guessing the color outcomes of five independent spinnings of a roulette wheel, 60% of whose slots are red and 40% white. Each correct guess yields a prize of $1. The guess of 5 Reds clearly first order stochastic dominates any other strategy. In contrast, subjects diversify their choices when facing a multiple decision problem in which the choice is between lotteries with clear objective (...) probabilities. The diversification is stronger when the subjects face uncertainty without objective probabilities and weaker when the choice problem involves real life actions. c 2002 Elsevier Science B.V. All rights reserved. (shrink)

This paper is an examination of some modelling problems regarding imperfect recall within the model of extensive games. It is argued that, if the assumption of perfect recall is violated, care must be taken in interpreting the main elements of the model. Interpretations that are inconsequential under perfect recall have important implications in the analysis of games with imperfect recall.

We identify the computational complexity of the satisfiability problem for FO 2 , the fragment of first-order logic consisting of all relational first-order sentences with at most two distinct variables. Although this fragment was shown to be decidable a long time ago, the computational complexity of its decision problem has not been pinpointed so far. In 1975 Mortimer proved that FO 2 has the finite-model property, which means that if an FO 2 -sentence is satisfiable, then it (...) has a finite model. Moreover, Mortimer showed that every satisfiable FO 2 -sentence has a model whose size is at most doubly exponential in the size of the sentence. In this paper, we improve Mortimer's bound by one exponential and show that every satisfiable FO 2 -sentence has a model whose size is at most exponential in the size of the sentence. As a consequence, we establish that the satisfiability problem for FO 2 is NEXPTIME-complete. (shrink)

The theory of trees with additional unary predicates and quantification over nodes and branches embraces a rich branching time logic. This theory was reduced in the companion paper to the first-order theory of binary, bounded, well-founded trees with additional unary predicates. Here we prove the decidability of the latter theory.

Contact Logics provide a natural framework for representing and reasoning about regions in several areas of computer science. In this paper, we focus our attention on reasoning methods for Contact Logics and address the satisfiability problem and the unifiability problem. Firstly, we give sound and complete tableaux-based decision procedures in Contact Logics and we obtain new results about the decidability/complexity of the satisfiability problem in these logics. Secondly, we address the computability of the unifiability problem (...) in Contact Logics and we obtain new results about the unification type of the unifiability problem in these logics. (shrink)

Many collective decision making problems have a combinatorial structure: the agents involved must decide on multiple issues and their preferences over one issue may depend on the choices adopted for some of the others. Voting is an attractive method for making collective decisions, but conducting a multi-issue election is challenging. On the one hand, requiring agents to vote by expressing their preferences over all combinations of issues is computationally infeasible; on the other, decomposing the problem into several (...) elections on smaller sets of issues can lead to paradoxical outcomes. Any pragmatic method for running a multi-issue election will have to balance these two concerns. We identify and analyse the problem of generating an agenda for a given election, specifying which issues to vote on together in local elections and in which order to schedule those local elections. (shrink)