×

The PRIZ system and propositional calculus. (English. Russian original) Zbl 0533.68072

Cybernetics 18, 777-788 (1983); translation from Kibernetika 1982, No. 6, 63-70 (1982).
Summary: In this paper we show that the design of the PRIZ system [M. I. Kakhro, A. P. Kal’ya, and E. Kh. Tyugu: The PRIZ instrumental system of computer programming (Russian) (Moskva, 1981)] contains a program of search for a deduction in intuitionistic (Heyting, or constructive) propositional calculus [S. C. Kleene: Introduction to metamathematics (1952; Zbl 0047.007)] with conjunction and implication that operates in the polynomial region (P-SPACE). A preprocessor is described that makes it possible to insert the other connectives (disjunction, negation, and equivalence), and the results of an experiment are presented during which an ES-1052 computer received the deductions of intuitionistically deducible propositional formulas from Kleene’s book mentioned above.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03F55 Intuitionistic mathematics
03-04 Software, source code, etc. for problems pertaining to mathematical logic and foundations
03B35 Mechanization of proofs and logical operations

Citations:

Zbl 0047.007
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] M. I. Kakhro, A. P. Kal’ya, and E. Kh. Tyugu, The PRIZ Instrumental System of Computer Programming [in Russian], Finansy i Statistika, Moscow (1981).
[2] S. C. Kleene, Introduction to Metamathematics, Van Nostrand, Princeton, N. J. (1952). · Zbl 0047.00703
[3] E. H. Tyugu, ?A programming system with automatic program synthesis,? Lect. Notes Comput. Sci. No. 47, 251?267 (1977). · Zbl 0353.68020 · doi:10.1007/3-540-08065-1_16
[4] I. Copy, Symbolic Logic, Macmillan, New York (1954).
[5] D. Prawitz, Natural Deduction, Aguist and Wiksell, Stockholm (1965). · Zbl 0173.00205
[6] N. N. Vorob’ev, ?A new deducibility algorithm in constructive propositional calculus,? Tr. Mat. Inst. Akad. Nauk SSSR,52, 193?226 (1958).
[7] R. A. Plyushkyavichus, ?A version of constructive propositional calculus without structural deduction rules,? Dokl. Akad. Nauk SSSR,161, No. 2, 292?295 (1965).
[8] J. B. Dennis, J. B. Fossin, and J. P. Lindermann, ?Data flow schemes,? Teor. Program-mirovaniya,2, 7?43 (1972).
[9] N. N. Nepeivoda, ?Relationship between natural deduction rules and operators of high-level algorithmic languages,? Dokl. Akad. Nauk SSSR,239, No. 3, 526?529 (1978). · Zbl 0392.68004
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.