scientific article
From MaRDI portal
Publication:3835049
zbMath0678.68091MaRDI QIDQ3835049
J. Strother Moore, Robert S. Boyer
Publication date: 1988
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
Introduction to the OBDD algorithm for the ATP community, An overview of the Tecton proof system, New uses of linear arithmetic in automated theorem proving by induction, A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures, Constraint contextual rewriting., A taxonomy of exact methods for partial Max-SAT, A reconstruction and extension of Maple's assume facility via constraint contextual rewriting, Proving theorems by reuse, Specification and proof in membership equational logic, Mechanically certifying formula-based Noetherian induction reasoning, Theorem proving in cancellative abelian monoids (extended abstract), A semi-algorithm for algebraic implementation proofs, Deduction as an Engineering Science, Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs, Learning Strategies for Mechanised Building of Decision Procedures, An ordinal measure based procedure for termination of functions, The control layer in open mechanized reasoning systems: Annotations and tactics, Superposition theorem proving for abelian groups represented as integer modules, Milestones from the Pure Lisp Theorem Prover to ACL2, Shallow confluence of conditional term rewriting systems, Bottom-up evaluation of Datalog programs with arithmetic constraints, Str∔ve and integers, Superposition theorem proving for abelian groups represented as integer modules, Combining Theories with Shared Set Operations, Cancellative Abelian monoids and related structures in refutational theorem proving. I
Uses Software
