There is a gap between theory and practice regarding the assessment of minimaxing versus product propagation. The use of minimaxing in real programs for certain two-player games like chess is more or less ubiquitous, due to the substantial search space reductions enabled by several pruning algorithms. In stark contrast, some theoretical work supported the view that product propagation could be a viable alternative, or even superior on theoretical grounds. In fact, these rules have different conceptual problems. While minimaxing treats heuristic values as true values, product propagation interprets them as independent probabilities. So, which is the better rule for backing up heuristic values in game trees, and under which circumstances? We present a systematic analysis and results of simulation studies that compare these backup rules in synthetic trees with properties found in certain real game trees, for a variety of situations with characteristic properties. Our results show yet unobserved complementary strengths in their respective capabilities, depending on the size of node score changes (“quiet” versus “nonquiet” positions), and on the degree of advantage of any player over the opponent. In particular, exhaustive analyses for shallow depths show that product propagation can indeed be better than minimaxing when both approaches search to the same depth, especially for making decisions from a huge amount of alternatives, where deep searches are still prohibitive. However, our results also provide some justification for the more or less ubiquitous use of minimaxing in chess programs, where deep searches prevail and the pruning algorithms available for minimaxing make the difference.

The minimaxing approach to backing-up heuristic values has been very successful, e.g., in computer chess for making move decisions on the world-champion level, by employing very deep searches and effective pruning algorithms. From a theoretical point of view, however, it is not yet clear whether minimaxing or product propagation is better in terms of decision quality without deep searches. We present a systematic analysis of game trees with depth 2, where a single application of the competing back-up rules each (in a given branch from the root of the search tree) reveals their pure decision quality. Interestingly, product propagation tends to make better decisions per se more frequently, under realistic assumptions modeled after real game-playing programs. So, its decision quality may still make it a viable alternative for game trees where only shallow searches are affordable.

Deductive reasoning is an area related to argumentation where machine-based techniques, notably theorem proving, can contribute substantially to the formation of arguments. However, making use of the functionality of theorem provers for this issue is associated with a number of difficulties and, as we will demonstrate, requires considerable effort for obtaining reasonable results. Aiming at the exploitation of machine-oriented reasoning for human-adequate argumentation in a broader sense, we present our model for producing proof presentations from machine-oriented inference structures. Capabilities of the model include adaptation to human-adequate degrees of granularity and explicitness in the underlying argumentation and interactive exploration of proofs. Enhancing capabilities in all these respects, even just those we have addressed so far, does not only improve the interactive use of theorem provers, but shows they are essential ingredients to support the functionality of dialog-oriented tutorial systems in formal domains. © 2007 Wiley Periodicals, Inc. Int J Int Syst 22: 49–70, 2007.

Abstract. The capabilities of a automated theorem prover's interface are essential for the effective use of (interactive) proof systems. L Ω UI is the multi-modal interface that combines several features: a graphical display of information in a proof graph, a selective term browser with hypertext facilities, proof and proof plan presentation in natural language, and an editor for adding and maintaining the knowledge base. L Ω UI is realized in an agent-based client-server architecture and implemented in the concurrent constraint programming language Oz.

Most algorithms dedicated to the generation of referential descriptions widely suffer from a fundamental problem: they make too strong assumptions about adjacent processing components, resulting in a limited coordination with their perceptive and linguistics data, that is, the provider for object descriptors and the lexical expression by which the chosen descriptors is ultimately realized. Motivated by this deficit, we present a new algorithm that (1) allows for a widely unconstrained, incremental, and goal-driven selection of descriptors, (2) integrates linguistic constraints to ensure the expressibility of the chosen descriptors, and (3) provides means to control the appearance of the created referring expression. Hence, the main achievement of our approach lies in providing a core algorithm that makes few assumptions about other processing components and improves the flow of control between modules.

Investigation of several algorithms for computing exact minimax values of game trees (utilizing backward pruning) are discussed. The focus is on trees with an ordering similar to that actually found in game playing practice. The authors compare the algorithms using two different distributions of the static values, the uniform distribution and a distribution estimated from practical data. A systematic comparison of using aspiration windows for all of the usual minimax algorithms is presented. The effects of aspiration windows of varying size and position are analyzed. Increasing the ordering of moves to near the optimum results in unexpectedly high savings. Algorithms with linear space complexity benefit most. Although the ordering of the first move is of predominant importance, that of the remainder has only second-order effects. The use of an aspiration window not only makes alpha-beta search competitive, but there also exist dependencies of its effects on certain properties of the trees.>