×

The practicality of generating semantic trees for proofs of unsatisfiability. (English) Zbl 1001.68513


MSC:

68Q25 Analysis of algorithms and problem complexity
68Q55 Semantics in the theory of computing
68R10 Graph theory (including graph drawing) in computer science

Software:

TGTP; SETHEO
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] DOI: 10.1016/0004-3702(71)90004-X · Zbl 0221.68052 · doi:10.1016/0004-3702(71)90004-X
[2] Chang C. L., Symbolic Logic and Mechanical Theorem Proving (1973) · Zbl 0263.68046
[3] Chang C. L., Theorem proving by generation of pseudo-semantic trees, Div. of Comput. Res. and TechnoL, Nat. Inst, of Health (1971)
[4] Hsiang J., Journal of the Assoc, for Computing Machinery 38 pp 559– (1991)
[5] Kowalski R., Machine Intelligence 5 pp 87– (1970)
[6] Kowalski R., Machine Intelligence 4 pp 87– (1969)
[7] Letz R., Journal of Automated ReasoningrH 4 pp 183– (1992)
[8] Loveland D. W., Automated Theorem Proving: A lagical Basis 6 (1978) · Zbl 0364.68082
[9] Manna Z., Mathematical Theory of Computation (1974) · Zbl 0353.68066
[10] Newborn M., The Great Theorem Prover Version 2, Newborn Software (1994)
[11] Nilsson N. J., Problem-Solving Methods in Artificial Intelligence (1971)
[12] DOI: 10.1016/0004-3702(71)90013-0 · Zbl 0234.68035 · doi:10.1016/0004-3702(71)90013-0
[13] DOI: 10.1145/321250.321253 · Zbl 0139.12303 · doi:10.1145/321250.321253
[14] Sikloosy L. Marinov V.Heuristic search vs. exhaustive search, Proc. 2nd International Conference on Artificial IntelligenceLondon1971 601 607
[15] Slagle J. R., Comm. Assoc, for Computing Machinery 14 pp 91– (1971)
[16] Slagle J. R., for Computing Machinery 14 pp 687– (1967)
[17] Stickel M. E., Set Theorey And Logic (1963)
[18] Stoll R., Set Theorey And Logic (1963)
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.