## 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

all
top 5

### Cited in 7 Serials

### Cited in 2 Fields

10 | Computer science (68-XX) |

2 | Mathematical logic and foundations (03-XX) |