A new use of an automated reasoning assistant: Open questions in equivalential calculus an the study of infinite domains (Q759491)

This article is dedicated to an application of the program AURA, which gives the solution of previously unsolved questions in the equivalential calculus EC [\textit{J. A. Kalman}, J. Lond. Math. Soc., II. Ser. 14, 193- 199 (1976; Zbl 0353.02004)]. AURA, developed by the Wos-group in Argonne Illinois, is an automated reasoning program for interactive use. The problem studied here is the shortest single axiom property of some formulas in EC. By applying the program to formulas of EC, the user can state conjectures about some formal properties, investigating the output of the program. One such conjecture is the ever-increasing length conjecture of deducible formulas; if it holds to be true, it may be applied in order to prove, that some true formulas (for example E(X,X)) are not derivable from the single axiom by condensed detachement. The authors succeeded not only in finding shorter proofs for already known theorems, but also to settle some unsolved questions in EC (questions about the single-axiom status of some formulas in EC). Demodulation is applied to analyze schemata of EC-formulas (instead of formulas themselves). New concepts as containment sets and unification sets of formulas are introduced, which proved to be very powerful for the solution of the problems mentioned above.