METEOR swMATH ID: 26327 Software Authors: O. L. Astrachan; D. W. Loveland Description: METEORs: High Performance Theorem Provers using Model Elimination. It has been thought for some time that linear resolution procedures are not the best resolution formats for doing very large unguided searches such as are required for proving significant mathematical theorems. Although very efficient with storage space, the depth-first implementations that take advantage of the linearity seem to preclude use of subsumption and similar devices to reduce redundant search. However, research in logic programming has led to sophisticated architectures giving high-speed performance for Prolog, which is based on a linear input resolution procedure. In particular, the WAM architecture, due to D. H. D. Warren (see [33]) has proven very successful. This has led to renewed interest in Model Elimination (ME) ([18, 19, 20]), which is a linear input proof procedure for full first-order logic, similar to but distinct from resolution. Interest has revived because there are situations where the significantly higher inference rate may offset the removal of some redundant computations. Homepage: https://link.springer.com/chapter/10.1007/978-94-011-3488-0_2 Related Software: SETHEO; OTTER; PARTHEO; PARTHENON; RRL; TPTP; Aquarius; HARP; SATCHMO; EQP; Roo; SPASS; Peers-mcd; SPTHEO; HERBY; Bliksem; DISCOUNT; Octopus; SicoTHEO; TGTP Cited in: 11 Publications all top 5 Cited by 19 Authors 1 Bibel, Wolfgang 1 Bledsoe, Woodrow W. 1 Bonacina, Maria Paola 1 Boyer, Robert S. 1 Feng, Guohui 1 Goller, Christoph 1 Horton, Joseph D. 1 Hsiang, Jieh 1 Iwanuma, Koji 1 Letz, Reinhold 1 Loveland, Donald W. 1 Newborn, Monty 1 Otten, Jens 1 Reed, David W. 1 Segre, Alberto Maria 1 Spencer, Bruce D. 1 Stickel, Mark E. 1 Sturgill, David B. 1 Wang, Zongyan all top 5 Cited in 7 Serials 3 Journal of Automated Reasoning 1 Artificial Intelligence 1 Theoretical Computer Science 1 Journal of Symbolic Computation 1 Information and Computation 1 Annals of Mathematics and Artificial Intelligence 1 Automated Reasoning Series Cited in 2 Fields 10 Computer science (68-XX) 2 Mathematical logic and foundations (03-XX) Citations by Year