Abductive reasoning involves finding the missing premise of an “unsaturated” deductive inference, thereby selecting a possible _explanans_ for a conclusion based on a set of previously accepted premises. In this paper, we explore abductive reasoning from a structural proof-theory perspective. We present a hybrid sequent calculus for classical propositional logic that uses sequents and antisequents to define a procedure for identifying the set of analytic hypotheses that a rational agent would be expected to select as _explanans_ when presented with an (...) abductive problem. Specifically, we show that this set may not include the deductively minimal hypothesis due to the presence of redundant information. We also establish that the set of all analytic hypotheses exhausts all possible solutions to the given problem. Finally, we propose a deductive criterion for differentiating between the best _explanans_ candidates and other hypotheses. (shrink)

Traditional abduction imposes as a precondition the restriction that the background information may not derive the goal data. In first-order logic such precondition is, in general, undecidable. To avoid such problem, we present a first-order cut-based abduction method, which has KE-tableaux as its underlying inference system. This inference system allows for the automation of non-analytic proofs in a tableau setting, which permits a generalization of traditional abduction that avoids the undecidable precondition problem. After demonstrating the correctness of the method, we (...) show how this method can be dynamically iterated in a process that leads to the construction of non-analytic first-order proofs and, in some terminating cases, to refutations as well. (shrink)

Logic has its roots in the study of valid argument, but while traditional logicians worked with natural language directly, modern approaches first translate natural arguments into an artificial language. The reason for this step is that some artificial languages now have very well developed inferential systems. There is no doubt that this is a great advantage in general, but for the study of natural reasoning it is a drawback that the original linguistic forms get lost in translation. An alternative approach (...) would be to develop a general theory of the natural logic behind human reasoning and human information processing by studying formal logics that operate directly on linguistic representations. That this is possible we will try to make plausible in this paper. It will turn out that one level of representation, that of Logical Form, can meaningfully be identified with the language of an existing and well-understood logic, a restricted form of the theory of types. It is not difficult to devise inference systems for this language, and it is thus possible to study reasoning systems that are based directly on language. (shrink)