Non-resolutional Formulae Derivation in Axiomatic Predicate Calculus.

Yu. Orekhov, A. Schwab: Non-resolutional Formulae Derivation in Axiomatic Predicate Calculus CSIT 1999 : E/E

Abstract

In this article we propose a new technique of formulas derivation in axiomatic predicate calculus (APC). The designed technique is non-resolutional, so it allows us to make inferences of formulas of any type and get these inferences in the type accustomed for APC. The technique has great possibilities of heuristic restriction of looking over the variants. The method is based on the introduced notion of formula's "tail". Formal, theoretical foundation of the method consists in formulated and proven theorems which are provided in the article. In addition, a proof algorithm scheme is described in the article and an example of formula derivation according to this scheme is given.

Copyright © 1999 by the Institute for Contemporary Education "JurInfoR-MSU". Permission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage, the CSIT copyright notice and the title of the publication and its date appear, and notice is given that copying is by permission of the Institute for Contemporary Education JMSUICE. To copy otherwise, or to republish, requires a fee and/or special permission from the JMSUICE.

Printed Edition

Ch. Freytag and V. Wolfengagen (Eds.): CSIT'99, Proceedings of 1st International Workshop on Computer Science and Information Technologies, January 18-22, 1999, Moscow, Russia. MEPhI Publishing 1999, ISBN 5-7262-0263-5

Electronic Edition