Search

Enrico Bombieri proved that the ABC Conjecture implies Roth's theorem in 1994. This paper concerns the other direction. In making use of Bombieri's and Van der Poorten's explicit formula for the coefficients of the regular continued fractions of algebraic numbers, we prove that Roth's theorem implies a weakened non-effective version of the ABC Conjecture in certain cases relating to roots.

This paper describes a decision procedure for disjunctions of conjunctions of anti-prenex normal forms of pure first-order logic (FOLDNFs) that do not contain $\vee$ within the scope of quantifiers. The disjuncts of these FOLDNFs are equivalent to prenex normal forms whose quantifier-free parts are conjunctions of atomic and negated atomic formulae (= Herbrand formulae). In contrast to the usual algorithms for Herbrand formulae, neither skolemization nor unification algorithms with function symbols are applied. Instead, a procedure is described that rests on nothing but equivalence transformations within pure first-order logic (FOL). This procedure involves the application of a calculus for negative normal forms (the NNF-calculus) with $A \dashv\vdash A \wedge A$ (= $\wedge$I) as the sole rule that increases the complexity of given FOLDNFs. The described algorithm illustrates how, in the case of Herbrand formulae, decision problems can be solved through a systematic search for proofs that reduce the number of applications of the rule $\wedge$I to a minimum in the NNF-calculus. In the case of Herbrand formulae, it is even possible to entirely abstain from applying $\wedge$I. Finally, it is shown how the described procedure can be used within an optimized general search for proofs of contradiction and what kind of questions arise for a $\wedge$I-minimal proof strategy in the case of a general search for proofs of contradiction., Comment: 30 pages, 2 figures