Abstract Robinson’s unification algorithm can be identified as the underlying machinery of both C. Meredith’s rule D (condensed detachment) in propositional logic and of the construction of principal types in lambda calculus and combinatory logic. In combinatory logic, it also plays a crucial role in the construction of Meyer, Bunder & Powers’ Fool’s model. This paper now considers pattern matching, the unidirectional variant of unification, as a basis for logical inference, typing, and a very simple and natural model for untyped combinatory logic. An analysis of the new typing scheme will enable us to characterize a large class of terms of combinatory logic which do not change their principal type when being weakly reduced. We also consider the question whether the major or the minor premisse should be used as the fixed pattern.

Abstract In three-valued logic, the third truth-value is often interpreted as undefined. However, the value of a logical term may be well defined if its ‘history’ is taken into account. Following this approach, the analogy to the Sorites paradox meets the eye, which in turn has recently been addressed by means of a ‘Talmudic Norms’ approach. This paper thus lays bare a religious contribution to the field of many-valued logic and implements a simplified dynamic model for the theory of Talmudic mixtures—and, thus, for the outlined Sorites logic—using standard AI search and planning techniques.