## Automated Theorem Proving: After 25 Years: After 25 Years |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

1 | |

Citation to Hao Wang | 47 |

Computer Theorem Proving and Artificial Intelligence | 49 |

Citation to Lawrence Wos and Steven Winker | 71 |

Open Questions Solved with the Assistance of AURA | 73 |

Some Automatic Proofs in Analysis | 89 |

ProofChecking TheoremProving and Program Verification | 119 |

A Mechanical Proof of the Turing Completeness of Pure LISP | 133 |

Abelian Group Unification Algorithms for Elementary Terms | 193 |

Combining Satisfiability Procedures by Equality Sharing | 201 |

On the Decision Problem and the Mechanization of TheoremProving in Elementary Geometry | 213 |

Some Recent Advances in Mechanical Theoremproving of Geometries | 235 |

Proving Elementary Geometry Theorems Using Wus Algorithm | 243 |

Automated Theory Formation in Mathematics | 287 |

Student Use of an Interactive Theorem Prover | 315 |

Automating Higherorder Logic | 169 |

### Other editions - View all

Automated Theorem Proving: After 25 Years W. W. Bledsoe,Donald W. Loveland No preview available - 1984 |

### Common terms and phrases

algebraic algorithm application automated theorem proving automatic Bledsoe Boyer BTMP Cantor's Theorem clauses command complete concept conjunction CONS current goal decision procedures defined definition elementary geometry EQUAL equations EVAL example EXCHECK facet finite first-order logic formal formula function G J J Hao Wang heuristics higher-order logic hypothesis implies induction inference rules input instantiated instr st integer inv F inv G irreducible LISP LISP program logic Loveland Mach Math Mathematics Mechanical method Natural Deduction open questions polynomials predicate calculus problem Proc program verification proof procedure proving theorems quantifiers recursive reduce resolution rewrite rules s-expression semigroup set theory single axiom ſº ST SYM ST TAPE TM student subgoals symbols task tion TMI ST TAPE TMIN Turing completeness Turing machine type theory variables verification Wang Winker Wu's