Narrowing based inductive proof search

DOI10.1007/978-3-642-37651-1_9MaRDI QIDQ4916079zbMATH OpenOpenAlexFDO

Authors Claude Kirchner, Hélène Kirchner, Fabrice Nahon

Publication date 19 April 2013

Published in Programming Logics (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-00692193/file/hg2011.pdf

zbMATH Keywords

inductionterm rewritingequational reasoningNoetherian inductiondeduction modulosequent calculus moduloinduction by rewriting

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Mechanization of proofs and logical operations (03B35)

Recommendations

• Inductive proof search modulo
• Theorem proving modulo
• scientific article; zbMATH DE number 139989
• scientific article; zbMATH DE number 1765670
• On narrowing, refutation proofs and constraints

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)

• Inductive proof search modulo
• Narrowing, Abstraction and Constraints for Proving Properties of Reduction Relations
• Sentence-normalized conditional narrowing modulo in rewriting logic and Maude
• scientific article; zbMATH DE number 139989 (Why is no real title available?)
• A Maude environment for CafeOBJ
• Higher-order proof construction based on first-order narrowing
• Focused Inductive Theorem Proving

Describes a project that uses

Uses Software

• SPIKE
• RRL

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)