scientific article; zbMATH DE number 4164171
From MaRDI portal
Recommendations
Cited in
(32)- Synthesis of ML programs in the system Coq
- E-generalization using grammars
- A theorem prover for a computational logic
- A taxonomy of exact methods for partial Max-SAT
- An experimental logic based on the fundamental deduction principle
- Building Theorem Provers
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Shallow confluence of conditional term rewriting systems
- Program tactics and logic tactics
- scientific article; zbMATH DE number 2024610 (Why is no real title available?)
- Meta-circular interpreter for a strongly typed language
- A machine program for theorem-proving
- A Modular Equational Generalization Algorithm
- The expressiveness of a family of finite set languages
- Theorem Proving in Higher Order Logics
- A theorem prover for Boolean BI
- On observational equivalence and algebraic specification
- Prolegomena to a theory of mechanized formal reasoning
- Proving Ramsey's theory by the cover set induction: A case and comparision study.
- An Evaluation Based Theorem Prover
- Automata-driven automated induction
- A framework for the verification of certifying computations
- A circumscriptive theorem prover
- A rewriting approach to satisfiability procedures.
- A general framework to build contextual cover set induction provers
- A metatheory of a mechanized object theory
- Efficient second-order matching
- Rippling: A heuristic for guiding inductive proofs
- The automated proof of a trace transformation for a bitonic sort
- Sound generalizations in mathematical induction
- Induction using term orderings
- Inferring the equivalence of functional programs that mutate data
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)
