Narrowing Based Inductive Proof Search

DOI10.1007/978-3-642-37651-1_9zbMath1383.03019OpenAlexW1552653843MaRDI QIDQ4916079

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

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

equational reasoninginductionterm rewritingNoetherian inductiondeduction modulosequent calculus moduloinduction by rewriting

Mathematics Subject Classification ID

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

Related Items

Sentence-normalized conditional narrowing modulo in rewriting logic and Maude, A Maude environment for CafeOBJ, Inductive proof search modulo

Uses Software

• SPIKE
• RRL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Inductive proof search modulo
• Theorem proving modulo
• Induction = I-axiomatization + first-order consistency.
• The force on an elastic singularity in a nonhomogeneous medium
• HOL-λσ: an intentional first-order expression of higher-order logic
• Pure patterns type systems
• Term Rewriting and All That
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• Automated Deduction – CADE-19