Narrowing based inductive proof search
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 42059 (Why is no real title available?)
- scientific article; zbMATH DE number 2090032 (Why is no real title available?)
- HOL-\(\lambda\sigma\): An intentional first-order expression of higher-order logic
- Induction = I-axiomatization + first-order consistency.
- Inductive proof search modulo
- Proof search and proof check for equational and inductive theorems.
- Pure patterns type systems
- Rewriting
- Rippling: Meta-Level Guidance for Mathematical Reasoning
- Term Rewriting and All That
- The force on an elastic singularity in a nonhomogeneous medium
- Theorem proving modulo
Cited in
(7)- Focused Inductive Theorem Proving
- scientific article; zbMATH DE number 139989 (Why is no real title available?)
- Sentence-normalized conditional narrowing modulo in rewriting logic and Maude
- Inductive proof search modulo
- Narrowing, Abstraction and Constraints for Proving Properties of Reduction Relations
- A Maude environment for CafeOBJ
- Higher-order proof construction based on first-order narrowing
This page was built for publication: Narrowing based inductive proof search
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4916079)
