Conference publications

Abstracts

XX conference

Applicative approach for automatic theorem proving

Mazhirin I.V.

KIFF, Russia, 121151, Moscow, Kutuzovsky Ave. 24/1, +74957291442, allo10@yandex.ru

It is known that in 50 years of development of the automatic theorem proving and a logic conclusion two main systems settled:

- denial system on the basis of resolutions;

- system of deductions on the basis of rules (direct, reverse or the mixed).

There were rather exact transformation rules of expressions in language of Predicate Calculus of First Order (PCFO) in a so-called Conjunctive Normal Form (CNF).

Finally for the above-stated purposes character processing of disjuncts in CNF and logical sheaves with substitution and unification of values of variables by different programming languages on the basis of traditional architecture the Von Neumann is used. That is represented not so convenient as in the course of computation any arithmetical operation isn't applied.

In case of applicative approach in automatic theorem proving and a logic conclusion process of the proof is represented in the chosen combinatory basis and is reduced to production system with a set of rules and rather simple management system with possibility of addition of combinatory expressions for heuristic and weight functions with hardware support of combinatory basis. As a result the hardware-software resource isn't spent for accomplishment of elementary transaction (application). Schemers of basis it is possible to provide in a binary code in the form of a bit line. It allows to use the hardware-software computing environment existing now constructed on binary arithmetic.

Essential difference of applicative approach is active participation in process of the automatic proof of the logic sheaves provided in a combinatory type. Practically, in any programming language we can determine one team calculation of logic value of application of a logic sheaf only to two logic arguments. In case of applicative approach logic sheaves are expressed in the same combinatory basis, as arguments and quantity of logic sheaves and arguments can be more than two that leads to unification of logic transactions and essential performance improvement of calculations.

• view as PDF (in Russian) (PDF)