zbMATH — the first resource for mathematics

Two systems for proving tautologies, based on the split method. (English) Zbl 0509.03004

03B05 Classical propositional logic
03D15 Complexity of computation (including implicit computational complexity)
03F20 Complexity of proofs
Full Text: DOI
[1] A. Aho, J. Hopcroft and J. Ullman, The Design and Analysis of Computer Algorithms (1976). · Zbl 0326.68005
[2] E. Ya. Dantsin, ?Parameters defining recognition time for tautologies by the split method,? Semiotika Inf. (Moskva),12, 8?17 (1979).
[3] Z. Galil, ?On enumeration procedures for theorem proving and for integer programming,? in: Automat Languages and Programming, 335?381 (1976). · Zbl 0358.68132
[4] S. Yu. Maslov, ?The theory of deduction search and some of its applications,? Kibernetika, No. 4 (1975).
[5] G. S. Tseitin, ?The complexity of deduction in a propositional calculus,? Zap. Nauchn. Sem. Leningr. Otd. Mat. Inst. Akad. Nauk SSSR,8, 234?259 (1968).
[6] S. A. Cook, ?A short proof of the pigeonhole principle using extended resolution,? SIGACT News,8, No. 4, 28?32 (1976).
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.