Automated Reasoning: Essays in Honor of Woody BledsoeRobert S. Boyer |
Contents
High Performance Theorem Provers | 31 |
Automatic Proofs of Theorems | 61 |
Perspectives on Automated Deduction | 77 |
Copyright | |
11 other sections not shown
Other editions - View all
Common terms and phrases
A-literal algorithm analysis applied approach Argonne Artificial Intelligence automated reasoning program Automated Theorem Proving axiom system back-propagation Bledsoe's C₁ C₂ cand case-based reasoning chain chemotaxis clauses combinatory logic compilation complete Computer Science contains CPU seconds database decision procedure defined delegates depth measure em-clauses em-literal example expression finite formal formula Fortran function given goal hyper implementation input lemmas linear linked inference literal Logic Programming Łukasiewicz mathematics ME-depth mega-clauses METEOR method model elimination node non-standard optimal OTTER p-resolution Paraconsistent Logics PATDEX PATDEX/2 performance predicate problem processors Prolog proof plans prove PTTP random walks recursive resolution rewrite rules search tree sentential calculus sequences shorter proof situation calculus solving stack standard steps strategy structure subsumption symbols symptom values techniques Theorem Prover theorem-proving theory thesis truth values University of Texas unsatisfiable UR-PTTP UR-resolution variables verification W. W. Bledsoe weight Woody Bledsoe