Narrowing based inductive proof search

DOI10.1007/978-3-642-37651-1_9zbMATH Open1383.03019OpenAlexW1552653843MaRDI QIDQ4916079FDOQ4916079

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

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

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)

Cites Work

• Title not available (Why is that?)
• Term Rewriting and All That
• Rewriting
• Theorem proving modulo
• The force on an elastic singularity in a nonhomogeneous medium
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• Proof search and proof check for equational and inductive theorems.
• HOL-\(\lambda\sigma\): An intentional first-order expression of higher-order logic
• Pure patterns type systems
• Induction = I-axiomatization + first-order consistency.
• Inductive proof search modulo
• Title not available (Why is that?)

Cited In (7)

• Focused Inductive Theorem Proving
• Title not available (Why is that?)
• 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

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)