Almulla, Mohammed; Newborn, Monroe The practicality of generating semantic trees for proofs of unsatisfiability. (English) Zbl 1001.68513 Int. J. Comput. Math. 62, No. 1-2, 45-61 (1996). Cited in 2 Documents MSC: 68Q25 Analysis of algorithms and problem complexity 68Q55 Semantics in the theory of computing 68R10 Graph theory (including graph drawing) in computer science Keywords:Herbrand universe; Herbrand base; unsatisfiability; Herbrand interpretation; Herbrand procedure; semantic trees Software:TGTP; SETHEO PDFBibTeX XMLCite \textit{M. Almulla} and \textit{M. Newborn}, Int. J. Comput. Math. 62, No. 1--2, 45--61 (1996; Zbl 1001.68513) 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.