In Y. Tagamlitzki's paper [4] an axiomatization for an abstract notion of segment is proposed (a somewhat more restrictive but similar axiomatization has been given earlier in [2]). The main result of [4] is a separation theorem formulated in set-theoretical terms and proved by using Zorn's Lemma. The results published in [4] have been presented earlier in a lecture course held in 1962. An intriguing logical problem arose in one of the lectures when the mentioned separation theorem has been applied to obtain a certain non-trivial corollary expressible without essential use of set-theoretical terminology. The problem was to prove this corollary in a way formalizable in the first-order predicate calculus. A proof of the indicated kind (presented in the ordinary mathematical language) was given by Ivan Prodanov shortly afterwards. In fact, Prodanov established even a stronger result, but the published version of his proof (present in [3]) is restricted to establishing only the mentioned corollary.

At the end of 1983 and the beginning of 1984 Jörg Siekmann and his group in Karlsruhe made attempts to prove the stronger Prodanov's result by using their Markgraf Karl Refutation Procedure (MKRP) [1]. Since the attempts did not succeed, the problem has been decomposed into two other ones - the first one of them was quite easy, but the second one was hard enough (the decomposition has been suggested by the present author on the basis of an analysis of a proof given by Dimiter Vakarelov). In May 1984 MKRP succeeded on both these problems.

An analysis of the solutions produced by MKRP showed that the second of them actually contains a solution of a further strengthening of the corresponding problem. This stronger variant, however, seems to be less difficult for a computer proof search. For example, we succeeded in 1998 to find a computer solution of that variant of the problem by using Prolog in an appropriate way. In the full paper we give the details concerning such an application of Prolog including the text of the corresponding Prolog program and the goal on which it has been executed (the solution has been found in about 40 minutes by a computer having a 133 Mhz CPU and running Dimiter Dobrev's freeware Strawberry Prolog). The idea of the application is to make firstly a straightforward translation of the problem into Prolog without bothering about direct usability of this translation, and then to search for a corresponding derivation in a formal system generating the minimal Herbrand model for the program. The mentioned search is done by restriction of the heights of the considered derivation trees and weakening the restriction until possibly the search succeeds (this kind of search is done by an appropriate modification of the initially constructed program).

In our opinion the above-mentioned variant of the problem could be useful for testing the capabilities of proof search computer programs.

Addendum (updated on July 7, 2015, and November 11, 2020). The run time mentioned above has been later reduced to less than 5 minutes by running Strawberry Prolog on a computer with an AMD K6-2 300 CPU. On contemporary computers, the run time under SWI Prolog is only several seconds.

REFERENCES

1. Ohlbach, H. J. and Siekmann, J. H. The Markgraf Karl Refutation Procedure. In: Computational Logic, Essays in Honor of Alan Robinson, MIT Press, 1991 (ed. J. L. Lassez and G. Plotkin), 41-112.

2. Prenowitz, W. A contemporary approach to classical geometry. Amer. Math. Monthly, 68 (1961), No. 1, part II, vi+67pp.

3. Prodanov, I. Zweifachassoziative Räume. Annuaire de l'Univ. de Sofia, Fac. de Math., 57 (1964), 393-422 (Bulgarian. German summary).

4. Tagamlitzki, Y. Über die Trennbarkeitsbedingungen in den abelschen assoziativen Räumen. Acad. des Sci. de Bulgarie, Bull. de l'Inst. de Math., 7 (1963), 169-183 (Bulgarian. Russian and German summaries).