Inductive proof search modulo

DOI10.1007/S10472-009-9154-5MaRDI QIDQ1037404zbMATH OpenOpenAlexFDO

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

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

Mechanization of proofs and logical operations (03B35)

Recommendations

• Narrowing based inductive proof search
• Theorem proving modulo
• Publication:4028349
• Publication:3347863
• Experimenting with deduction modulo

Cites work

• scientific article; zbMATH DE number 1722668 (Why is no real title available?)
• scientific article; zbMATH DE number 1722718 (Why is no real title available?)
• scientific article; zbMATH DE number 3956434 (Why is no real title available?)
• scientific article; zbMATH DE number 3684925 (Why is no real title available?)
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 51770 (Why is no real title available?)
• scientific article; zbMATH DE number 2090032 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• A Finite First-Order Theory of Classes
• Complete Sets of Reductions for Some Equational Theories
• Completion of a Set of Rules Modulo a Set of Equations
• Dealing with Non-orientable Equations in Rewriting Induction
• HOL-\(\lambda\sigma\): An intentional first-order expression of higher-order logic
• Implicit induction in conditional theories
• Induction = I-axiomatization + first-order consistency.
• Inductionless induction
• Isabelle/HOL. A proof assistant for higher-order logic
• Narrowing based inductive proof search
• Proof search and proof check for equational and inductive theorems.
• Sequent calculi for induction and infinite descent
• Superdeduction at Work
• Term Rewriting and All That
• The force on an elastic singularity in a nonhomogeneous medium
• Theorem proving modulo

Cited in

(4)

• Proof search and proof check for equational and inductive theorems.
• Narrowing based inductive proof search
• Narrowing, Abstraction and Constraints for Proving Properties of Reduction Relations
• Automated Certification of Implicit Induction Proofs

Describes a project that uses

Uses Software

• ACL2
• Stratego
• SPIKE
• RRL

This page was built for publication: Inductive proof search modulo

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1037404)