scientific article; zbMATH DE number 4164171
From MaRDI portal
zbMATH Open0708.68060MaRDI QIDQ3490989FDOQ3490989
Robert S. Boyer, J Strother Moore
Publication date: 1990
Title of this publication is not available (Why is that?)
Cited In (29)
- Prolegomena to a theory of mechanized formal reasoning
- A Modular Equational Generalization Algorithm
- A theorem prover for Boolean BI
- A taxonomy of exact methods for partial Max-SAT
- E-generalization using grammars
- Rippling: A heuristic for guiding inductive proofs
- Inferring the equivalence of functional programs that mutate data
- Sound generalizations in mathematical induction
- A machine program for theorem-proving
- A framework for the verification of certifying computations
- Theorem Proving in Higher Order Logics
- On observational equivalence and algebraic specification
- An experimental logic based on the fundamental deduction principle
- Efficient second-order matching
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Automata-driven automated induction
- A rewriting approach to satisfiability procedures.
- An Evaluation Based Theorem Prover
- A circumscriptive theorem prover
- A metatheory of a mechanized object theory
- Meta-circular interpreter for a strongly typed language
- Shallow confluence of conditional term rewriting systems
- Proving Ramsey's theory by the cover set induction: A case and comparision study.
- Induction using term orderings
- Synthesis of ML programs in the system Coq
- A general framework to build contextual cover set induction provers
- The automated proof of a trace transformation for a bitonic sort
- Program tactics and logic tactics
- The expressiveness of a family of finite set languages
Uses Software
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3490989)
