Volozh, B. B.; Matskin, M. B.; Mints, G. E.; Tyugu, Eh. Kh. 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. Cited in 3 Documents 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 Keywords:intuitionistic propositional calculus; logical connectives; deductions of intuitionistically deducible propositional formulas Citations:Zbl 0047.007 PDFBibTeX XMLCite \textit{B. B. Volozh} et al., Cybernetics 18, 777--788 (1983; Zbl 0533.68072); translation from Kibernetika 1982, No. 6, 63--70 (1982) 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.