Inductive proof search modulo

DOI10.1007/s10472-009-9154-5zbMath1192.68631OpenAlexW1971274612MaRDI QIDQ1037404

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

Publication date: 16 November 2009

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/inria-00337380/document

zbMATH Keywords

equational rewrite system

Mathematics Subject Classification ID

Related Items (2)

Narrowing Based Inductive Proof Search ⋮ Automated Certification of Implicit Induction Proofs

Uses Software

• ACL2
• Stratego
• SPIKE
• RRL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Theorem proving modulo
• Isabelle/HOL. A proof assistant for higher-order logic
• Induction = I-axiomatization + first-order consistency.
• Implicit induction in conditional theories
• The force on an elastic singularity in a nonhomogeneous medium
• HOL-λσ: an intentional first-order expression of higher-order logic
• Sequent calculi for induction and infinite descent
• Dealing with Non-orientable Equations in Rewriting Induction
• Superdeduction at Work
• A Finite First-Order Theory of Classes
• Completion of a Set of Rules Modulo a Set of Equations
• Complete Sets of Reductions for Some Equational Theories
• Term Rewriting and All That
• Narrowing Based Inductive Proof Search
• Automated Deduction – CADE-19

This page was built for publication: Inductive proof search modulo